Irreducible

📁 Source: Mathlib/AlgebraicGeometry/Geometrically/Irreducible.lean

Statistics

Metric	Count
Definitions GeometricallyIrreducible, irreducibleComponentsEquiv	2
Theorems comp, eq_geometrically, geometrically_irreducibleSpace, iff_geometricallyIrreducible_fiber, irreducibleSpace, irreducibleSpace_of_subsingleton, irreducibleComponentsEquiv_apply_coe, irreducibleComponentsEquiv_symm_apply_coe, isIrreducible_preimage, geometricallyIrreducible_iff, instGeometricallyIrreducibleCompSchemeOfIsOpenImmersionOfSurjective, instGeometricallyIrreducibleFiberToSpecResidueField, instGeometricallyIrreducibleFstScheme, instGeometricallyIrreducibleMorphismRestrict, instGeometricallyIrreducibleSndScheme, instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible, instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen, instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1, instIsStableUnderBaseChangeSchemeGeometricallyIrreducible, instSurjectiveOfGeometricallyIrreducible	20
Total	22

AlgebraicGeometry

Definitions

Name	Category	Theorems
GeometricallyIrreducible 📖	CompData	12 math math: instIsStableUnderBaseChangeSchemeGeometricallyIrreducible, instGeometricallyIrreducibleOfGeometricallyIntegral, instGeometricallyIrreducibleMorphismRestrict, GeometricallyIrreducible.comp, GeometricallyIrreducible.iff_geometricallyIrreducible_fiber, instGeometricallyIrreducibleCompSchemeOfIsOpenImmersionOfSurjective, instGeometricallyIrreducibleSndScheme, GeometricallyIrreducible.eq_geometrically, geometricallyIrreducible_iff, GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible, instGeometricallyIrreducibleFstScheme, instGeometricallyIrreducibleFiberToSpecResidueField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geometricallyIrreducible_iff 📖	mathematical	—	GeometricallyIrreducible geometrically IrreducibleSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—
instGeometricallyIrreducibleCompSchemeOfIsOpenImmersionOfSurjective 📖	mathematical	—	GeometricallyIrreducible CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory	—	GeometricallyIrreducible.iff_geometricallyIrreducible_fiber Scheme.Pullback.instHasPullback geometrically_iff_of_isClosedUnderIsomorphisms instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.limit.lift_π Equiv.nonempty_congr Set.nonempty_coe_sort Set.Nonempty.preimage Set.singleton_nonempty Scheme.Hom.surjective Topology.IsOpenEmbedding.irreducibleSpace Scheme.Hom.isOpenEmbedding Scheme.pullback_map_isOpenImmersion IsOpenImmersion.of_isIso CategoryTheory.IsIso.id IsOpenImmersion.mono instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen instGeometricallyIrreducibleFiberToSpecResidueField instUniversallyOpenOfIsIntegralOfSubsingletonCarrierCarrierCommRingCat instIsIntegralSpecOfIsDomainCarrier instIsDomain Unique.instSubsingleton instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier Scheme.Pullback.instNonemptyCarrierCarrierCommRingCatPullbackOfSubsingleton instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier EuclideanDomain.toNontrivial
instGeometricallyIrreducibleFiberToSpecResidueField 📖	mathematical	—	GeometricallyIrreducible Scheme.Hom.fiber Spec Scheme.residueField Scheme.Hom.fiberToSpecResidueField	—	CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyIrreducible
instGeometricallyIrreducibleFstScheme 📖	mathematical	—	GeometricallyIrreducible CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyIrreducible
instGeometricallyIrreducibleMorphismRestrict 📖	mathematical	—	GeometricallyIrreducible Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict	—	CategoryTheory.MorphismProperty.of_isPullback instIsStableUnderBaseChangeSchemeGeometricallyIrreducible CategoryTheory.IsPullback.flip isPullback_morphismRestrict
instGeometricallyIrreducibleSndScheme 📖	mathematical	—	GeometricallyIrreducible CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyIrreducible
instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible 📖	mathematical	—	IrreducibleSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace Scheme.Hom.fiber SheafedSpace.instTopologicalSpaceCarrierCarrier	—	GeometricallyIrreducible.geometrically_irreducibleSpace CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPullback.of_hasPullback
instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen 📖	mathematical	—	IrreducibleSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback SheafedSpace.instTopologicalSpaceCarrierCarrier	—	GeometricallyIrreducible.irreducibleSpace Scheme.Pullback.instHasPullback instGeometricallyIrreducibleSndScheme Scheme.Hom.isOpenMap UniversallyOpen.snd
instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1 📖	mathematical	—	IrreducibleSpace TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback SheafedSpace.instTopologicalSpaceCarrierCarrier	—	GeometricallyIrreducible.irreducibleSpace Scheme.Pullback.instHasPullback instGeometricallyIrreducibleFstScheme Scheme.Hom.isOpenMap UniversallyOpen.fst
instIsStableUnderBaseChangeSchemeGeometricallyIrreducible 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange Scheme Scheme.instCategory GeometricallyIrreducible	—	instIsStableUnderBaseChangeSchemeGeometrically GeometricallyIrreducible.eq_geometrically
instSurjectiveOfGeometricallyIrreducible 📖	mathematical	—	Surjective	—	ConnectedSpace.toNonempty IrreducibleSpace.connectedSpace instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible Eq.le Scheme.Hom.range_fiberι

