ClosedImmersion

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

Statistics

Metric	Count
Definitions IsClosedImmersion, overEquivIdealSheafData	2
Theorems SpecMap_residue, Spec_iff, Spec_map_residue, base_closed, comp, eq_inf, hasAffineProperty, iff_isPreimmersion, instIsAffineHom, instIsIsoSchemeToImage, instIsMultiplicativeScheme, instIsPreimmersion, instOfIsEmptyCarrierCarrierCommRingCat, instOfIsIsoScheme, instSubschemeι, isAffine_surjective_of_isAffine, isClosedEmbedding, isIso_iff_ker_eq_bot, isIso_lift, isIso_of_injective_of_isAffine, isIso_of_ker_eq, isStableUnderBaseChange, isZariskiLocalAtTarget, lift_fac, lift_fac_assoc, of_comp_isClosedImmersion, of_isPreimmersion, of_surjective_of_isAffine, respectsIso, spec_of_quotient_mk, spec_of_surjective, toSurjectiveOnStalks, app_surjective, isClosedEmbedding, instIsClosedImmersionFstScheme, instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat, instIsClosedImmersionMorphismRestrict, instIsClosedImmersionOfSubsingletonCarrierCarrierCommRingCatOfIsOver, instIsClosedImmersionSndScheme, instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat, instLocallyOfFiniteTypeOfIsClosedImmersion, isClosedImmersion_iff, isClosedImmersion_iff_isAffineHom, isClosedImmersion_of_comp_eq_id, isClosed_singleton_iff_isClosedImmersion, isDominant_of_of_appTop_injective, isIso_of_isClosedImmersion_of_surjective, stalkMap_injective_of_isOpenMap_of_injective	48
Total	50

AlgebraicGeometry

Definitions

