Subscheme

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

Statistics

Metric	Count
Definitions image, imageι, toImage, glueDataObj, glueDataObjCarrierIso, glueDataObjHom, glueDataObjMap, glueDataObjι, inclusion, subscheme, subschemeCover, subschemeFunctor, subschemeObjIso, subschemeι, kerAdjunction	15
Theorems stalkFunctor_toImage_injective, toImage_app, toImage_app_injective, toImage_imageι, toImage_imageι_assoc, glueDataObjHom_comp, glueDataObjHom_comp_assoc, glueDataObjHom_id, glueDataObjHom_ι, glueDataObjHom_ι_assoc, glueDataObjMap_glueDataObjι, glueDataObjMap_glueDataObjι_assoc, glueDataObjι_ι, ideal_le_ker_glueDataObjι, inclusion_comp, inclusion_comp_assoc, inclusion_id, inclusion_id_assoc, inclusion_subschemeι, inclusion_subschemeι_assoc, instIsEmptyCarrierCarrierCommRingCatSubschemeTop, instIsPreimmersionGlueDataObjι, instIsPreimmersionSubschemeι, instQuasiCompactSubschemeι, isLocalization_away, isOpenImmersion_glueDataObjMap, ker_glueDataObjι_appTop, ker_subschemeι, ker_subschemeι_app, opensRange_glueDataObjMap, opensRange_subschemeCover_map, range_glueDataObjι, range_glueDataObjι_ι, range_glueDataObjι_ι_eq_support_inter, range_subschemeι, subSchemeCover_map_inclusion, subSchemeCover_map_inclusion_assoc, subschemeCover_map_subschemeι, subschemeFunctor_map, subschemeFunctor_obj, subschemeι_app, subschemeι_app_surjective, subschemeι_apply, ideal_ker_le_ker_ΓSpecIso_inv_comp, instFullOppositeIdealSheafDataOverSubschemeFunctor, instIsDominantToImageOfQuasiCompact, instIsIsoSubschemeιBotIdealSheafData, instQuasiCompactToImage, kerAdjunction_counit_app, kerAdjunction_unit_app	50
Total	65

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
kerAdjunction 📖	CompOp	2 math math: kerAdjunction_unit_app, kerAdjunction_counit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ideal_ker_le_ker_ΓSpecIso_inv_comp 📖	mathematical	—	Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Opens Set Set.instMembership affineOpens CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Preorder.toLE Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IdealSheafData.ideal Hom.ker RingHom.ker CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme instCategory Opens.toScheme Opens.ι Pullback.instHasPullback Top.top OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder RingHom RingHom.instFunLike RingHom.instRingHomClass CommRingCat.Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Spec CategoryTheory.Iso.inv ΓSpecIso Hom.appTop CategoryTheory.Limits.pullback.snd Opens.toSpecΓ	—	Pullback.instHasPullback AlgebraicGeometry.IsOpenImmersion.instFstScheme Opens.instIsOpenImmersionι Hom.image_top_eq_opensRange AlgebraicGeometry.IsOpenImmersion.hasPullback_of_right Hom.opensRange_pullbackFst Opens.opensRange_ι CategoryTheory.Iso.inv_comp_eq AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop CategoryTheory.Category.assoc CategoryTheory.Iso.eq_inv_comp LE.le.trans Hom.preimage_image_eq le_rfl CategoryTheory.Limits.pullback.condition AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv CategoryTheory.eqToHom_op Hom.app_eq_appLE Hom.appIso_hom Hom.appLE_map Hom.map_appLE Hom.appLE_comp_appLE Hom.appLE.congr_simp Hom.comp_appLE Set.image_preimage_subset Opens.ι_app le_top RingHom.instRingHomClass LE.le.trans_eq IdealSheafData.ideal_ofIdeals_le RingHom.ker_equiv_comp
instFullOppositeIdealSheafDataOverSubschemeFunctor 📖	mathematical	—	CategoryTheory.Functor.Full Opposite IdealSheafData CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder IdealSheafData.instPartialOrder CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.instCategoryOver IdealSheafData.subschemeFunctor	—	CategoryTheory.eqToHom_op CategoryTheory.Functor.FullyFaithful.full
instIsDominantToImageOfQuasiCompact 📖	mathematical	—	AlgebraicGeometry.IsDominant Hom.image Hom.toImage	—	denseRange_iff_closure_range Topology.IsEmbedding.closure_eq_preimage_closure_image Hom.isEmbedding IdealSheafData.instIsPreimmersionSubschemeι Set.univ_subset_iff Set.image_subset_iff Set.image_univ IdealSheafData.range_subschemeι Hom.support_ker Set.range_comp TopCat.coe_comp Hom.comp_base Hom.toImage_imageι subset_refl Set.instReflSubset
instIsIsoSubschemeιBotIdealSheafData 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme instCategory IdealSheafData.subscheme Bot.bot IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder IdealSheafData.instPartialOrder IdealSheafData.instOrderBot IdealSheafData.subschemeι	—	bot_le CategoryTheory.cancel_mono AlgebraicGeometry.IsPreimmersion.instMonoScheme IdealSheafData.instIsPreimmersionSubschemeι CategoryTheory.Category.assoc IdealSheafData.inclusion_subschemeι Hom.toImage_imageι CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
instQuasiCompactToImage 📖	mathematical	—	AlgebraicGeometry.QuasiCompact Hom.image Hom.toImage	—	Hom.toImage_imageι AlgebraicGeometry.QuasiCompact.of_comp AlgebraicGeometry.instQuasiSeparatedOfMonoScheme AlgebraicGeometry.IsPreimmersion.instMonoScheme IdealSheafData.instIsPreimmersionSubschemeι
kerAdjunction_counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.comp IdealSheafData Preorder.smallCategory PartialOrder.toPreorder IdealSheafData.instPartialOrder kerFunctor CategoryTheory.Functor.rightOp IdealSheafData.subschemeFunctor CategoryTheory.Functor.id CategoryTheory.Adjunction.counit kerAdjunction Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite.op CategoryTheory.Over.homMk Hom.toImage CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
kerAdjunction_unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app IdealSheafData Preorder.smallCategory PartialOrder.toPreorder IdealSheafData.instPartialOrder CategoryTheory.Functor.id CategoryTheory.Functor.comp Opposite CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.rightOp IdealSheafData.subschemeFunctor kerFunctor CategoryTheory.Adjunction.unit kerAdjunction CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj	—	—

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
image 📖	CompOp	13 math math: AlgebraicGeometry.IsClosedImmersion.instIsIsoSchemeToImage, toImage_app_injective, toImage_imageι, AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, toImage_imageι_assoc, stalkFunctor_toImage_injective, AlgebraicGeometry.Scheme.instQuasiCompactToImage, AlgebraicGeometry.Scheme.instIsDominantToImageOfQuasiCompact, AlgebraicGeometry.instUniversallyClosedToImage, AlgebraicGeometry.IsImmersion.instToImage, AlgebraicGeometry.IsImmersion.instIsOpenImmersionToImageOfQuasiCompact, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, toImage_app
imageι 📖	CompOp	6 math math: toImage_app_injective, toImage_imageι, AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, toImage_imageι_assoc, AlgebraicGeometry.exists_finite_imageι_comp_morphismRestrict_of_finite_image_preimage, toImage_app
toImage 📖	CompOp	13 math math: AlgebraicGeometry.IsClosedImmersion.instIsIsoSchemeToImage, toImage_app_injective, toImage_imageι, AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder, toImage_imageι_assoc, AlgebraicGeometry.Scheme.kerAdjunction_counit_app, stalkFunctor_toImage_injective, AlgebraicGeometry.Scheme.instQuasiCompactToImage, AlgebraicGeometry.Scheme.instIsDominantToImageOfQuasiCompact, AlgebraicGeometry.instUniversallyClosedToImage, AlgebraicGeometry.IsImmersion.instToImage, AlgebraicGeometry.IsImmersion.instIsOpenImmersionToImageOfQuasiCompact, toImage_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
stalkFunctor_toImage_injective 📖	mathematical	—	CommRingCat.carrier CategoryTheory.Functor.obj TopCat.Presheaf CommRingCat CommRingCat.instCategory AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace image TopCat.instCategoryPresheaf TopCat.Presheaf.stalkFunctor CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.PresheafedSpace.presheaf TopCat.Presheaf.pushforward AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' toImage DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Functor.map AlgebraicGeometry.PresheafedSpace.Hom.c	—	TopCat.Presheaf.stalkFunctor_map_injective_of_isBasis CommRingCat.Colimits.hasColimits_commRingCat CommRingCat.FilteredColimits.forget_preservesFilteredColimits IsOpen.preimage Topology.IsInducing.continuous Topology.IsEmbedding.isInducing isEmbedding AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionSubschemeι TopologicalSpace.Opens.is_open' TopologicalSpace.Opens.IsBasis.of_isInducing AlgebraicGeometry.Scheme.isBasis_affineOpens toImage_app_injective
toImage_app 📖	mathematical	—	app image toImage CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory 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 TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' imageι Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite TopologicalSpace.Opens AlgebraicGeometry.Scheme.IdealSheafData.subscheme ker TopCat.str CategoryTheory.Category.opposite AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.IdealSheafData.subschemeι CommRingCat.of HasQuotient.Quotient CommRingCat.carrier Ideal CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Ideal.instHasQuotient_1 AlgebraicGeometry.Scheme.IdealSheafData.ideal Ideal.Quotient.commRing CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso CommRingCat.ofHom Ideal.Quotient.lift CommRing.toRing Ideal.instIsTwoSided_1 CommRingCat.Hom.hom AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le RingHom.ker RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	CategoryTheory.ConcreteCategory.epi_of_surjective AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective Ideal.instIsTwoSided_1 AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le CategoryTheory.cancel_epi comp_app toImage_imageι congr_app AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app CategoryTheory.Functor.map_isIso CategoryTheory.isIso_op CategoryTheory.instIsIsoEqToHom CategoryTheory.IsIso.eq_comp_inv CategoryTheory.Functor.map_inv CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.eqToHom_op CategoryTheory.inv.congr_simp CategoryTheory.inv_eqToHom Mathlib.Tactic.Reassoc.eq_whisker' CommRingCat.ofHom_comp CommRingCat.ofHom_hom CategoryTheory.eqToHom_refl CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
toImage_app_injective 📖	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 image 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' imageι Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens toImage DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier app	—	Ideal.instIsTwoSided_1 AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le toImage_app RingHom.lift_injective_of_ker_le_ideal RingHom.instRingHomClass ker_apply RingEquiv.injective
toImage_imageι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory image toImage imageι	—	copyBase_eq
toImage_imageι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory image toImage imageι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toImage_imageι

