Documentation Verification Report

Preimmersion

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

Statistics

Metric	Count
Definitions `IsPreimmersion`	1
Theorems `SpecMap_iff`, `Spec_map_iff`, `base_embedding`, `comp`, `comp_iff`, `instFstScheme`, `instIsMultiplicativeScheme`, `instIsStableUnderBaseChangeScheme`, `instIsZariskiLocalAtTarget`, `instMonoScheme`, `instMorphismRestrict`, `instOfIsOpenImmersion`, `instSndScheme`, `isEmbedding`, `mk_SpecMap`, `mk_Spec_map`, `of_comp`, `of_isLocalization`, `toSurjectiveOnStalks`, `isEmbedding`, `isPreimmersion_eq_inf`, `isPreimmersion_iff`	22
Total	23

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsPreimmersion` 📖	CompData	30 math math: `IsPreimmersion.of_isLocalization`, `IsPreimmersion.mk_SpecMap`, `Scheme.IdealSheafData.instIsPreimmersionSubschemeι`, `IsPreimmersion.instOfIsOpenImmersion`, `isImmersion_eq_inf`, `IsPreimmersion.mk_Spec_map`, `IsPreimmersion.Spec_map_iff`, `IsClosedImmersion.iff_isPreimmersion`, `isImmersion_iff`, `Scheme.instIsPreimmersionFromSpecResidueField`, `isPreimmersion_eq_inf`, `isPreimmersion_iff`, `IsClosedImmersion.instIsPreimmersion`, `Scheme.IdealSheafData.instIsPreimmersionGlueDataObjι`, `IsPreimmersion.SpecMap_iff`, `IsPreimmersion.instSndScheme`, `instIsPreimmersionFromSpecStalk`, `IsImmersion.toIsPreimmersion`, `Scheme.instIsPreimmersionMapResidue`, `IsPreimmersion.of_comp`, `IsAffineOpen.fromSpecStalk_isPreimmersion`, `IsPreimmersion.instIsMultiplicativeScheme`, `IsPreimmersion.instFstScheme`, `IsPreimmersion.instIsStableUnderBaseChangeScheme`, `instIsPreimmersionAsFiberHom`, `IsPreimmersion.instMorphismRestrict`, `instIsPreimmersionFiberι`, `IsPreimmersion.comp_iff`, `IsPreimmersion.comp`, `IsPreimmersion.instIsZariskiLocalAtTarget`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPreimmersion_eq_inf` 📖	mathematical	—	`IsPreimmersion` `CategoryTheory.MorphismProperty` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `SurjectiveOnStalks` `topologically` `Topology.IsEmbedding`	—	`isPreimmersion_iff`
`isPreimmersion_iff` 📖	mathematical	—	`IsPreimmersion` `SurjectiveOnStalks` `Topology.IsEmbedding` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'`	—	—

