Immersion

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

Statistics

Metric	Count
Definitions IsImmersion, coborderRange, liftCoborder	3
Theorems comp, comp_iff, instDiagonalScheme, instFstScheme, instHasOfPostcompPropertySchemeTopMorphismProperty, instIsMultiplicativeScheme, instIsOpenImmersionToImageOfQuasiCompact, instIsZariskiLocalAtTarget, instLiftSchemeId, instLocallyOfFiniteType, instMapDescScheme, instMorphismRestrict, instOfIsClosedImmersion, instOfIsOpenImmersion, instResLE, instSndScheme, instToImage, instιScheme, isImmersion_iff_exists, isImmersion_iff_exists_of_quasiCompact, isLocallyClosed_range, isPullback_toImage_liftCoborder, isStableUnderBaseChange, of_comp, toIsPreimmersion, isLocallyClosed_range, liftCoborder_preimage, liftCoborder_ι, liftCoborder_ι_assoc, instIsClosedImmersionLiftCoborder, instIsDominantιCoborderRange, isImmersion_eq_inf, isImmersion_iff, liftCoborder_app	34
Total	37

AlgebraicGeometry

Definitions

Name	Category	Theorems
IsImmersion 📖	CompData	23 math math: IsImmersion.instOfIsClosedImmersion, IsImmersion.isStableUnderBaseChange, Scheme.IsQuasiAffine.toIsImmersion, isImmersion_eq_inf, IsImmersion.comp, IsImmersion.instιScheme, IsImmersion.instMorphismRestrict, IsImmersion.instResLE, IsImmersion.instMapDescScheme, IsImmersion.instIsZariskiLocalAtTarget, IsImmersion.instDiagonalScheme, IsImmersion.isImmersion_iff_exists, IsImmersion.instIsMultiplicativeScheme, isImmersion_iff, IsImmersion.instFstScheme, IsImmersion.instOfIsOpenImmersion, IsImmersion.instToImage, IsImmersion.instHasOfPostcompPropertySchemeTopMorphismProperty, IsImmersion.of_comp, IsImmersion.instLiftSchemeId, IsImmersion.instSndScheme, IsImmersion.isImmersion_iff_exists_of_quasiCompact, IsImmersion.comp_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsClosedImmersionLiftCoborder 📖	mathematical	—	IsClosedImmersion Scheme.Opens.toScheme Scheme.Hom.coborderRange Scheme.Hom.liftCoborder	—	Scheme.Hom.liftCoborder_ι IsImmersion.toIsPreimmersion IsPreimmersion.of_comp IsPreimmersion.instOfIsOpenImmersion Scheme.Opens.instIsOpenImmersionι IsClosedImmersion.of_isPreimmersion Set.image_injective Topology.IsEmbedding.injective Scheme.Hom.isEmbedding Set.range_comp TopCat.coe_comp Scheme.Hom.comp_base Set.image_preimage_eq_of_subset Scheme.Opens.range_ι subset_coborder isClosed_preimage_val_coborder
instIsDominantιCoborderRange 📖	mathematical	—	IsDominant Scheme.Opens.toScheme Scheme.Hom.coborderRange Scheme.Opens.ι	—	isDominant_iff DenseRange.eq_1 Scheme.Opens.range_ι dense_coborder
isImmersion_eq_inf 📖	mathematical	—	IsImmersion CategoryTheory.MorphismProperty Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra IsPreimmersion topologically IsLocallyClosed Set.range	—	isImmersion_iff
isImmersion_iff 📖	mathematical	—	IsImmersion IsPreimmersion IsLocallyClosed TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace SheafedSpace.instTopologicalSpaceCarrierCarrier Set.range DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom'	—	—
liftCoborder_app 📖	mathematical	—	Scheme.Hom.app Scheme.Opens.toScheme Scheme.Hom.coborderRange Scheme.Hom.liftCoborder CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier 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 Scheme.Hom.opensFunctor Scheme.Opens.ι Scheme.Opens.instIsOpenImmersionι TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.eqToHom Scheme.Hom.liftCoborder_preimage	—	Scheme.Opens.instIsOpenImmersionι Scheme.Hom.liftCoborder_preimage Scheme.Hom.liftCoborder_ι Scheme.Hom.congr_app Scheme.Hom.preimage_image_eq Set.image_preimage_subset Scheme.Hom.app_eq CategoryTheory.eqToHom_op CategoryTheory.eqToHom_unop CategoryTheory.subsingleton_of_unop Preorder.subsingleton_hom CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.eqToHom_map_comp CategoryTheory.Category.comp_id

