Integral

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

Statistics

Metric	Count
Definitions `IsIntegralHom`	1
Theorems `SpecMap_iff`, `comp_iff`, `eq_universallyClosed_inf_isAffineHom`, `hasAffineProperty`, `iff_universallyClosed_and_isAffineHom`, `instCompScheme`, `instDescScheme`, `instFstScheme`, `instHasOfPostcompPropertySchemeIsSeparated`, `instIsMultiplicativeScheme`, `instIsMultiplicativeScheme_1`, `instIsStableUnderBaseChangeScheme`, `instIsStableUnderCompositionScheme`, `instMorphismRestrict`, `instOfIsClosedImmersion`, `instSndScheme`, `instUniversallyClosed`, `integral_app`, `isIntegral_app`, `of_comp`, `toIsAffineHom`, `isIntegral_app`, `isIntegralHom_iff`	23
Total	24

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsIntegralHom` 📖	CompData	25 math math: `AffineSpace.not_isIntegralHom`, `IsIntegralHom.iff_universallyClosed_and_isAffineHom`, `IsIntegralHom.instSndScheme`, `IsIntegralHom.instIsStableUnderCompositionScheme`, `IsIntegralHom.instOfIsClosedImmersion`, `IsIntegralHom.instFstScheme`, `Scheme.Hom.instIsIntegralHomNormalizationDesc`, `IsIntegralHom.instIsMultiplicativeScheme_1`, `IsIntegralHom.instMorphismRestrict`, `IsIntegralHom.of_comp`, `Scheme.Hom.instIsIntegralHomFromNormalization`, `IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparated`, `AffineSpace.isIntegralHom_over_iff_isEmpty`, `isIntegralHom_iff`, `IsIntegralHom.SpecMap_iff`, `IsIntegralHom.hasAffineProperty`, `IsFinite.instIsIntegralHom`, `IsIntegralHom.instDescScheme`, `IsFinite.iff_isIntegralHom_and_locallyOfFiniteType`, `IsIntegralHom.instIsStableUnderBaseChangeScheme`, `IsFinite.eq_inf`, `IsIntegralHom.instIsMultiplicativeScheme`, `IsIntegralHom.instCompScheme`, `IsIntegralHom.eq_universallyClosed_inf_isAffineHom`, `IsIntegralHom.comp_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegralHom_iff` 📖	mathematical	—	`IsIntegralHom` `IsAffineHom` `RingHom.IsIntegral` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `Scheme.Opens` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRing.toRing` `CommRingCat.Hom.hom` `Scheme.Hom.app`	—	—

