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 CommRingCat.carrier IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRingCat.commRing RingHom.ker RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.instRingHomClass CommRingCat.Hom.hom 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 📖	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' AlgebraicGeometry.Scheme Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensRange CategoryTheory.CategoryStruct.comp	AlgebraicGeometry.IsOpenImmersion	—	CategoryTheory.Presieve.map_ofArrows of_openCover_source
of_openCover_source 📖	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' 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	AlgebraicGeometry.IsOpenImmersion	—	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