AlgebraicGeometry.GeometricallyIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	AlgebraicGeometry.GeometricallyIrreducible CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.geometrically_iff_of_isClosedUnderIsomorphisms AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat CategoryTheory.Limits.hasPullbackHorizPaste Homeomorph.irreducibleSpace_iff CategoryTheory.Iso.isIso_hom AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier instIsDomain
eq_geometrically 📖	mathematical	—	AlgebraicGeometry.GeometricallyIrreducible AlgebraicGeometry.geometrically IrreducibleSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	AlgebraicGeometry.geometricallyIrreducible_iff
geometrically_irreducibleSpace 📖	mathematical	—	AlgebraicGeometry.geometrically IrreducibleSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	—
iff_geometricallyIrreducible_fiber 📖	mathematical	—	AlgebraicGeometry.GeometricallyIrreducible AlgebraicGeometry.Scheme.Hom.fiber AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField	—	eq_geometrically
irreducibleSpace 📖	mathematical	IsOpenMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	IrreducibleSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	AlgebraicGeometry.Scheme.Hom.isIrreducible_preimage IrreducibleSpace.isIrreducible_univ
irreducibleSpace_of_subsingleton 📖	mathematical	—	IrreducibleSpace TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	instPreirreducibleSpaceOfSubsingleton irreducibleSpace isOpen_discrete Subsingleton.discreteTopology

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
irreducibleComponentsEquiv 📖	CompOp	2 math math: irreducibleComponentsEquiv_symm_apply_coe, irreducibleComponentsEquiv_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
irreducibleComponentsEquiv_apply_coe 📖	mathematical	IsOpenMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instMembership irreducibleComponents AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike irreducibleComponentsEquiv Set.image ContinuousMap TopCat.str CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	—
irreducibleComponentsEquiv_symm_apply_coe 📖	mathematical	IsOpenMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instMembership irreducibleComponents AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm irreducibleComponentsEquiv Set.preimage ContinuousMap TopCat.str CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	—
isIrreducible_preimage 📖	mathematical	IsOpenMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' IsIrreducible	IsIrreducible TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set.preimage DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom'	—	range_fiberι Set.image_univ IsIrreducible.image IrreducibleSpace.isIrreducible_univ AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible Continuous.continuousOn continuous IsIrreducible.preimage_of_isPreirreducible_fiber IsIrreducible.isPreirreducible isIrreducible_singleton Set.range_eq_univ surjective AlgebraicGeometry.instSurjectiveOfGeometricallyIrreducible Set.inter_univ IsIrreducible.nonempty

---

← Back to Index