Functorial

📁 Source: Mathlib/AlgebraicGeometry/IdealSheaf/Functorial.lean

Statistics

Metric	Count
Definitions comap, comapIso, map, subschemeMap	4
Theorems ker_comp, comapIso_hom_fst, comapIso_hom_fst_assoc, comapIso_hom_snd, comapIso_hom_snd_assoc, comapIso_inv_subschemeι, comapIso_inv_subschemeι_assoc, comap_bot, comap_comp, comap_id, comap_map_le, comap_mono, comap_sup, comap_top, ideal_comap_of_isOpenImmersion, ideal_map, ideal_map_of_isAffineHom, ker_fst_of_isClosedImmersion, le_map_comap, le_map_iff_comap_le, map_bot, map_comp, map_gc, map_id, map_inf, map_ker, map_mono, map_top, map_vanishingIdeal, subschemeMap_subschemeι, subschemeMap_subschemeι_assoc, support_comap, support_map, isPullback_of_isClosedImmersion	34
Total	38

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPullback_of_isClosedImmersion 📖	mathematical	CategoryTheory.CategoryStruct.comp Scheme CategoryTheory.Category.toCategoryStruct Scheme.instCategory Scheme.IdealSheafData.comap Scheme.Hom.ker	CategoryTheory.IsPullback	—	Scheme.Pullback.instHasPullback IsClosedImmersion.isIso_of_ker_eq instIsClosedImmersionFstScheme CategoryTheory.Limits.limit.lift_π Scheme.IdealSheafData.ker_fst_of_isClosedImmersion CategoryTheory.Category.id_comp CategoryTheory.IsPullback.paste_vert CategoryTheory.IsPullback.of_vert_isIso CategoryTheory.IsIso.id CategoryTheory.Category.comp_id CategoryTheory.IsPullback.of_hasPullback

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_comp 📖	mathematical	—	ker CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.IdealSheafData.map	—	AlgebraicGeometry.Scheme.IdealSheafData.map_ker

AlgebraicGeometry.Scheme.IdealSheafData

Definitions