AlgebraicGeometry.IsIntegralHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SpecMap_iff` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map` `RingHom.IsIntegral` `CommRingCat.carrier` `CommRingCat.commRing` `CommRing.toRing` `CommRingCat.Hom.hom`	—	`RingHom.toMorphismProperty_respectsIso_iff` `RingHom.isIntegral_respectsIso` `AlgebraicGeometry.HasAffineProperty.iff_of_isAffine` `hasAffineProperty` `AlgebraicGeometry.isAffine_Spec` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff`
`comp_iff` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`of_comp` `AlgebraicGeometry.IsSeparated.of_isAffineHom` `toIsAffineHom` `instCompScheme`
`eq_universallyClosed_inf_isAffineHom` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `CategoryTheory.MorphismProperty` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.UniversallyClosed` `AlgebraicGeometry.IsAffineHom`	—	`iff_universallyClosed_and_isAffineHom`
`hasAffineProperty` 📖	mathematical	—	`AlgebraicGeometry.HasAffineProperty` `AlgebraicGeometry.IsIntegralHom` `AlgebraicGeometry.IsAffine` `RingHom.IsIntegral` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `Top.top` `OrderTop.toTop` `Preorder.toLE` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRing.toRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.app`	—	`AlgebraicGeometry.HasAffineProperty.affineAnd_iff` `RingHom.isIntegral_respectsIso` `RingHom.LocalizationPreserves.away` `RingHom.IsStableUnderBaseChange.localizationPreserves` `RingHom.isIntegral_isStableUnderBaseChange` `RingHom.isIntegral_ofLocalizationSpan`
`iff_universallyClosed_and_isAffineHom` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `AlgebraicGeometry.UniversallyClosed` `AlgebraicGeometry.IsAffineHom`	—	`instUniversallyClosed` `toIsAffineHom` `AlgebraicGeometry.Spec.map_preimage` `SpecMap_iff` `PrimeSpectrum.isIntegral_of_isClosedMap_comap_mapRingHom` `AlgebraicGeometry.UniversallyClosed.universally_isClosedMap` `Polynomial.map_one` `Polynomial.map_mul` `Polynomial.map_zero` `Polynomial.map_add` `CategoryTheory.IsPullback.flip` `AlgebraicGeometry.isPullback_SpecMap_of_isPushout` `CommRingCat.isPushout_of_isPushout` `instIsScalarTowerPolynomial` `IsScalarTower.left` `Polynomial.isScalarTower` `IsScalarTower.right` `instIsPushoutPolynomial` `AlgebraicGeometry.isAffine_of_isAffineHom` `AlgebraicGeometry.isAffine_Spec` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion` `AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `hasAffineProperty` `CategoryTheory.Iso.isIso_inv` `AlgebraicGeometry.universallyClosedTypeComp` `AlgebraicGeometry.instUniversallyClosedOfIsClosedImmersion` `AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme` `AlgebraicGeometry.instIsAffineHomCompScheme` `instOfIsClosedImmersion` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `AlgebraicGeometry.universallyClosed_isZariskiLocalAtTarget` `AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine` `AlgebraicGeometry.Scheme.local_affine`
`instCompScheme` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.comp_mem` `instIsStableUnderCompositionScheme`
`instDescScheme` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `CategoryTheory.Limits.coprod` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `AlgebraicGeometry.Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.desc`	—	`AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd` `hasAffineProperty` `RingHom.isIntegral_respectsIso` `algebraMap_isIntegral_iff` `Algebra.IsIntegral.prod`
`instFstScheme` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.MorphismProperty.pullback_fst` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `instIsStableUnderBaseChangeScheme`
`instHasOfPostcompPropertySchemeIsSeparated` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsIntegralHom` `AlgebraicGeometry.IsSeparated`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal` `instIsStableUnderBaseChangeScheme` `instIsMultiplicativeScheme` `AlgebraicGeometry.IsSeparated.isStableUnderBaseChange` `instOfIsClosedImmersion` `AlgebraicGeometry.IsSeparated.diagonal_isClosedImmersion`
`instIsMultiplicativeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsIntegralHom`	—	`instOfIsClosedImmersion` `AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme` `CategoryTheory.IsIso.id` `instIsStableUnderCompositionScheme`
`instIsMultiplicativeScheme_1` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsIntegralHom`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities` `instIsMultiplicativeScheme` `instIsStableUnderCompositionScheme`
`instIsStableUnderBaseChangeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsIntegralHom`	—	`AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderBaseChange` `hasAffineProperty` `RingHom.isIntegral_respectsIso` `RingHom.isIntegral_isStableUnderBaseChange`
`instIsStableUnderCompositionScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsIntegralHom`	—	`AlgebraicGeometry.HasAffineProperty.affineAnd_isStableUnderComposition` `hasAffineProperty` `RingHom.isIntegral_stableUnderComposition`
`instMorphismRestrict` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `AlgebraicGeometry.Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme.Opens` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `AlgebraicGeometry.morphismRestrict`	—	`AlgebraicGeometry.IsZariskiLocalAtTarget.restrict` `AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `hasAffineProperty`
`instOfIsClosedImmersion` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom`	—	`AlgebraicGeometry.IsClosedImmersion.instIsAffineHom` `RingHom.Finite.to_isIntegral` `RingHom.Finite.of_surjective` `AlgebraicGeometry.Scheme.Hom.app_surjective`
`instSndScheme` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.MorphismProperty.pullback_snd` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `instIsStableUnderBaseChangeScheme`
`instUniversallyClosed` 📖	mathematical	—	`AlgebraicGeometry.UniversallyClosed`	—	`AlgebraicGeometry.universallyClosed_eq` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq` `instIsStableUnderBaseChangeScheme` `CategoryTheory.MorphismProperty.universally_mono` `AlgebraicGeometry.Spec.map_surjective` `SpecMap_iff` `PrimeSpectrum.isClosedMap_comap_of_isIntegral` `AlgebraicGeometry.isAffine_of_isAffineHom` `toIsAffineHom` `AlgebraicGeometry.isAffine_Spec` `CategoryTheory.MorphismProperty.cancel_left_of_respectsIso` `AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsClosedMap` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion` `AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget` `hasAffineProperty` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover` `AlgebraicGeometry.isClosedMap_isZariskiLocalAtTarget` `AlgebraicGeometry.Scheme.local_affine`
`integral_app` 📖	mathematical	—	`RingHom.IsIntegral` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRing.toRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.app`	—	`isIntegral_app`
`isIntegral_app` 📖	mathematical	—	`RingHom.IsIntegral` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CommRingCat.commRing` `CommRing.toRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.app`	—	—
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.IsIntegralHom`	—	`CategoryTheory.MorphismProperty.of_postcomp` `instHasOfPostcompPropertySchemeIsSeparated`
`toIsAffineHom` 📖	mathematical	—	`AlgebraicGeometry.IsAffineHom`	—	—

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegral_app` 📖	mathematical	—	`RingHom.IsIntegral` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.Scheme.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `CommRingCat.commRing` `CommRing.toRing` `CommRingCat.Hom.hom` `app`	—	`AlgebraicGeometry.IsIntegralHom.isIntegral_app`

---

← Back to Index