AlgebraicGeometry.IsPreimmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SpecMap_iff` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map` `Topology.IsEmbedding` `PrimeSpectrum` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `PrimeSpectrum.zariskiTopology` `PrimeSpectrum.comap` `CommRingCat.Hom.hom` `RingHom.SurjectiveOnStalks`	—	`AlgebraicGeometry.HasRingHomProperty.Spec_iff` `AlgebraicGeometry.SurjectiveOnStalks.instHasRingHomPropertySurjectiveOnStalks` `AlgebraicGeometry.isPreimmersion_iff`
`Spec_map_iff` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map` `Topology.IsEmbedding` `PrimeSpectrum` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `PrimeSpectrum.zariskiTopology` `PrimeSpectrum.comap` `CommRingCat.Hom.hom` `RingHom.SurjectiveOnStalks`	—	`SpecMap_iff`
`base_embedding` 📖	mathematical	—	`Topology.IsEmbedding` `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'`	—	`AlgebraicGeometry.Scheme.Hom.isEmbedding`
`comp` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `instIsMultiplicativeScheme`
`comp_iff` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`of_comp` `comp`
`instFstScheme` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion` `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`
`instIsMultiplicativeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsPreimmersion`	—	`instOfIsOpenImmersion` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id` `AlgebraicGeometry.SurjectiveOnStalks.comp` `toSurjectiveOnStalks` `Topology.IsEmbedding.comp` `AlgebraicGeometry.Scheme.Hom.isEmbedding`
`instIsStableUnderBaseChangeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.IsPreimmersion`	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk'` `CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects` `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion` `instIsZariskiLocalAtTarget` `CategoryTheory.MorphismProperty.pullback_fst` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `AlgebraicGeometry.SurjectiveOnStalks.stableUnderBaseChange` `toSurjectiveOnStalks` `CategoryTheory.Limits.pullback.condition` `Topology.IsEmbedding.of_comp` `Continuous.prodMk` `AlgebraicGeometry.Scheme.Hom.continuous` `continuous_subtype_val` `AlgebraicGeometry.SurjectiveOnStalks.isEmbedding_pullback` `Topology.IsEmbedding.comp` `AlgebraicGeometry.Scheme.Hom.isEmbedding` `Topology.IsEmbedding.subtypeVal` `Homeomorph.isEmbedding`
`instIsZariskiLocalAtTarget` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtTarget` `AlgebraicGeometry.IsPreimmersion`	—	`CategoryTheory.MorphismProperty.IsLocalAtTarget.inf` `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion` `AlgebraicGeometry.SurjectiveOnStalks.instIsZariskiLocalAtTarget` `AlgebraicGeometry.isEmbedding_isZariskiLocalAtTarget` `AlgebraicGeometry.isPreimmersion_eq_inf`
`instMonoScheme` 📖	mathematical	—	`CategoryTheory.Mono` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`AlgebraicGeometry.SurjectiveOnStalks.mono_of_injective` `toSurjectiveOnStalks` `Topology.IsEmbedding.injective` `AlgebraicGeometry.Scheme.Hom.isEmbedding`
`instMorphismRestrict` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion` `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` `instIsZariskiLocalAtTarget`
`instOfIsOpenImmersion` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.ConcreteCategory.bijective_of_isIso` `AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap` `Topology.IsOpenEmbedding.isEmbedding` `AlgebraicGeometry.Scheme.Hom.isOpenEmbedding`
`instSndScheme` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion` `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`
`isEmbedding` 📖	mathematical	—	`Topology.IsEmbedding` `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'`	—	—
`mk_SpecMap` 📖	mathematical	`Topology.IsEmbedding` `PrimeSpectrum` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `PrimeSpectrum.zariskiTopology` `PrimeSpectrum.comap` `CommRingCat.Hom.hom` `RingHom.SurjectiveOnStalks`	`AlgebraicGeometry.IsPreimmersion` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map`	—	`SpecMap_iff`
`mk_Spec_map` 📖	mathematical	`Topology.IsEmbedding` `PrimeSpectrum` `CommRingCat.carrier` `CommRing.toCommSemiring` `CommRingCat.commRing` `PrimeSpectrum.zariskiTopology` `PrimeSpectrum.comap` `CommRingCat.Hom.hom` `RingHom.SurjectiveOnStalks`	`AlgebraicGeometry.IsPreimmersion` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map`	—	`mk_SpecMap`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.Scheme.Hom.stalkMap_surjective` `toSurjectiveOnStalks` `Function.Surjective.of_comp` `AlgebraicGeometry.Scheme.Hom.stalkMap_comp` `AlgebraicGeometry.Scheme.Hom.isEmbedding` `Topology.IsEmbedding.of_comp_iff`
`of_isLocalization` 📖	mathematical	—	`AlgebraicGeometry.IsPreimmersion` `AlgebraicGeometry.Spec` `CommRingCat.of` `AlgebraicGeometry.Spec.map` `CommRingCat.ofHom` `algebraMap` `CommRing.toCommSemiring` `CommSemiring.toSemiring`	—	`mk_SpecMap` `PrimeSpectrum.localization_comap_isEmbedding` `RingHom.surjectiveOnStalks_of_isLocalization`
`toSurjectiveOnStalks` 📖	mathematical	—	`AlgebraicGeometry.SurjectiveOnStalks`	—	—

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmbedding` 📖	mathematical	—	`Topology.IsEmbedding` `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'`	—	`AlgebraicGeometry.IsPreimmersion.isEmbedding`

---

← Back to Index