Name	Category	Theorems
IsClosedImmersion 📖	CompData	51 math math: IsSeparated.isClosedImmersion_diagonal, IsSeparated.instIsClosedImmersionMapDescScheme, IsClosedImmersion.comp, Scheme.instIsClosedImmersionιOfIsSeparated, IsSeparated.instIsClosedImmersionLiftSchemeId, IsClosedImmersion.eq_proper_inf_monomorphisms, instHasOfPostcompPropertySchemeIsClosedImmersionIsSeparated, IsClosedImmersion.of_isPreimmersion, IsSeparated.isSeparated_eq_diagonal_isClosedImmersion, IsSeparated.diagonal_isClosedImmersion, IsClosedImmersion.respectsIso, instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, instIsClosedImmersionInclusion, IsClosedImmersion.instOfIsEmptyCarrierCarrierCommRingCat, isClosedImmersion_of_comp_eq_id, instIsClosedImmersionLiftCoborder, IsClosedImmersion.iff_isPreimmersion, instIsClosedImmersionSndScheme, IsClosedImmersion.comp_iff, IsClosedImmersion.of_surjective_of_isAffine, IsClosedImmersion.spec_of_quotient_mk, IsImmersion.isImmersion_iff_exists, isClosedImmersion_iff_isAffineHom, IsClosedImmersion.Spec_map_residue, IsClosedImmersion.isStableUnderBaseChange, isSeparated_iff, IsClosedImmersion.instIsMultiplicativeScheme, instIsClosedImmersionOfSubsingletonCarrierCarrierCommRingCatOfIsOver, IsClosedImmersion.iff_isFinite_and_mono, IsClosedImmersion.hasAffineProperty, IsClosedImmersion.spec_of_surjective, IsClosedImmersion.eq_inf, IsClosedImmersion.Spec_iff, Scheme.isSeparated_iff_isClosedImmersion_prod_lift, IsClosedImmersion.instOfIsIsoScheme, IsClosedImmersion.eq_isFinite_inf_mono, isClosedImmersion_equalizer_ι_left, isClosed_singleton_iff_isClosedImmersion, IsClosedImmersion.iff_isProper_and_mono, instIsClosedImmersionMorphismRestrict, instIsClosedImmersionFstScheme, isClosedImmersion_iff, IsClosedImmersion.isZariskiLocalAtTarget, instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat, IsClosedImmersion.SpecMap_residue, Scheme.instIsClosedImmersionLiftIdOfIsSeparated, IsImmersion.isImmersion_iff_exists_of_quasiCompact, IsClosedImmersion.of_comp, isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange, IsClosedImmersion.instSubschemeι, IsClosedImmersion.of_comp_isClosedImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsClosedImmersionFstScheme 📖	mathematical	—	IsClosedImmersion CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange IsClosedImmersion.isStableUnderBaseChange
instIsClosedImmersionISchemeOfSubsingletonCarrierCarrierCommRingCat 📖	mathematical	—	IsClosedImmersion CategoryTheory.Retract.i Scheme Scheme.instCategory	—	isClosedImmersion_of_comp_eq_id CategoryTheory.Retract.retract
instIsClosedImmersionMorphismRestrict 📖	mathematical	—	IsClosedImmersion Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict	—	IsZariskiLocalAtTarget.restrict IsClosedImmersion.isZariskiLocalAtTarget
instIsClosedImmersionOfSubsingletonCarrierCarrierCommRingCatOfIsOver 📖	mathematical	—	IsClosedImmersion	—	isClosedImmersion_of_comp_eq_id CategoryTheory.comp_over
instIsClosedImmersionSndScheme 📖	mathematical	—	IsClosedImmersion CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange IsClosedImmersion.isStableUnderBaseChange
instIsDominantToSpecΓOfCompactSpaceCarrierCarrierCommRingCat 📖	mathematical	—	IsDominant Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Scheme.toSpecΓ	—	isDominant_of_of_appTop_injective isAffine_Spec Scheme.toSpecΓ_appTop CategoryTheory.ConcreteCategory.bijective_of_isIso CategoryTheory.Iso.isIso_hom
instLocallyOfFiniteTypeOfIsClosedImmersion 📖	mathematical	—	LocallyOfFiniteType	—	HasRingHomProperty.eq_affineLocally instHasRingHomPropertyLocallyOfFiniteTypeFiniteType IsClosedImmersion.instIsAffineHom targetAffineLocally_affineAnd_iff_affineLocally RingHom.finiteType_isLocal targetAffineLocally_affineAnd_le RingHom.FiniteType.of_surjective HasAffineProperty.eq_targetAffineLocally IsClosedImmersion.hasAffineProperty
isClosedImmersion_iff 📖	mathematical	—	IsClosedImmersion SurjectiveOnStalks Topology.IsClosedEmbedding 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'	—	—
isClosedImmersion_iff_isAffineHom 📖	mathematical	—	IsClosedImmersion IsAffineHom 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' DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.app	—	HasAffineProperty.eq_targetAffineLocally IsClosedImmersion.hasAffineProperty targetAffineLocally_affineAnd_iff' RingHom.surjective_respectsIso
isClosedImmersion_of_comp_eq_id 📖	mathematical	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory CategoryTheory.CategoryStruct.id	IsClosedImmersion	—	Spec.map_surjective IsClosedImmersion.spec_of_surjective Function.LeftInverse.surjective Spec.map_injective Spec.map_id Spec.map_comp Function.Injective.subsingleton instIsAffineOfFiniteOfDiscreteTopologyCarrierCarrierCommRingCat Finite.of_subsingleton Subsingleton.discreteTopology CategoryTheory.Iso.isIso_inv Homeomorph.injective CategoryTheory.MorphismProperty.cancel_left_of_respectsIso IsClosedImmersion.respectsIso CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Iso.inv_hom_id Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange Scheme.instIsJointlySurjectivePreservingIsOpenImmersion isOpenImmersion_stableUnderBaseChange Scheme.Pullback.instHasPullback IsZariskiLocalAtTarget.iff_of_openCover IsClosedImmersion.isZariskiLocalAtTarget Scheme.instIsOpenImmersionF Scheme.Cover.pullbackHom.eq_1 CategoryTheory.IsPullback.flip IsOpenImmersion.isPullback_lift_id CategoryTheory.IsPullback.isoPullback_inv_snd IsOpenImmersion.lift_fac_assoc Scheme.local_affine Scheme.isEmpty_pullback Set.subset_compl_iff_disjoint_left IsClosedImmersion.instOfIsEmptyCarrierCarrierCommRingCat
isClosed_singleton_iff_isClosedImmersion 📖	mathematical	—	IsClosed TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier Set Set.instSingletonSet IsClosedImmersion Spec Scheme.residueField Scheme.fromSpecResidueField	—	Scheme.range_fromSpecResidueField IsClosedImmersion.of_isPreimmersion Scheme.instIsPreimmersionFromSpecResidueField Topology.IsClosedEmbedding.isClosed_range Scheme.Hom.isClosedEmbedding
isDominant_of_of_appTop_injective 📖	mathematical	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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.appTop	IsDominant	—	HasAffineProperty.iff_of_isAffine instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat Scheme.IdealSheafData.ext_of_isAffine isAffineOpen_top RingHom.instRingHomClass Scheme.Hom.ker_apply Scheme.Hom.support_ker
isIso_of_isClosedImmersion_of_surjective 📖	mathematical	—	CategoryTheory.IsIso Scheme Scheme.instCategory	—	IsClosedImmersion.isIso_iff_ker_eq_bot Scheme.IdealSheafData.support_eq_top_iff SetLike.coe_injective Scheme.Hom.support_ker instQuasiCompactOfIsAffineHom IsClosedImmersion.instIsAffineHom range_eq_univ IsClosed.closure_eq
stalkMap_injective_of_isOpenMap_of_injective 📖	mathematical	IsOpenMap 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' CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder PresheafedSpace.presheaf Opposite.op Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier Scheme.Hom.appTop	TopCat.Presheaf.stalk CommRingCat.Colimits.hasColimits_commRingCat Scheme.Hom.stalkMap	—	stalkMap_injective_of_isAffine CommRingCat.Colimits.hasColimits_commRingCat RingedSpace.exists_res_eq_zero_of_germ_eq_zero Scheme.Hom.germ_stalkMap_apply TopCat.Presheaf.Γgerm.eq_1 TopologicalSpace.Opens.is_open' TopologicalSpace.Opens.isBasis_iff_nbhd isBasis_basicOpen Scheme.preimage_basicOpen_top Scheme.Hom.comp_base TopologicalSpace.Opens.map_comp_obj Scheme.Hom.preimage_mono le_trans le_of_eq Set.image_congr IsOpen.preimage ContinuousMap.continuous Set.preimage_image_eq LE.le.trans Scheme.Hom.appLE_map le_rfl Scheme.Hom.map_appLE CommRingCat.comp_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass exists_of_res_zero_of_qcqs_of_top Scheme.compactSpace_of_isAffine instIsAffineXSchemeFiniteSubcover Scheme.isAffine_affineCover quasiSeparatedSpace_of_isAffine map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass pow_mul_eq_zero_of_le Finset.le_sup Finset.mem_univ germ_eq_zero_of_pow_mul_eq_zero RingHom.ker_eq_bot_iff_eq_zero RingHom.injective_iff_ker_eq_bot Scheme.zero_of_zero_cover

