Documentation Verification Report

SurjectiveOnStalks

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

Statistics

Metric	Count
Definitions `SurjectiveOnStalks`	1
Theorems `stalkMap_surjective`, `Spec_iff`, `comp`, `eq_stalkwise`, `iff_of_isAffine`, `instHasRingHomPropertySurjectiveOnStalks`, `instIsMultiplicativeScheme`, `instIsZariskiLocalAtSource`, `instIsZariskiLocalAtTarget`, `instOfIsOpenImmersion`, `isEmbedding_pullback`, `mono_of_injective`, `of_comp`, `stableUnderBaseChange`, `stalkMap_surjective`, `surj_on_stalks`, `surjectiveOnStalks_iff`	17
Total	18

AlgebraicGeometry

Definitions

Name	Category	Theorems
`SurjectiveOnStalks` 📖	CompData	18 math math: `SurjectiveOnStalks.eq_stalkwise`, `surjectiveOnStalks_iff`, `SurjectiveOnStalks.iff_of_isAffine`, `SurjectiveOnStalks.instHasRingHomPropertySurjectiveOnStalks`, `SurjectiveOnStalks.of_comp`, `SurjectiveOnStalks.comp`, `SurjectiveOnStalks.instIsZariskiLocalAtTarget`, `SurjectiveOnStalks.instIsZariskiLocalAtSource`, `IsClosedImmersion.eq_inf`, `SurjectiveOnStalks.instOfIsOpenImmersion`, `SurjectiveOnStalks.Spec_iff`, `isPreimmersion_eq_inf`, `isPreimmersion_iff`, `IsPreimmersion.toSurjectiveOnStalks`, `SurjectiveOnStalks.instIsMultiplicativeScheme`, `isClosedImmersion_iff`, `SurjectiveOnStalks.stableUnderBaseChange`, `IsClosedImmersion.toSurjectiveOnStalks`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`surjectiveOnStalks_iff` 📖	mathematical	—	`SurjectiveOnStalks` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `PresheafedSpace.carrier` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `PresheafedSpace.presheaf` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `PresheafedSpace.Hom.base` `LocallyRingedSpace.Hom.toHom` `Scheme.Hom.toLRSHom'` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `Scheme.Hom.stalkMap`	—	`CommRingCat.Colimits.hasColimits_commRingCat`

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stalkMap_surjective` 📖	mathematical	—	`CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.PresheafedSpace.presheaf` `DFunLike.coe` `TopCat.carrier` `CategoryTheory.ConcreteCategory.hom` `TopCat` `TopCat.instCategory` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `stalkMap`	—	`AlgebraicGeometry.SurjectiveOnStalks.stalkMap_surjective`

AlgebraicGeometry.SurjectiveOnStalks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Spec_iff` 📖	mathematical	—	`AlgebraicGeometry.SurjectiveOnStalks` `AlgebraicGeometry.Spec` `AlgebraicGeometry.Spec.map` `RingHom.SurjectiveOnStalks` `CommRingCat.carrier` `CommRingCat.commRing` `CommRingCat.Hom.hom`	—	`eq_stalkwise` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `AlgebraicGeometry.stalkwise_SpecMap_iff` `RingHom.surjective_respectsIso` `RingHom.SurjectiveOnStalks.eq_1`
`comp` 📖	mathematical	—	`AlgebraicGeometry.SurjectiveOnStalks` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `instIsMultiplicativeScheme`
`eq_stalkwise` 📖	mathematical	—	`AlgebraicGeometry.SurjectiveOnStalks` `AlgebraicGeometry.stalkwise` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`AlgebraicGeometry.surjectiveOnStalks_iff`
`iff_of_isAffine` 📖	mathematical	—	`AlgebraicGeometry.SurjectiveOnStalks` `RingHom.SurjectiveOnStalks` `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` `CommRingCat.commRing` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.app`	—	`Spec_iff` `CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects` `instIsZariskiLocalAtSource`
`instHasRingHomPropertySurjectiveOnStalks` 📖	mathematical	—	`AlgebraicGeometry.HasRingHomProperty` `AlgebraicGeometry.SurjectiveOnStalks` `RingHom.SurjectiveOnStalks`	—	`AlgebraicGeometry.HasRingHomProperty.stalkwise` `RingHom.surjective_respectsIso` `eq_stalkwise`
`instIsMultiplicativeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.SurjectiveOnStalks`	—	`instOfIsOpenImmersion` `AlgebraicGeometry.IsOpenImmersion.of_isIso` `CategoryTheory.IsIso.id` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.Scheme.Hom.stalkMap_comp` `AlgebraicGeometry.Scheme.Hom.stalkMap_surjective`
`instIsZariskiLocalAtSource` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtSource` `AlgebraicGeometry.SurjectiveOnStalks`	—	`AlgebraicGeometry.stalkwise_isZariskiLocalAtSource_of_respectsIso` `RingHom.surjective_respectsIso` `eq_stalkwise`
`instIsZariskiLocalAtTarget` 📖	mathematical	—	`AlgebraicGeometry.IsZariskiLocalAtTarget` `AlgebraicGeometry.SurjectiveOnStalks`	—	`AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIso` `RingHom.surjective_respectsIso` `eq_stalkwise`
`instOfIsOpenImmersion` 📖	mathematical	—	`AlgebraicGeometry.SurjectiveOnStalks`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `CategoryTheory.ConcreteCategory.bijective_of_isIso` `AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap`
`isEmbedding_pullback` 📖	mathematical	—	`Topology.IsEmbedding` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `instTopologicalSpaceProd` `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'` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.Limits.pullback.snd`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullback` `comp` `instOfIsOpenImmersion` `of_comp` `AlgebraicGeometry.Spec.map_preimage` `Homeomorph.surjective` `CategoryTheory.Limits.pullback.lift_fst` `CategoryTheory.Iso.inv_hom_id` `AlgebraicGeometry.Scheme.Hom.comp_apply` `AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc` `CategoryTheory.Limits.pullback.lift_snd` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc` `Topology.IsEmbedding.comp` `Topology.IsOpenEmbedding.isEmbedding` `Topology.IsOpenEmbedding.prodMap` `AlgebraicGeometry.Scheme.Hom.isOpenEmbedding` `PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks` `AlgebraicGeometry.HasRingHomProperty.Spec_iff` `instHasRingHomPropertySurjectiveOnStalks` `Homeomorph.isEmbedding` `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange` `AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion` `AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange` `AlgebraicGeometry.IsOpenImmersion.comp` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `IsOpen.inter` `Continuous.isOpen_preimage` `continuous_fst` `TopologicalSpace.Opens.is_open'` `continuous_snd` `AlgebraicGeometry.Scheme.Cover.exists_eq` `AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage` `CategoryTheory.Limits.pullback.condition` `AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.exists_preimage_fst_triplet_of_prop` `AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition` `AlgebraicGeometry.isOpenImmersion_isStableUnderComposition` `isEmbedding_of_iSup_eq_top_of_preimage_subset_range` `Continuous.prodMk` `AlgebraicGeometry.Scheme.Hom.continuous` `AlgebraicGeometry.IsOpenImmersion.instFstScheme` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.IsPullback.instHasPullbackFst` `CategoryTheory.Category.assoc` `AlgebraicGeometry.IsOpenImmersion.mono` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.limit.lift_π_assoc` `AlgebraicGeometry.Scheme.local_affine` `AlgebraicGeometry.Scheme.Cover.pullbackHom_map`
`mono_of_injective` 📖	mathematical	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `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'`	`CategoryTheory.Mono` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory`	—	`CategoryTheory.Functor.mono_of_mono_map` `CategoryTheory.Functor.reflectsMonomorphisms_comp` `CategoryTheory.reflectsMonomorphisms_of_reflectsLimitsOfShape` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits` `CategoryTheory.Limits.fullyFaithful_reflectsLimits` `AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace` `AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace` `CategoryTheory.Functor.reflectsMonomorphisms_of_faithful` `AlgebraicGeometry.LocallyRingedSpace.instFaithfulSheafedSpaceCommRingCatForgetToSheafedSpace` `AlgebraicGeometry.SheafedSpace.mono_of_base_injective_of_stalk_epi` `CommRingCat.Colimits.hasColimits_commRingCat` `CommRingCat.hasLimits` `CommRingCat.forget_preservesLimits` `CommRingCat.FilteredColimits.forget_preservesFilteredColimits` `CommRingCat.forgetReflectIsos` `CategoryTheory.ConcreteCategory.epi_of_surjective` `AlgebraicGeometry.Scheme.Hom.stalkMap_surjective`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.SurjectiveOnStalks`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.Scheme.Hom.stalkMap_surjective` `Function.Surjective.of_comp` `AlgebraicGeometry.Scheme.Hom.stalkMap_comp`
`stableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.SurjectiveOnStalks`	—	`AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange` `instHasRingHomPropertySurjectiveOnStalks` `RingHom.PropertyIsLocal.respectsIso` `AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty` `RingHom.SurjectiveOnStalks.baseChange`
`stalkMap_surjective` 📖	mathematical	—	`CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.PresheafedSpace.presheaf` `DFunLike.coe` `TopCat.carrier` `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'` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `AlgebraicGeometry.Scheme.Hom.stalkMap`	—	—
`surj_on_stalks` 📖	mathematical	—	`CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.PresheafedSpace.presheaf` `DFunLike.coe` `TopCat.carrier` `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'` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `AlgebraicGeometry.Scheme.Hom.stalkMap`	—	`AlgebraicGeometry.Scheme.Hom.stalkMap_surjective`

---

← Back to Index