AlgebraicGeometry.Scheme.IdealSheafData

Definitions

Name	Category	Theorems
glueDataObj 📖	CompOp	19 math math: glueDataObjHom_ι_assoc, glueDataObjHom_ι, ideal_le_ker_glueDataObjι, range_glueDataObjι_ι_eq_support_inter, range_glueDataObjι_ι, subschemeCover_map_subschemeι, glueDataObjMap_glueDataObjι_assoc, glueDataObjMap_glueDataObjι, opensRange_glueDataObjMap, range_glueDataObjι, isOpenImmersion_glueDataObjMap, instIsPreimmersionGlueDataObjι, subSchemeCover_map_inclusion_assoc, subSchemeCover_map_inclusion, glueDataObjHom_comp_assoc, glueDataObjHom_comp, ker_glueDataObjι_appTop, glueDataObjι_ι, glueDataObjHom_id
glueDataObjCarrierIso 📖	CompOp	—
glueDataObjHom 📖	CompOp	7 math math: glueDataObjHom_ι_assoc, glueDataObjHom_ι, subSchemeCover_map_inclusion_assoc, subSchemeCover_map_inclusion, glueDataObjHom_comp_assoc, glueDataObjHom_comp, glueDataObjHom_id
glueDataObjMap 📖	CompOp	4 math math: glueDataObjMap_glueDataObjι_assoc, glueDataObjMap_glueDataObjι, opensRange_glueDataObjMap, isOpenImmersion_glueDataObjMap
glueDataObjι 📖	CompOp	13 math math: glueDataObjHom_ι_assoc, glueDataObjHom_ι, ideal_le_ker_glueDataObjι, range_glueDataObjι_ι_eq_support_inter, range_glueDataObjι_ι, subschemeCover_map_subschemeι, glueDataObjMap_glueDataObjι_assoc, glueDataObjMap_glueDataObjι, opensRange_glueDataObjMap, range_glueDataObjι, instIsPreimmersionGlueDataObjι, ker_glueDataObjι_appTop, glueDataObjι_ι
inclusion 📖	CompOp	10 math math: inclusion_subschemeι_assoc, inclusion_subschemeι, AlgebraicGeometry.instIsClosedImmersionInclusion, inclusion_comp_assoc, inclusion_comp, subSchemeCover_map_inclusion_assoc, subSchemeCover_map_inclusion, inclusion_id_assoc, inclusion_id, subschemeFunctor_map
subscheme 📖	CompOp	33 math math: instIsPreimmersionSubschemeι, inclusion_subschemeι_assoc, inclusion_subschemeι, instIsEmptyCarrierCarrierCommRingCatSubschemeTop, comapIso_hom_snd_assoc, AlgebraicGeometry.instIsClosedImmersionInclusion, subschemeCover_map_subschemeι, range_subschemeι, inclusion_comp_assoc, subschemeι_app, comapIso_inv_subschemeι_assoc, comapIso_inv_subschemeι, inclusion_comp, opensRange_subschemeCover_map, subschemeFunctor_obj, ker_subschemeι_app, AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData, comapIso_hom_snd, ker_subschemeι, comapIso_hom_fst_assoc, subSchemeCover_map_inclusion_assoc, subSchemeCover_map_inclusion, inclusion_id_assoc, comapIso_hom_fst, subschemeι_app_surjective, inclusion_id, subschemeMap_subschemeι_assoc, AlgebraicGeometry.Scheme.Hom.toImage_app, instQuasiCompactSubschemeι, subschemeMap_subschemeι, subschemeFunctor_map, AlgebraicGeometry.IsClosedImmersion.instSubschemeι, subschemeι_apply
subschemeCover 📖	CompOp	4 math math: subschemeCover_map_subschemeι, opensRange_subschemeCover_map, subSchemeCover_map_inclusion_assoc, subSchemeCover_map_inclusion
subschemeFunctor 📖	CompOp	5 math math: AlgebraicGeometry.Scheme.kerAdjunction_unit_app, AlgebraicGeometry.Scheme.kerAdjunction_counit_app, AlgebraicGeometry.Scheme.instFullOppositeIdealSheafDataOverSubschemeFunctor, subschemeFunctor_obj, subschemeFunctor_map
subschemeObjIso 📖	CompOp	2 math math: subschemeι_app, AlgebraicGeometry.Scheme.Hom.toImage_app
subschemeι 📖	CompOp	25 math math: instIsPreimmersionSubschemeι, inclusion_subschemeι_assoc, inclusion_subschemeι, comapIso_hom_snd_assoc, subschemeCover_map_subschemeι, range_subschemeι, subschemeι_app, comapIso_inv_subschemeι_assoc, comapIso_inv_subschemeι, opensRange_subschemeCover_map, subschemeFunctor_obj, ker_subschemeι_app, AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData, comapIso_hom_snd, ker_subschemeι, comapIso_hom_fst_assoc, comapIso_hom_fst, subschemeι_app_surjective, subschemeMap_subschemeι_assoc, AlgebraicGeometry.Scheme.Hom.toImage_app, instQuasiCompactSubschemeι, subschemeMap_subschemeι, subschemeFunctor_map, AlgebraicGeometry.IsClosedImmersion.instSubschemeι, subschemeι_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
glueDataObjHom_comp 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory glueDataObj glueDataObjHom LE.le.trans	—	LE.le.trans CategoryTheory.cancel_mono AlgebraicGeometry.IsPreimmersion.instMonoScheme instIsPreimmersionGlueDataObjι CategoryTheory.Category.assoc glueDataObjHom_ι
glueDataObjHom_comp_assoc 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory glueDataObj glueDataObjHom LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' glueDataObjHom_comp
glueDataObjHom_id 📖	mathematical	—	glueDataObjHom le_refl AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder instPartialOrder CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory glueDataObj	—	le_refl CategoryTheory.cancel_mono AlgebraicGeometry.IsPreimmersion.instMonoScheme instIsPreimmersionGlueDataObjι glueDataObjHom_ι CategoryTheory.Category.id_comp
glueDataObjHom_ι 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory glueDataObj AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens glueDataObjHom glueDataObjι	—	glueDataObjHom.eq_1 glueDataObjι.eq_1 AlgebraicGeometry.Spec.map_comp_assoc CommRingCat.ofHom_comp
glueDataObjHom_ι_assoc 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory glueDataObj glueDataObjHom AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens glueDataObjι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' glueDataObjHom_ι
glueDataObjMap_glueDataObjι 📖	mathematical	Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory glueDataObj AlgebraicGeometry.Scheme.Opens.toScheme glueDataObjMap glueDataObjι AlgebraicGeometry.Scheme.homOfLE	—	ideal_le_comap_ideal glueDataObjMap.eq_1 glueDataObjι.eq_1 AlgebraicGeometry.Spec.map_comp_assoc CommRingCat.ofHom_comp CategoryTheory.Category.assoc CategoryTheory.Iso.eq_inv_comp AlgebraicGeometry.IsAffineOpen.isoSpec_hom CommRingCat.ofHom_hom AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
glueDataObjMap_glueDataObjι_assoc 📖	mathematical	Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory glueDataObj glueDataObjMap AlgebraicGeometry.Scheme.Opens.toScheme glueDataObjι AlgebraicGeometry.Scheme.homOfLE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' glueDataObjMap_glueDataObjι
glueDataObjι_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory glueDataObj AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens glueDataObjι AlgebraicGeometry.Scheme.Opens.ι AlgebraicGeometry.Spec CommRingCat.of HasQuotient.Quotient CommRingCat.carrier Opposite.op Ideal Ring.toSemiring CommRing.toRing CommRingCat.commRing Ideal.instHasQuotient ideal Ideal.Quotient.commRing AlgebraicGeometry.Spec.map CommRingCat.ofHom Ideal.instIsTwoSided_1 AlgebraicGeometry.IsAffineOpen.fromSpec	—	Ideal.instIsTwoSided_1 glueDataObjι.eq_1 CategoryTheory.Category.assoc
ideal_le_ker_glueDataObjι 📖	mathematical	—	Ideal 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 CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Preorder.toLE Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal RingHom.ker glueDataObj AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' glueDataObjι AlgebraicGeometry.Scheme.Opens.ι RingHom RingHom.instFunLike RingHom.instRingHomClass CommRingCat.Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.Hom.app	—	TopCat.Presheaf.IsSheaf.section_ext CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.forgetReflectIsos AlgebraicGeometry.SheafedSpace.IsSheaf AlgebraicGeometry.exists_basicOpen_le_affine_inter AlgebraicGeometry.Scheme.basicOpen_le AlgebraicGeometry.Scheme.affineBasicOpen_le AlgebraicGeometry.Scheme.Hom.isIso_app isOpenImmersion_glueDataObjMap opensRange_glueDataObjMap le_refl CategoryTheory.ConcreteCategory.isIso_iff_bijective CategoryTheory.Category.assoc map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass LE.le.trans le_rfl glueDataObjMap_glueDataObjι_assoc AlgebraicGeometry.Scheme.Hom.app_eq_appLE AlgebraicGeometry.Scheme.Hom.map_appLE AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE AlgebraicGeometry.Scheme.Hom.appLE.congr_simp AlgebraicGeometry.Scheme.Hom.appLE.eq_1 AlgebraicGeometry.Scheme.homOfLE_ι Eq.trans_le AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι Set.image_preimage_subset AlgebraicGeometry.Scheme.ι_image_homOfLE_le_ι_image AlgebraicGeometry.Scheme.homOfLE_app AlgebraicGeometry.Scheme.Hom.app_eq RingHom.mem_ker ker_glueDataObjι_appTop Ideal.mem_comap Ideal.comap_comap CommRingCat.hom_comp Ideal.comap.congr_simp CategoryTheory.eqToHom_op CategoryTheory.eqToHom_unop ideal_le_comap_ideal RingHom.map_zero
inclusion_comp 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme inclusion LE.le.trans	—	AlgebraicGeometry.Scheme.Cover.hom_ext LE.le.trans subSchemeCover_map_inclusion_assoc subSchemeCover_map_inclusion glueDataObjHom_comp_assoc
inclusion_comp_assoc 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme inclusion LE.le.trans	—	LE.le.trans CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inclusion_comp
inclusion_id 📖	mathematical	—	inclusion le_rfl AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder instPartialOrder CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme	—	AlgebraicGeometry.Scheme.Cover.hom_ext le_rfl subSchemeCover_map_inclusion glueDataObjHom_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
inclusion_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme inclusion le_rfl AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder instPartialOrder	—	le_rfl CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inclusion_id
inclusion_subschemeι 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme inclusion subschemeι	—	AlgebraicGeometry.Scheme.Cover.hom_ext subSchemeCover_map_inclusion_assoc subschemeCover_map_subschemeι glueDataObjHom_ι_assoc
inclusion_subschemeι_assoc 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory subscheme inclusion subschemeι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inclusion_subschemeι
instIsEmptyCarrierCarrierCommRingCatSubschemeTop 📖	mathematical	—	IsEmpty TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace subscheme Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop	—	AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty ker_subschemeι
instIsPreimmersionGlueDataObjι 📖	mathematical	—	AlgebraicGeometry.IsPreimmersion glueDataObj AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens glueDataObjι	—	Ideal.instIsTwoSided_1 AlgebraicGeometry.IsPreimmersion.mk_SpecMap Topology.IsClosedEmbedding.isEmbedding PrimeSpectrum.isClosedEmbedding_comap_of_surjective Ideal.Quotient.mk_surjective RingHom.surjectiveOnStalks_of_surjective AlgebraicGeometry.IsPreimmersion.comp AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_inv
instIsPreimmersionSubschemeι 📖	mathematical	—	AlgebraicGeometry.IsPreimmersion subscheme subschemeι	—	AlgebraicGeometry.IsPreimmersion.comp AlgebraicGeometry.IsPreimmersion.instOfIsOpenImmersion AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Iso.isIso_hom
instQuasiCompactSubschemeι 📖	mathematical	—	AlgebraicGeometry.QuasiCompact subscheme subschemeι	—	AlgebraicGeometry.quasiCompact_comp AlgebraicGeometry.quasiCompact_of_isIso CategoryTheory.Iso.isIso_hom
isLocalization_away 📖	mathematical	Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership AlgebraicGeometry.Scheme.affineBasicOpen	IsLocalization.Away HasQuotient.Quotient CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Ideal Ring.toSemiring CommRing.toRing CommRingCat.commRing Ideal.instHasQuotient ideal Ideal.Quotient.commSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 RingHom.toAlgebra Ideal.quotientMap CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Subtype.preorder CategoryTheory.homOfLE ideal_le_comap_ideal	—	Ideal.instIsTwoSided_1 ideal_le_comap_ideal AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsLocalization.of_surjective Ideal.Quotient.mk_surjective Ideal.mk_ker map_ideal'
isOpenImmersion_glueDataObjMap 📖	mathematical	—	AlgebraicGeometry.IsOpenImmersion glueDataObj AlgebraicGeometry.Scheme.affineBasicOpen glueDataObjMap AlgebraicGeometry.Scheme.affineBasicOpen_le	—	Ideal.instIsTwoSided_1 AlgebraicGeometry.Scheme.affineBasicOpen_le ideal_le_comap_ideal isLocalization_away AlgebraicGeometry.IsOpenImmersion.of_isLocalization
ker_glueDataObjι_appTop 📖	mathematical	—	RingHom.ker 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 AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder glueDataObj RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike RingHom.instRingHomClass CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appTop glueDataObjι Ideal.comap CategoryTheory.Iso.hom AlgebraicGeometry.Scheme.Opens.topIso ideal	—	Ideal.instIsTwoSided_1 RingHom.instRingHomClass Ideal.mk_ker RingHom.ker_equiv_comp RingHom.comap_ker RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.toRingHom_eq_coe CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom CommRingCat.hom_comp AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.ΓSpecIso_naturality AlgebraicGeometry.Scheme.Hom.appTop.eq_1 AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop CategoryTheory.Iso.inv_hom_id_assoc
ker_subschemeι 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.ker subscheme subschemeι	—	ext Ideal.ext RingHom.instRingHomClass AlgebraicGeometry.Scheme.Hom.ker_apply instQuasiCompactSubschemeι ker_subschemeι_app
ker_subschemeι_app 📖	mathematical	—	RingHom.ker 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 subscheme AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' subschemeι RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike RingHom.instRingHomClass CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.app ideal	—	RingHom.instRingHomClass Ideal.instIsTwoSided_1 subschemeι_app AlgebraicGeometry.Scheme.AffineOpenCover.instIsOpenImmersionF AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange opensRange_subschemeCover_map RingHom.ker_equiv_comp Ideal.mk_ker
opensRange_glueDataObjMap 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.opensRange glueDataObj AlgebraicGeometry.Scheme.affineBasicOpen glueDataObjMap AlgebraicGeometry.Scheme.affineBasicOpen_le isOpenImmersion_glueDataObjMap CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.Opens.toScheme Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens 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' glueDataObjι AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier AlgebraicGeometry.Scheme.Opens.ι AlgebraicGeometry.Scheme.basicOpen	—	Ideal.instIsTwoSided_1 AlgebraicGeometry.Scheme.affineBasicOpen_le ideal_le_comap_ideal isLocalization_away TopologicalSpace.Opens.ext isOpenImmersion_glueDataObjMap PrimeSpectrum.localization_away_comap_range PrimeSpectrum.continuous_comap PrimeSpectrum.comap_basicOpen AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen AlgebraicGeometry.Scheme.Hom.comp_preimage glueDataObjι_ι
opensRange_subschemeCover_map 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.opensRange AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.AffineCover.X AlgebraicGeometry.IsOpenImmersion subscheme subschemeCover AlgebraicGeometry.Scheme.AffineCover.f AlgebraicGeometry.Scheme.AffineOpenCover.instIsOpenImmersionF 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' subschemeι Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens	—	—
range_glueDataObjι 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens glueDataObj 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' glueDataObjι Set.image AlgebraicGeometry.Spec CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CategoryTheory.Iso.inv AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.IsAffineOpen.isoSpec PrimeSpectrum.zeroLocus CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal	—	Set.range_comp Set.image_congr RingHom.instRingHomClass range_comap_of_surjective Ideal.Quotient.mk_surjective Ideal.mk_ker
range_glueDataObjι_ι 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace glueDataObj 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' CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens glueDataObjι AlgebraicGeometry.Scheme.Opens.ι Set.instInter AlgebraicGeometry.Scheme.zeroLocus SetLike.coe Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier	—	Set.range_comp range_glueDataObjι Set.image_congr Set.image_comp TopCat.coe_comp AlgebraicGeometry.Scheme.Hom.comp_base AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus
range_glueDataObjι_ι_eq_support_inter 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace glueDataObj 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' CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens glueDataObjι AlgebraicGeometry.Scheme.Opens.ι Set.instInter SetLike.coe TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike support TopologicalSpace.Opens.instSetLike	—	range_glueDataObjι_ι coe_support_inter
range_subschemeι 📖	mathematical	—	Set.range TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace subscheme 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' subschemeι SetLike.coe TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike support	—	Set.range_comp AlgebraicGeometry.range_eq_univ AlgebraicGeometry.instSurjectiveOfIsIsoScheme CategoryTheory.Iso.isIso_hom Set.image_univ
subSchemeCover_map_inclusion 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.AffineCover.X AlgebraicGeometry.IsOpenImmersion subscheme subschemeCover AlgebraicGeometry.Scheme.AffineCover.f inclusion glueDataObj glueDataObjHom	—	AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms
subSchemeCover_map_inclusion_assoc 📖	mathematical	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.AffineCover.X AlgebraicGeometry.IsOpenImmersion subscheme subschemeCover AlgebraicGeometry.Scheme.AffineCover.f inclusion glueDataObj glueDataObjHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' subSchemeCover_map_inclusion
subschemeCover_map_subschemeι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec AlgebraicGeometry.Scheme.AffineCover.X AlgebraicGeometry.IsOpenImmersion subscheme subschemeCover AlgebraicGeometry.Scheme.AffineCover.f subschemeι glueDataObj AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens glueDataObjι AlgebraicGeometry.Scheme.Opens.ι	—	CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc
subschemeFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite AlgebraicGeometry.Scheme.IdealSheafData CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver subschemeFunctor CategoryTheory.Over.homMk subscheme Opposite.unop subschemeι inclusion	—	—
subschemeFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite AlgebraicGeometry.Scheme.IdealSheafData CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver subschemeFunctor subscheme Opposite.unop subschemeι	—	—
subschemeι_app 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.app subscheme subschemeι AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CommRingCat.of CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier 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 CommRingCat.commRing HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient ideal Ideal.Quotient.commRing AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CommRingCat.ofHom Ideal.instIsTwoSided_1 CategoryTheory.Iso.inv CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 subschemeObjIso	—	subschemeCover_map_subschemeι CategoryTheory.Category.assoc AlgebraicGeometry.Scheme.Hom.congr_app Ideal.instIsTwoSided_1 Set.image_preimage_subset AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self CategoryTheory.isIso_op CategoryTheory.Functor.map_isIso CategoryTheory.instIsIsoEqToHom CategoryTheory.isIso_unop CategoryTheory.Iso.isIso_inv AlgebraicGeometry.IsAffineOpen.fromSpec_app_self CategoryTheory.eqToHom_op AlgebraicGeometry.Scheme.Hom.naturality_assoc CategoryTheory.inv_eqToHom CategoryTheory.eqToHom_unop CategoryTheory.inv.congr_simp CategoryTheory.IsIso.Iso.inv_inv CategoryTheory.Iso.hom_inv_id_assoc AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc CategoryTheory.unop_inv AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
subschemeι_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 Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens subscheme AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' subschemeι DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.app	—	Ideal.instIsTwoSided_1 subschemeι_app RingEquiv.surjective Ideal.Quotient.mk_surjective
subschemeι_apply 📖	mathematical	—	DFunLike.coe AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace subscheme TopCat.carrier 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' subschemeι TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Closeds.instSetLike support	—	—

---

← Back to Index