AlgebraicGeometry.IsClosedImmersion

Definitions

Name	Category	Theorems
overEquivIdealSheafData 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecMap_residue 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField 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 AlgebraicGeometry.Spec.map AlgebraicGeometry.Scheme.residue	—	spec_of_surjective CommRingCat.Colimits.hasColimits_commRingCat Ideal.Quotient.mk_surjective
Spec_iff 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.Spec CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CommRingCat.of HasQuotient.Quotient CommRingCat.carrier Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Ideal.instHasQuotient_1 Ideal.Quotient.commRing CategoryTheory.Iso.hom AlgebraicGeometry.Spec.map CommRingCat.ofHom CommRing.toRing Ideal.instIsTwoSided_1	—	Ideal.instIsTwoSided_1 isAffine_surjective_of_isAffine AlgebraicGeometry.isAffine_Spec RingHom.instRingHomClass RingHom.instIsTwoSidedKer RingHomClass.toNonUnitalRingHomClass RingHom.kerLift_injective Ideal.Quotient.lift_surjective_of_surjective RingEquiv.surjective CategoryTheory.Category.assoc AlgebraicGeometry.Spec.map_comp CategoryTheory.Iso.inv_hom_id AlgebraicGeometry.Spec.map_id CategoryTheory.Category.comp_id comp instOfIsIsoScheme CategoryTheory.Iso.isIso_hom
Spec_map_residue 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.residueField 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 AlgebraicGeometry.Spec.map AlgebraicGeometry.Scheme.residue	—	SpecMap_residue
base_closed 📖	mathematical	—	Topology.IsClosedEmbedding 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.isClosedEmbedding
comp 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeScheme
eq_inf 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra AlgebraicGeometry.topologically Topology.IsClosedEmbedding AlgebraicGeometry.SurjectiveOnStalks	—	AlgebraicGeometry.isClosedImmersion_iff
hasAffineProperty 📖	mathematical	—	AlgebraicGeometry.HasAffineProperty AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.IsAffine 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 DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop	—	of_surjective_of_isAffine isAffine_surjective_of_isAffine AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget isZariskiLocalAtTarget
iff_isPreimmersion 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.IsPreimmersion IsClosed TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set.range 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.isClosedImmersion_iff AlgebraicGeometry.isPreimmersion_iff Topology.isClosedEmbedding_iff
instIsAffineHom 📖	mathematical	—	AlgebraicGeometry.IsAffineHom	—	AlgebraicGeometry.isAffineHom_of_isInducing Topology.IsClosedEmbedding.isInducing AlgebraicGeometry.Scheme.Hom.isClosedEmbedding Topology.IsClosedEmbedding.isClosed_range
instIsIsoSchemeToImage 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Hom.image AlgebraicGeometry.Scheme.Hom.toImage	—	of_comp_isClosedImmersion instSubschemeι AlgebraicGeometry.Scheme.Hom.toImage_imageι isHomeomorph_iff_isEmbedding_surjective AlgebraicGeometry.Scheme.Hom.isEmbedding instIsPreimmersion Set.range_eq_univ IsClosed.closure_eq Topology.IsClosedEmbedding.isClosed_range AlgebraicGeometry.Scheme.Hom.isClosedEmbedding Dense.closure_eq AlgebraicGeometry.Scheme.Hom.denseRange AlgebraicGeometry.Scheme.instIsDominantToImageOfQuasiCompact AlgebraicGeometry.instQuasiCompactOfIsAffineHom instIsAffineHom Eq.ge AlgebraicGeometry.isomorphisms_eq_stalkwise CategoryTheory.Iso.isIso_hom CommRingCat.Colimits.hasColimits_commRingCat TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing Topology.IsEmbedding.isInducing CategoryTheory.ConcreteCategory.isIso_iff_bijective CommRingCat.forgetReflectIsos AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective AlgebraicGeometry.Scheme.Hom.stalkMap_surjective toSurjectiveOnStalks
instIsMultiplicativeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsClosedImmersion	—	instOfIsIsoScheme CategoryTheory.IsIso.id AlgebraicGeometry.SurjectiveOnStalks.comp toSurjectiveOnStalks Topology.IsClosedEmbedding.comp AlgebraicGeometry.Scheme.Hom.isClosedEmbedding
instIsPreimmersion 📖	mathematical	—	AlgebraicGeometry.IsPreimmersion	—	iff_isPreimmersion
instOfIsEmptyCarrierCarrierCommRingCat 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion	—	of_isPreimmersion AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion AlgebraicGeometry.isOpenImmersion_of_isEmpty Set.range_eq_empty isClosed_empty
instOfIsIsoScheme 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion	—	CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.ConcreteCategory.bijective_of_isIso AlgebraicGeometry.IsOpenImmersion.instIsIsoCommRingCatStalkMap AlgebraicGeometry.IsOpenImmersion.of_isIso Homeomorph.isClosedEmbedding AlgebraicGeometry.Scheme.Hom.isIso_base
instSubschemeι 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.Scheme.IdealSheafData.subscheme AlgebraicGeometry.Scheme.IdealSheafData.subschemeι	—	of_isPreimmersion AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionSubschemeι TopologicalSpace.Closeds.isClosed AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι
isAffine_surjective_of_isAffine 📖	mathematical	—	AlgebraicGeometry.IsAffine 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 DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop	—	AlgebraicGeometry.isAffine_of_isAffineHom instIsAffineHom AlgebraicGeometry.Scheme.Hom.toImage_imageι AlgebraicGeometry.Scheme.Hom.appTop.eq_1 AlgebraicGeometry.isAffineOpen_top Ideal.instIsTwoSided_1 AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app CommRingCat.hom_comp RingHom.coe_comp CategoryTheory.ConcreteCategory.bijective_of_isIso AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp instIsIsoSchemeToImage CategoryTheory.Iso.isIso_inv Ideal.Quotient.mk_surjective
isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding 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'	—	—
isIso_iff_ker_eq_bot 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Hom.ker Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder AlgebraicGeometry.Scheme.IdealSheafData.instOrderBot	—	AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData CategoryTheory.IsIso.comp_isIso instIsIsoSchemeToImage AlgebraicGeometry.Scheme.Hom.toImage_imageι
isIso_lift 📖	mathematical	AlgebraicGeometry.Scheme.Hom.ker	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory lift Eq.le AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder	—	isIso_of_ker_eq Eq.le lift_fac
isIso_of_injective_of_isAffine 📖	mathematical	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 DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory	—	isIso_iff_ker_eq_bot AlgebraicGeometry.Scheme.IdealSheafData.ext_of_isAffine AlgebraicGeometry.isAffineOpen_top RingHom.instRingHomClass AlgebraicGeometry.Scheme.Hom.ker_apply AlgebraicGeometry.instQuasiCompactOfIsAffineHom instIsAffineHom
isIso_of_ker_eq 📖	mathematical	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Hom.ker	CategoryTheory.IsIso	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor Eq.le CategoryTheory.Over.forget_reflects_iso CategoryTheory.MorphismProperty.instFullOverTopOverForget CategoryTheory.MorphismProperty.instFaithfulOverTopOverForget CategoryTheory.isIso_op_iff
isStableUnderBaseChange 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsClosedImmersion	—	AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange hasAffineProperty AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso AlgebraicGeometry.HasAffineProperty.isLocal_affineProperty AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.instIsAffinePullbackSchemeOfIsAffineHom_1 AlgebraicGeometry.isAffineHom_of_isAffine RingHom.IsStableUnderBaseChange.pullback_fst_appTop RingHom.surjective_isStableUnderBaseChange RingHom.surjective_respectsIso
isZariskiLocalAtTarget 📖	mathematical	—	AlgebraicGeometry.IsZariskiLocalAtTarget AlgebraicGeometry.IsClosedImmersion	—	CategoryTheory.MorphismProperty.IsLocalAtTarget.inf AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion AlgebraicGeometry.isClosedEmbedding_isZariskiLocalAtTarget AlgebraicGeometry.SurjectiveOnStalks.instIsZariskiLocalAtTarget eq_inf
lift_fac 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder AlgebraicGeometry.Scheme.Hom.ker	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory lift	—	AlgebraicGeometry.Scheme.Hom.toImage_imageι instIsIsoSchemeToImage CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id_assoc AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeι
lift_fac_assoc 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder AlgebraicGeometry.Scheme.Hom.ker	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory lift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fac
of_comp_isClosedImmersion 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.Scheme.Hom.stalkMap_surjective toSurjectiveOnStalks Function.Surjective.of_comp AlgebraicGeometry.Scheme.Hom.stalkMap_comp AlgebraicGeometry.Scheme.Hom.isClosedEmbedding Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap AlgebraicGeometry.Scheme.Hom.continuous Function.Injective.of_comp Topology.IsEmbedding.injective Topology.IsClosedEmbedding.toIsEmbedding Topology.IsClosedEmbedding.isClosed_iff_image_isClosed Set.image_comp Topology.IsClosedEmbedding.isClosedMap
of_isPreimmersion 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion	—	iff_isPreimmersion
of_surjective_of_isAffine 📖	mathematical	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 DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop	AlgebraicGeometry.IsClosedImmersion	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff respectsIso spec_of_surjective
respectsIso 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsClosedImmersion	—	comp instOfIsIsoScheme CategoryTheory.Iso.isIso_hom
spec_of_quotient_mk 📖	mathematical	—	AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.Spec CommRingCat.of HasQuotient.Quotient CommRingCat.carrier Ideal Ring.toSemiring CommRing.toRing CommRingCat.commRing Ideal.instHasQuotient Ideal.Quotient.commRing AlgebraicGeometry.Spec.map CommRingCat.ofHom Ideal.instIsTwoSided_1	—	spec_of_surjective Ideal.instIsTwoSided_1 Ideal.Quotient.mk_surjective
spec_of_surjective 📖	mathematical	CommRingCat.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom CommRingCat CommRingCat.instCategory RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier	AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.Spec AlgebraicGeometry.Spec.map	—	CommRingCat.Colimits.hasColimits_commRingCat PrimeSpectrum.isPrime CategoryTheory.MorphismProperty.arrow_mk_iso_iff RingHom.toMorphismProperty_respectsIso_iff RingHom.surjective_respectsIso RingHom.surjective_localRingHom_of_surjective PrimeSpectrum.isClosedEmbedding_comap_of_surjective
toSurjectiveOnStalks 📖	mathematical	—	AlgebraicGeometry.SurjectiveOnStalks	—	—

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_surjective 📖	mathematical	—	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' DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier app	—	AlgebraicGeometry.isClosedImmersion_iff_isAffineHom
isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding 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.IsClosedImmersion.isClosedEmbedding

---

← Back to Index