Name	Category	Theorems
comap 📖	CompOp	19 math math: le_map_iff_comap_le, comap_mono, comapIso_hom_snd_assoc, comap_id, ker_fst_of_isClosedImmersion, ideal_comap_of_isOpenImmersion, comapIso_inv_subschemeι_assoc, support_comap, comap_sup, comapIso_inv_subschemeι, comapIso_hom_snd, comapIso_hom_fst_assoc, comap_bot, comapIso_hom_fst, comap_comp, comap_top, map_gc, comap_map_le, le_map_comap
comapIso 📖	CompOp	6 math math: comapIso_hom_snd_assoc, comapIso_inv_subschemeι_assoc, comapIso_inv_subschemeι, comapIso_hom_snd, comapIso_hom_fst_assoc, comapIso_hom_fst
map 📖	CompOp	16 math math: le_map_iff_comap_le, ideal_map, map_inf, map_comp, map_mono, map_vanishingIdeal, map_top, AlgebraicGeometry.Scheme.Hom.ker_comp, support_map, map_id, map_bot, ideal_map_of_isAffineHom, map_gc, comap_map_le, map_ker, le_map_comap
subschemeMap 📖	CompOp	4 math math: comapIso_hom_snd_assoc, comapIso_hom_snd, subschemeMap_subschemeι_assoc, subschemeMap_subschemeι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comapIso_hom_fst 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme comap CategoryTheory.Limits.pullback subschemeι AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Iso.hom comapIso CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback comapIso_inv_subschemeι CategoryTheory.Iso.hom_inv_id_assoc
comapIso_hom_fst_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme comap CategoryTheory.Limits.pullback subschemeι AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Iso.hom comapIso CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comapIso_hom_fst
comapIso_hom_snd 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme comap CategoryTheory.Limits.pullback subschemeι AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Iso.hom comapIso CategoryTheory.Limits.pullback.snd subschemeMap le_map_comap	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback le_map_comap CategoryTheory.cancel_mono AlgebraicGeometry.IsPreimmersion.instMonoScheme instIsPreimmersionSubschemeι CategoryTheory.Category.assoc comapIso_hom_fst_assoc subschemeMap_subschemeι
comapIso_hom_snd_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme comap CategoryTheory.Limits.pullback subschemeι AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Iso.hom comapIso CategoryTheory.Limits.pullback.snd subschemeMap le_map_comap	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback le_map_comap CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comapIso_hom_snd
comapIso_inv_subschemeι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback subscheme subschemeι AlgebraicGeometry.Scheme.Pullback.instHasPullback comap CategoryTheory.Iso.inv comapIso CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.Hom.toImage_imageι AlgebraicGeometry.Scheme.Pullback.instHasPullback
comapIso_inv_subschemeι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory CategoryTheory.Limits.pullback subscheme subschemeι AlgebraicGeometry.Scheme.Pullback.instHasPullback comap CategoryTheory.Iso.inv comapIso CategoryTheory.Limits.pullback.fst	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comapIso_inv_subschemeι
comap_bot 📖	mathematical	—	comap Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot	—	GaloisConnection.l_bot map_gc
comap_comp 📖	mathematical	—	comap CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp comapIso_hom_fst CategoryTheory.Limits.pullback.map_isIso CategoryTheory.IsIso.id CategoryTheory.Iso.isIso_hom comap.eq_1 AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso CategoryTheory.Category.assoc CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst CategoryTheory.Limits.limit.lift_π
comap_id 📖	mathematical	—	comap CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	comap.eq_1 CategoryTheory.Limits.pullback_snd_iso_of_left_iso CategoryTheory.IsIso.id AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso CategoryTheory.IsIso.inv_isIso CategoryTheory.Limits.hasPullback_of_left_iso CategoryTheory.Limits.pullback_inv_snd_fst_of_left_isIso CategoryTheory.IsIso.inv_id CategoryTheory.Category.comp_id ker_subschemeι
comap_map_le 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder comap map	—	GaloisConnection.l_u_le map_gc
comap_mono 📖	mathematical	—	Monotone AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder instPartialOrder comap	—	GaloisConnection.monotone_l map_gc
comap_sup 📖	mathematical	—	comap AlgebraicGeometry.Scheme.IdealSheafData SemilatticeSup.toMax IdemSemiring.toSemilatticeSup IdemCommSemiring.toIdemSemiring instIdemCommSemiring	—	GaloisConnection.l_sup map_gc
comap_top 📖	mathematical	—	comap Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop	—	comap.eq_1 AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty Function.isEmpty instIsEmptyCarrierCarrierCommRingCatSubschemeTop AlgebraicGeometry.Scheme.Pullback.instHasPullback
ideal_comap_of_isOpenImmersion 📖	mathematical	—	ideal comap Ideal.comap 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 Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Hom.opensFunctor AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.Hom.appIso RingHom.instRingHomClass	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion RingHom.instRingHomClass AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion instQuasiCompactSubschemeι CategoryTheory.IsPullback.of_hasPullback Ideal.comap.congr_simp ker_subschemeι
ideal_map 📖	mathematical	—	ideal map Ideal.comap 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 Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.app RingHom.instRingHomClass	—	RingHom.instRingHomClass RingHom.ker_coe_equiv AlgebraicGeometry.Scheme.Hom.ker_apply AlgebraicGeometry.quasiCompact_comp instQuasiCompactSubschemeι Ideal.instIsTwoSided_1 RingHom.ker.congr_simp subschemeι_app Ideal.comap.congr_simp Ideal.mk_ker
ideal_map_of_isAffineHom 📖	mathematical	—	ideal map Ideal.comap 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 Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.IsAffineOpen.preimage RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.app RingHom.instRingHomClass	—	ideal_map AlgebraicGeometry.instQuasiCompactOfIsAffineHom AlgebraicGeometry.IsAffineOpen.preimage
ker_fst_of_isClosedImmersion 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.ker CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst comap	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp AlgebraicGeometry.Scheme.Hom.toImage_imageι AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso CategoryTheory.Limits.pullback.map_isIso CategoryTheory.IsIso.id AlgebraicGeometry.IsClosedImmersion.instIsIsoSchemeToImage CategoryTheory.Limits.pullback.lift_fst
le_map_comap 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	GaloisConnection.le_u_l map_gc
le_map_iff_comap_le 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	ker_subschemeι AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Category.assoc inclusion_subschemeι AlgebraicGeometry.Scheme.Hom.toImage_imageι CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.Scheme.Hom.le_ker_comp comapIso_hom_fst_assoc inclusion_subschemeι_assoc map.eq_1
map_bot 📖	mathematical	—	map Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot AlgebraicGeometry.Scheme.Hom.ker	—	AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData
map_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	le_antisymm le_map_iff_comap_le comap_comp comap_map_le LE.le.trans comap_mono
map_gc 📖	mathematical	—	GaloisConnection AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder instPartialOrder comap map	—	le_map_iff_comap_le
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.Category.comp_id ker_subschemeι
map_inf 📖	mathematical	—	map AlgebraicGeometry.Scheme.IdealSheafData SemilatticeInf.toMin instSemilatticeInf	—	GaloisConnection.u_inf map_gc
map_ker 📖	mathematical	—	map AlgebraicGeometry.Scheme.Hom.ker CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	map_comp
map_mono 📖	mathematical	—	Monotone AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder instPartialOrder map	—	GaloisConnection.monotone_u map_gc
map_top 📖	mathematical	—	map Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop	—	GaloisConnection.u_top map_gc
map_vanishingIdeal 📖	mathematical	—	map vanishingIdeal TopologicalSpace.Closeds.closure TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set.image 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' SetLike.coe TopologicalSpace.Closeds TopologicalSpace.Closeds.instSetLike	—	le_antisymm map.eq_1 le_support_iff_le_vanishingIdeal TopologicalSpace.Closeds.closure_le HasSubset.Subset.trans Set.instIsTransSubset AlgebraicGeometry.Scheme.Hom.comp_base TopCat.coe_comp Set.range_comp range_subschemeι coe_support_vanishingIdeal subset_refl Set.instReflSubset AlgebraicGeometry.Scheme.Hom.range_subset_ker_support Set.image_congr AlgebraicGeometry.Scheme.Hom.continuous support_comap instIsConcreteLE
subschemeMap_subschemeι 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder map	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme subschemeMap subschemeι	—	AlgebraicGeometry.IsClosedImmersion.lift_fac AlgebraicGeometry.IsClosedImmersion.instSubschemeι
subschemeMap_subschemeι_assoc 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder map	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme subschemeMap subschemeι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' subschemeMap_subschemeι
support_comap 📖	mathematical	—	support comap TopologicalSpace.Closeds.preimage 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.continuous	—	TopologicalSpace.Closeds.ext AlgebraicGeometry.Scheme.Hom.continuous comap.eq_1 AlgebraicGeometry.Scheme.Hom.support_ker AlgebraicGeometry.instQuasiCompactFstScheme instQuasiCompactSubschemeι AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.Scheme.Pullback.range_fst range_subschemeι TopologicalSpace.Closeds.coe_preimage IsClosed.closure_eq IsClosed.preimage TopologicalSpace.Closeds.isClosed
support_map 📖	mathematical	—	support map TopologicalSpace.Closeds.closure TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set.image 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' SetLike.coe TopologicalSpace.Closeds TopologicalSpace.Closeds.instSetLike	—	TopologicalSpace.Closeds.ext map.eq_1 AlgebraicGeometry.Scheme.Hom.support_ker AlgebraicGeometry.quasiCompact_comp instQuasiCompactSubschemeι AlgebraicGeometry.Scheme.Hom.comp_base TopCat.coe_comp Set.range_comp range_subschemeι TopologicalSpace.Closeds.coe_closure

---

← Back to Index