AlgebraicGeometry.IsImmersion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	AlgebraicGeometry.IsImmersion 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.IsImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	of_comp comp
instDiagonalScheme 📖	mathematical	—	AlgebraicGeometry.IsImmersion CategoryTheory.Limits.pullback.diagonalObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.diagonal	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback top_le_iff AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange AlgebraicGeometry.Scheme.isAffine_affineCover comp instOfIsClosedImmersion instOfIsOpenImmersion AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion instIsZariskiLocalAtTarget CategoryTheory.Iso.isIso_hom AlgebraicGeometry.Scheme.topIso_hom AlgebraicGeometry.morphismRestrict_ι
instFstScheme 📖	mathematical	—	AlgebraicGeometry.IsImmersion 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 isStableUnderBaseChange
instHasOfPostcompPropertySchemeTopMorphismProperty 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsImmersion Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal isStableUnderBaseChange instIsMultiplicativeScheme CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop instDiagonalScheme
instIsMultiplicativeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsImmersion	—	instOfIsClosedImmersion AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme CategoryTheory.IsIso.id AlgebraicGeometry.IsPreimmersion.comp toIsPreimmersion Set.range_comp IsLocallyClosed.image AlgebraicGeometry.Scheme.Hom.isLocallyClosed_range Topology.IsEmbedding.isInducing AlgebraicGeometry.Scheme.Hom.isEmbedding
instIsOpenImmersionToImageOfQuasiCompact 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.Scheme.Hom.image AlgebraicGeometry.Scheme.Hom.toImage	—	CategoryTheory.MorphismProperty.of_isPullback AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange CategoryTheory.IsPullback.flip isPullback_toImage_liftCoborder AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι
instIsZariskiLocalAtTarget 📖	mathematical	—	AlgebraicGeometry.IsZariskiLocalAtTarget AlgebraicGeometry.IsImmersion	—	AlgebraicGeometry.topologically_isZariskiLocalAtTarget' Set.range_comp Set.range_eq_univ AlgebraicGeometry.Scheme.Hom.surjective AlgebraicGeometry.instSurjectiveOfIsIsoScheme Set.image_univ IsLocallyClosed.image Homeomorph.isInducing IsOpen.isLocallyClosed isOpen_univ Set.range_restrictPreimage TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage CategoryTheory.MorphismProperty.IsLocalAtTarget.inf AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion AlgebraicGeometry.IsPreimmersion.instIsZariskiLocalAtTarget AlgebraicGeometry.isImmersion_eq_inf
instLiftSchemeId 📖	mathematical	—	AlgebraicGeometry.IsImmersion CategoryTheory.Limits.prod AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts AlgebraicGeometry.instCartesianMonoidalCategoryScheme Finite.of_fintype CategoryTheory.Limits.fintypeWalkingPair CategoryTheory.Limits.pair CategoryTheory.Limits.prod.lift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype AlgebraicGeometry.instHasTerminalScheme AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion instIsZariskiLocalAtTarget CategoryTheory.Iso.isIso_hom AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.hom_ext CategoryTheory.Category.assoc prodIsoPullback_hom_fst CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.pullback.diagonal_fst prodIsoPullback_hom_snd CategoryTheory.Limits.pullback.diagonal_snd instDiagonalScheme
instLocallyOfFiniteType 📖	mathematical	—	AlgebraicGeometry.LocallyOfFiniteType	—	AlgebraicGeometry.Scheme.Hom.liftCoborder_ι AlgebraicGeometry.locallyOfFiniteType_comp AlgebraicGeometry.instLocallyOfFiniteTypeOfIsClosedImmersion AlgebraicGeometry.instIsClosedImmersionLiftCoborder AlgebraicGeometry.locallyOfFiniteType_of_isOpenImmersion AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι
instMapDescScheme 📖	mathematical	—	AlgebraicGeometry.IsImmersion CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.pullback.mapDesc	—	CategoryTheory.MorphismProperty.of_isPullback isStableUnderBaseChange AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.comp_id CategoryTheory.Limits.pullback_map_diagonal_isPullback AlgebraicGeometry.Scheme.Pullback.instHasPullbacks instDiagonalScheme
instMorphismRestrict 📖	mathematical	—	AlgebraicGeometry.IsImmersion 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
instOfIsClosedImmersion 📖	mathematical	—	AlgebraicGeometry.IsImmersion	—	AlgebraicGeometry.IsClosedImmersion.instIsPreimmersion IsClosed.isLocallyClosed Topology.IsClosedEmbedding.isClosed_range AlgebraicGeometry.Scheme.Hom.isClosedEmbedding
instOfIsOpenImmersion 📖	mathematical	—	AlgebraicGeometry.IsImmersion	—	AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion IsOpen.isLocallyClosed Topology.IsOpenEmbedding.isOpen_range AlgebraicGeometry.Scheme.Hom.isOpenEmbedding
instResLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	AlgebraicGeometry.IsImmersion AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Hom.resLE	—	comp instOfIsOpenImmersion AlgebraicGeometry.instIsOpenImmersionHomOfLE instMorphismRestrict
instSndScheme 📖	mathematical	—	AlgebraicGeometry.IsImmersion 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 isStableUnderBaseChange
instToImage 📖	mathematical	—	AlgebraicGeometry.IsImmersion AlgebraicGeometry.Scheme.Hom.image AlgebraicGeometry.Scheme.Hom.toImage	—	AlgebraicGeometry.Scheme.Hom.toImage_imageι of_comp
instιScheme 📖	mathematical	—	AlgebraicGeometry.IsImmersion CategoryTheory.Limits.equalizer AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits AlgebraicGeometry.instHasFiniteLimitsScheme CategoryTheory.Limits.instFinCategoryWalkingParallelPair CategoryTheory.Limits.parallelPair CategoryTheory.Limits.equalizer.ι	—	CategoryTheory.MorphismProperty.of_isPullback isStableUnderBaseChange CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits AlgebraicGeometry.instHasFiniteLimitsScheme CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype CategoryTheory.IsPullback.flip CategoryTheory.Limits.isPullback_equalizer_prod instLiftSchemeId
isImmersion_iff_exists 📖	mathematical	—	AlgebraicGeometry.IsImmersion AlgebraicGeometry.IsClosedImmersion AlgebraicGeometry.IsOpenImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	AlgebraicGeometry.instIsClosedImmersionLiftCoborder AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι AlgebraicGeometry.Scheme.Hom.liftCoborder_ι comp instOfIsClosedImmersion instOfIsOpenImmersion
isImmersion_iff_exists_of_quasiCompact 📖	mathematical	—	AlgebraicGeometry.IsImmersion AlgebraicGeometry.IsOpenImmersion AlgebraicGeometry.IsClosedImmersion CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	instIsOpenImmersionToImageOfQuasiCompact AlgebraicGeometry.IsClosedImmersion.instSubschemeι AlgebraicGeometry.Scheme.Hom.toImage_imageι comp instOfIsOpenImmersion instOfIsClosedImmersion
isLocallyClosed_range 📖	mathematical	—	IsLocallyClosed 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'	—	—
isPullback_toImage_liftCoborder 📖	mathematical	—	CategoryTheory.IsPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Hom.image AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Hom.coborderRange AlgebraicGeometry.Scheme.Hom.toImage AlgebraicGeometry.Scheme.Hom.liftCoborder AlgebraicGeometry.Scheme.Hom.imageι AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.IsPullback.flip AlgebraicGeometry.isPullback_of_isClosedImmersion AlgebraicGeometry.instIsClosedImmersionLiftCoborder AlgebraicGeometry.IsClosedImmersion.instSubschemeι AlgebraicGeometry.Scheme.Hom.liftCoborder_ι AlgebraicGeometry.Scheme.Hom.toImage_imageι AlgebraicGeometry.Scheme.Hom.imageι.eq_1 AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι AlgebraicGeometry.Scheme.IdealSheafData.ext AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι RingHom.instRingHomClass AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersion Ideal.comap.congr_simp AlgebraicGeometry.Scheme.Opens.ι_appIso AlgebraicGeometry.Scheme.Hom.ker_apply RingHom.comap_ker AlgebraicGeometry.instQuasiCompactOfIsAffineHom AlgebraicGeometry.IsClosedImmersion.instIsAffineHom RingHomCompTriple.comp_eq RingHomCompTriple.ids AlgebraicGeometry.Scheme.Hom.liftCoborder_preimage AlgebraicGeometry.liftCoborder_app CommRingCat.hom_comp RingHom.ker_comp_of_injective CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CommRingCat.forget_preservesLimits CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.instIsSplitMonoMap CategoryTheory.instIsSplitMonoOppositeOpOfIsSplitEpi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.instIsIsoEqToHom
isStableUnderBaseChange 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsImmersion	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Hom.liftCoborder_ι CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq CategoryTheory.IsPullback.paste_horiz_iff CategoryTheory.IsPullback.of_hasPullback CategoryTheory.Limits.pullback.lift_snd CategoryTheory.Limits.limit.lift_π CategoryTheory.IsPullback.flip CategoryTheory.MorphismProperty.of_isPullback AlgebraicGeometry.IsClosedImmersion.isStableUnderBaseChange AlgebraicGeometry.instIsClosedImmersionLiftCoborder CategoryTheory.Limits.pullback.lift_fst comp instOfIsClosedImmersion instOfIsOpenImmersion AlgebraicGeometry.IsOpenImmersion.instFstScheme AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι
of_comp 📖	mathematical	—	AlgebraicGeometry.IsImmersion	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_postcomp instHasOfPostcompPropertySchemeTopMorphismProperty
toIsPreimmersion 📖	mathematical	—	AlgebraicGeometry.IsPreimmersion	—	—

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
coborderRange 📖	CompOp	7 math math: AlgebraicGeometry.instIsDominantιCoborderRange, AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, AlgebraicGeometry.instIsClosedImmersionLiftCoborder, AlgebraicGeometry.liftCoborder_app, liftCoborder_preimage, liftCoborder_ι_assoc, liftCoborder_ι
liftCoborder 📖	CompOp	6 math math: AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, AlgebraicGeometry.instIsClosedImmersionLiftCoborder, AlgebraicGeometry.liftCoborder_app, liftCoborder_preimage, liftCoborder_ι_assoc, liftCoborder_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallyClosed_range 📖	mathematical	—	IsLocallyClosed 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 toLRSHom'	—	AlgebraicGeometry.IsImmersion.isLocallyClosed_range
liftCoborder_preimage 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.Opens.toScheme coborderRange 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 toLRSHom' liftCoborder AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier opensFunctor AlgebraicGeometry.Scheme.Opens.ι AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι	—	AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι liftCoborder_ι comp_preimage preimage_image_eq
liftCoborder_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme coborderRange liftCoborder AlgebraicGeometry.Scheme.Opens.ι	—	AlgebraicGeometry.IsOpenImmersion.lift_fac
liftCoborder_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme coborderRange liftCoborder AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCoborder_ι

---

← Back to Index