Structures · Topology
IrreducibleSpace
An irreducible space is one that is nonempty and where there is no non-trivial pair of disjoint opens.
- Defined in
- Mathlib.Topology.Irreducible
- Shape
- One type argument · adds toNonempty
Extends1
Extended by0
Nothing extends this class yet.
Forgetful instances
Every IrreducibleSpace is also a
Concrete types that are instances3
- TopCat.carrier
- PrimeSpectrum
- CofiniteTopology
How is a type an instance?
Loading the hierarchy index…
Assumed by43
- AlgebraicGeometry.Scheme.functionField
- genericPoint
- IrreducibleSpace.isIrreducible_univ
- genericPoint_spec
- AlgebraicGeometry.Scheme.germToFunctionField
- AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced
- AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk
- AlgebraicGeometry.Scheme.RationalMap.fromFunctionField
- AlgebraicGeometry.Scheme.PartialMap.fromFunctionField
- AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace
- irreducibleComponents_eq_singleton
- AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion
- AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem_ofFromSpecStalk
- IsIrreducible.of_subtype
- AlgebraicGeometry.Scheme.algebraMap_germ_eq_germToFunctionField
- AlgebraicGeometry.Scheme.PartialMap.equiv_of_fromSpecStalkOfMem_eq
- Function.Surjective.irreducibleSpace
- AlgebraicGeometry.Scheme.PartialMap.id_comp
- AlgebraicGeometry.Scheme.PartialMap.mem_domain_ofFromSpecStalk
- AlgebraicGeometry.functionField_isScalarTower
- AlgebraicGeometry.stalkFunctionFieldAlgebra
- AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen
- AlgebraicGeometry.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme
- AlgebraicGeometry.AffineSpace.instIrreducibleSpaceCarrierCarrierCommRingCat
- AlgebraicGeometry.Scheme.RationalMap.id_comp
- genericPoint_closure
- AlgebraicGeometry.Scheme.instIsIsoIrreducibleComponentιOfIrreducibleSpaceCarrierCarrierCommRingCat
- IrreducibleSpace.connectedSpace
- AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1
- IrreducibleSpace.toPreirreducibleSpace
- genericPoints_eq_singleton
- AlgebraicGeometry.Scheme.PartialMap.comp_assoc
- AlgebraicGeometry.Scheme.RationalMap.isOver_comp
- AlgebraicGeometry.Scheme.irreducibleComponentOpen_eq_top
- Topology.IsOpenEmbedding.irreducibleSpace
- AlgebraicGeometry.Scheme.RationalMap.comp_assoc
- AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk_comp
- genericPoint_specializes
- IrreducibleSpace.toNonempty
- AlgebraicGeometry.Scheme.PartialMap.fromFunctionField_restrict
- AlgebraicGeometry.Scheme.RationalMap.fromFunctionField_toRationalMap
- genericPoint.congr_simp
- AlgebraicGeometry.Scheme.germToFunctionField.congr_simp