Integral

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

Statistics

Metric	Count
Definitions GeometricallyIntegral	1
Theorems eq_geometrically, eq_geometricallyReduced_inf_geometricallyIrreducible, geometrically_isIntegral, iff_geometricallyIntegral_fiber, isIntegral_of_isLocallyNoetherian, isIntegral_of_subsingleton, of_geometricallyReduced_of_geometricallyIrreducible, geometricallyIntegral_iff, instGeometricallyIntegralFiberToSpecResidueField, instGeometricallyIntegralFstScheme, instGeometricallyIntegralMorphismRestrict, instGeometricallyIntegralSndScheme, instGeometricallyIrreducibleOfGeometricallyIntegral, instGeometricallyReducedOfGeometricallyIntegral, instIsIntegralFiberOfGeometricallyIntegral, instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian, instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1, instIsStableUnderBaseChangeSchemeGeometricallyIntegral, instSurjectiveOfGeometricallyIntegral	19
Total	20

AlgebraicGeometry

Definitions

Name	Category	Theorems
GeometricallyIntegral 📖	CompData	10 math math: GeometricallyIntegral.of_geometricallyReduced_of_geometricallyIrreducible, instGeometricallyIntegralSndScheme, instGeometricallyIntegralFiberToSpecResidueField, geometricallyIntegral_iff, instIsStableUnderBaseChangeSchemeGeometricallyIntegral, instGeometricallyIntegralFstScheme, GeometricallyIntegral.iff_geometricallyIntegral_fiber, instGeometricallyIntegralMorphismRestrict, GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible, GeometricallyIntegral.eq_geometrically

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geometricallyIntegral_iff 📖	mathematical	—	GeometricallyIntegral geometrically IsIntegral	—	—
instGeometricallyIntegralFiberToSpecResidueField 📖	mathematical	—	GeometricallyIntegral Scheme.Hom.fiber Spec Scheme.residueField Scheme.Hom.fiberToSpecResidueField	—	CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyIntegral
instGeometricallyIntegralFstScheme 📖	mathematical	—	GeometricallyIntegral CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyIntegral
instGeometricallyIntegralMorphismRestrict 📖	mathematical	—	GeometricallyIntegral 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 instIsStableUnderBaseChangeSchemeGeometricallyIntegral CategoryTheory.IsPullback.flip isPullback_morphismRestrict
instGeometricallyIntegralSndScheme 📖	mathematical	—	GeometricallyIntegral CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyIntegral
instGeometricallyIrreducibleOfGeometricallyIntegral 📖	mathematical	—	GeometricallyIrreducible	—	Eq.le GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible
instGeometricallyReducedOfGeometricallyIntegral 📖	mathematical	—	GeometricallyReduced	—	Eq.le GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible
instIsIntegralFiberOfGeometricallyIntegral 📖	mathematical	—	IsIntegral Scheme.Hom.fiber	—	GeometricallyIntegral.geometrically_isIntegral CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPullback.of_hasPullback
instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian 📖	mathematical	—	IsIntegral CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback	—	GeometricallyIntegral.isIntegral_of_isLocallyNoetherian Scheme.Pullback.instHasPullback instGeometricallyIntegralSndScheme Flat.instSndScheme UniversallyOpen.snd
instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1 📖	mathematical	—	IsIntegral CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback	—	GeometricallyIntegral.isIntegral_of_isLocallyNoetherian Scheme.Pullback.instHasPullback instGeometricallyIntegralFstScheme Flat.instFstScheme UniversallyOpen.fst
instIsStableUnderBaseChangeSchemeGeometricallyIntegral 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange Scheme Scheme.instCategory GeometricallyIntegral	—	instIsStableUnderBaseChangeSchemeGeometrically GeometricallyIntegral.eq_geometrically
instSurjectiveOfGeometricallyIntegral 📖	mathematical	—	Surjective	—	IsIntegral.nonempty instIsIntegralFiberOfGeometricallyIntegral Eq.le Scheme.Hom.range_fiberι

AlgebraicGeometry.GeometricallyIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_geometrically 📖	mathematical	—	AlgebraicGeometry.GeometricallyIntegral AlgebraicGeometry.geometrically AlgebraicGeometry.IsIntegral	—	AlgebraicGeometry.geometricallyIntegral_iff
eq_geometricallyReduced_inf_geometricallyIrreducible 📖	mathematical	—	AlgebraicGeometry.GeometricallyIntegral CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra AlgebraicGeometry.GeometricallyReduced AlgebraicGeometry.GeometricallyIrreducible	—	eq_geometrically AlgebraicGeometry.GeometricallyReduced.eq_geometrically AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically AlgebraicGeometry.geometrically_inf
geometrically_isIntegral 📖	mathematical	—	AlgebraicGeometry.geometrically AlgebraicGeometry.IsIntegral	—	—
iff_geometricallyIntegral_fiber 📖	mathematical	—	AlgebraicGeometry.GeometricallyIntegral AlgebraicGeometry.Scheme.Hom.fiber AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField	—	eq_geometrically
isIntegral_of_isLocallyNoetherian 📖	mathematical	—	AlgebraicGeometry.IsIntegral	—	AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace AlgebraicGeometry.instGeometricallyIrreducibleOfGeometricallyIntegral AlgebraicGeometry.irreducibleSpace_of_isIntegral AlgebraicGeometry.Scheme.Hom.isOpenMap AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian AlgebraicGeometry.instGeometricallyReducedOfGeometricallyIntegral AlgebraicGeometry.isReduced_of_isIntegral
isIntegral_of_subsingleton 📖	mathematical	—	AlgebraicGeometry.IsIntegral	—	AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton AlgebraicGeometry.instGeometricallyIrreducibleOfGeometricallyIntegral AlgebraicGeometry.IsIntegral.nonempty AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian AlgebraicGeometry.instGeometricallyReducedOfGeometricallyIntegral AlgebraicGeometry.Flat.instOfSubsingletonCarrierCarrierCommRingCatOfIsIntegral AlgebraicGeometry.isReduced_of_isIntegral AlgebraicGeometry.IsLocallyArtinian.isLocallyNoetherian AlgebraicGeometry.IsArtinianScheme.toIsLocallyArtinian AlgebraicGeometry.instIsArtinianSchemeOfSubsingletonCarrierCarrierCommRingCatOfIsReduced
of_geometricallyReduced_of_geometricallyIrreducible 📖	mathematical	—	AlgebraicGeometry.GeometricallyIntegral	—	Eq.ge eq_geometricallyReduced_inf_geometricallyIrreducible

---

← Back to Index