Documentation Verification Report

OpenImmersion

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

Statistics

Metric	Count
Definitions	0
Theorems `of_forall_source_exists`, `of_openCover_source`, `instIsOpenImmersionMapScheme`, `instIsZariskiLocalAtTargetStalkwiseBijectiveCoeRingHom`, `isOpenImmersion_SpecMap_iff_of_surjective`, `isOpenImmersion_eq_inf`, `isOpenImmersion_iff_stalk`, `isOpenImmersion_isZariskiLocalAtTarget`	8
Total	8

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsOpenImmersionMapScheme` 📖	mathematical	—	`IsOpenImmersion` `CategoryTheory.Limits.coprod` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.pair` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.Limits.coprod.map`	—	`IsZariskiLocalAtTarget.coprodMap` `isOpenImmersion_isZariskiLocalAtTarget`
`instIsZariskiLocalAtTargetStalkwiseBijectiveCoeRingHom` 📖	mathematical	—	`IsZariskiLocalAtTarget` `stalkwise` `Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`stalkwiseIsZariskiLocalAtTarget_of_respectsIso` `RingHom.toMorphismProperty_respectsIso_iff` `CategoryTheory.MorphismProperty.ext` `CategoryTheory.ConcreteCategory.isIso_iff_bijective` `CommRingCat.forgetReflectIsos` `CategoryTheory.MorphismProperty.RespectsIso.isomorphisms`
`isOpenImmersion_SpecMap_iff_of_surjective` 📖	mathematical	`CommRingCat.carrier` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.Hom.hom`	`IsOpenImmersion` `Spec` `Spec.map` `IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `RingHom.ker` `RingHom.instRingHomClass` `Ideal.span` `Set` `Set.instSingletonSet`	—	`RingHom.instRingHomClass` `PrimeSpectrum.isClopen_iff_zeroLocus` `PrimeSpectrum.isClosed_range_comap_of_surjective` `Topology.IsOpenEmbedding.isOpen_range` `Scheme.Hom.isOpenEmbedding` `Ideal.instIsTwoSided_1` `IsLocalization.away_of_isIdempotentElem` `IsIdempotentElem.one_sub` `Ideal.mk_ker` `sub_sub_cancel` `Ideal.Quotient.mk_surjective` `IsOpenImmersion.of_isLocalization` `range_comap_of_surjective` `PrimeSpectrum.zeroLocus_span` `Spec.full` `Spec.faithful` `CategoryTheory.ConcreteCategory.bijective_of_isIso` `CategoryTheory.Iso.isIso_inv` `Spec.map_injective` `Spec.map_comp` `CategoryTheory.Functor.map_preimage` `IsOpenImmersion.isoOfRangeEq_inv_fac` `CommRingCat.hom_comp` `RingHom.ker_eq_comap_bot` `Ideal.comap_comap` `RingHom.injective_iff_ker_eq_bot`
`isOpenImmersion_eq_inf` 📖	mathematical	—	`IsOpenImmersion` `CategoryTheory.MorphismProperty` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `topologically` `Topology.IsOpenEmbedding` `stalkwise` `Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	—	`CategoryTheory.MorphismProperty.ext` `CommRingCat.Colimits.hasColimits_commRingCat` `IsOpenImmersion.iff_isIso_stalkMap` `CategoryTheory.ConcreteCategory.isIso_iff_bijective` `CommRingCat.forgetReflectIsos`
`isOpenImmersion_iff_stalk` 📖	mathematical	—	`IsOpenImmersion` `Topology.IsOpenEmbedding` `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'` `CategoryTheory.IsIso` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `PresheafedSpace.presheaf` `Scheme.Hom.stalkMap`	—	`IsOpenImmersion.iff_isIso_stalkMap`
`isOpenImmersion_isZariskiLocalAtTarget` 📖	mathematical	—	`IsZariskiLocalAtTarget` `IsOpenImmersion`	—	`CategoryTheory.MorphismProperty.IsLocalAtTarget.inf` `Scheme.instHasPullbacksPrecoverageOfHasPullbacks` `Scheme.instHasPullbacksIsOpenImmersion` `isOpenEmbedding_isZariskiLocalAtTarget` `instIsZariskiLocalAtTargetStalkwiseBijectiveCoeRingHom` `isOpenImmersion_eq_inf`

AlgebraicGeometry.IsOpenImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_forall_source_exists` 📖	—	`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'` `AlgebraicGeometry.Scheme.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `AlgebraicGeometry.Scheme.Hom.opensRange` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	—	`CategoryTheory.Presieve.map_ofArrows` `of_openCover_source`
`of_openCover_source` 📖	—	`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'` `AlgebraicGeometry.IsOpenImmersion` `CategoryTheory.PreZeroHypercover.X` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `AlgebraicGeometry.Scheme.precoverage` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.PreZeroHypercover.f`	—	—	`CommRingCat.Colimits.hasColimits_commRingCat` `iff_isIso_stalkMap` `Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap` `AlgebraicGeometry.Scheme.Hom.continuous` `Set.ext` `AlgebraicGeometry.Scheme.Cover.exists_eq` `AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage` `IsOpen.preimage` `ContinuousMap.continuous` `isOpen_iUnion` `TopologicalSpace.Opens.is_open'` `Set.image_congr` `instIsIsoCommRingCatStalkMap` `AlgebraicGeometry.Scheme.instIsOpenImmersionF` `CategoryTheory.IsIso.comp_inv_eq` `AlgebraicGeometry.Scheme.Hom.stalkMap_comp` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.IsIso.inv_isIso`

---

← Back to Index