Basic

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

Statistics

Metric	Count
Definitions ker, IdealSheafData, coe_support, equivOfIsAffine, gci, ideal, instAdd, instCompleteLattice, instCompleteSemilatticeSup, instIdemCommSemiring, instMul, instOne, instOrderBot, instOrderTop, instPartialOrder, instPowNat, instSemilatticeInf, instZero, mkOfMemSupportIff, ofIdealTop, ofIdeals, radical, support, supportSet, vanishingIdeal, kerFunctor, nilradical	27
Theorems iInf_ker_openCover_map_comp, iInf_ker_openCover_map_comp_apply, iUnion_support_ker_openCover_map_comp, ideal_ker_le, ker_apply, ker_comp_of_isIso, ker_eq_bot_of_isIso, ker_eq_top_iff_isEmpty, le_ker_comp, range_subset_ker_support, support_ker, add_eq_sup, bot_mul, coe_support_eq_eq_iInter_zeroLocus, coe_support_inter, coe_support_mkOfMemSupportIff, coe_support_ofIdealTop, coe_support_vanishingIdeal, equivOfIsAffine_apply, equivOfIsAffine_symm_apply, ext, ext_iff, ext_of_iSup_eq_top, ext_of_isAffine, gc, ideal_biInf, ideal_bot, ideal_iInf, ideal_iSup, ideal_inf, ideal_le_comap_ideal, ideal_mono, ideal_mul, ideal_ofIdeals_le, ideal_pow, ideal_sSup, ideal_sup, ideal_top, inf_mul, instIsOrderedRing, isClosed_supportSet, le_def, le_ofIdeals_iff, le_of_iSup_eq_top, le_of_isAffine, le_radical, le_support_iff_le_vanishingIdeal, map_ideal, map_ideal', map_ideal_basicOpen, mem_supportSet_iff, mem_supportSet_iff_mem_support, mem_supportSet_iff_of_mem, mem_support_iff, mem_support_iff_of_mem, mkOfMemSupportIff_ideal, mul_bot, mul_inf, mul_top, ofIdealTop_ideal, ofIdeals_ideal, ofIdeals_mono, one_eq_top, radical_bot, radical_ideal, radical_inf, radical_mul, radical_sup, radical_top, strictMono_ideal, supportSet_eq_iInter_zeroLocus, supportSet_inter, supportSet_subset_zeroLocus, support_antitone, support_bot, support_eq_bot_iff, support_eq_top_iff, support_iSup, support_mul, support_pow, support_pow_succ, support_radical, support_sSup, support_sup, support_top, top_mul, vanishingIdeal_antimono, vanishingIdeal_bot, vanishingIdeal_iSup, vanishingIdeal_ideal, vanishingIdeal_sSup, vanishingIdeal_sup, vanishingIdeal_support, vanishingIdeal_top, zeroLocus_inter_subset_supportSet, zero_eq_bot, kerFunctor_map, kerFunctor_obj, ker_eq_top_of_isEmpty, ker_ideal_of_isPullback_of_isOpenImmersion, ker_morphismRestrict_ideal, ker_of_isAffine, ker_toSpecΓ, nilradical_eq_bot, support_nilradical	105
Total	132

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
IdealSheafData 📖	CompData	90 math math: IdealSheafData.radical_sup, IdealSheafData.ideal_sSup, IdealSheafData.one_eq_top, IdealSheafData.le_of_iSup_eq_top, IdealSheafData.le_map_iff_comap_le, IdealSheafData.gc, Hom.le_ker_comp, IdealSheafData.le_of_isAffine, IdealSheafData.radical_bot, IdealSheafData.equivOfIsAffine_apply, IdealSheafData.equivOfIsAffine_symm_apply, IdealSheafData.ideal_mul, IdealSheafData.support_mul, IdealSheafData.radical_mul, IdealSheafData.comap_mono, IdealSheafData.radical_inf, IdealSheafData.ideal_pow, IdealSheafData.zero_eq_bot, kerAdjunction_unit_app, IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop, AlgebraicGeometry.isSchemeTheoreticallyDominant_iff, IdealSheafData.map_inf, IdealSheafData.le_radical, ker_toSpecΓ, IdealSheafData.ideal_bot, IdealSheafData.le_support_iff_le_vanishingIdeal, IdealSheafData.le_ofIdeals_iff, kerAdjunction_counit_app, IdealSheafData.support_antitone, Hom.iInf_ker_openCover_map_comp, IdealSheafData.support_eq_top_iff, IdealSheafData.bot_mul, ker_eq_top_of_isEmpty, IdealSheafData.ofIdeals_mono, IdealSheafData.map_mono, IdealSheafData.mul_top, IdealSheafData.vanishingIdeal_sup, IdealSheafData.comap_sup, Hom.ker_eq_bot_of_isIso, instFullOppositeIdealSheafDataOverSubschemeFunctor, nilradical_eq_bot, IdealSheafData.support_eq_bot_iff, Hom.ker_eq_top_iff_isEmpty, IdealSheafData.map_top, IdealSheafData.support_iSup, IdealSheafData.subschemeFunctor_obj, IdealSheafData.ideal_top, AlgebraicGeometry.IsClosedImmersion.isIso_lift, IdealSheafData.mul_inf, kerFunctor_map, Hom.ker_eq_bot, instIsIsoSubschemeιBotIdealSheafData, IdealSheafData.ideal_iInf, Hom.ker_toNormalization, IdealSheafData.support_pow_succ, IdealSheafData.comap_bot, IdealSheafData.ideal_sup, IdealSheafData.ideal_mono, IdealSheafData.ideal_iSup, IdealSheafData.inclusion_id_assoc, IdealSheafData.ideal_inf, AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot, IdealSheafData.support_top, IdealSheafData.support_pow, IdealSheafData.top_mul, IdealSheafData.map_bot, IdealSheafData.inclusion_id, IdealSheafData.instIsOrderedRing, kerFunctor_obj, IdealSheafData.inf_mul, IdealSheafData.ideal_biInf, IdealSheafData.support_bot, IdealSheafData.radical_top, IdealSheafData.support_sup, IdealSheafData.mul_bot, IdealSheafData.comap_top, IdealSheafData.support_sSup, IdealSheafData.vanishingIdeal_iSup, IdealSheafData.strictMono_ideal, IdealSheafData.subschemeFunctor_map, IdealSheafData.vanishingIdeal_sSup, IdealSheafData.map_gc, IdealSheafData.comap_map_le, AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot, IdealSheafData.le_def, IdealSheafData.vanishingIdeal_bot, IdealSheafData.le_map_comap, IdealSheafData.glueDataObjHom_id, IdealSheafData.add_eq_sup, IdealSheafData.vanishingIdeal_antimono
kerFunctor 📖	CompOp	4 math math: kerAdjunction_unit_app, kerAdjunction_counit_app, kerFunctor_map, kerFunctor_obj
nilradical 📖	CompOp	4 math math: support_nilradical, IdealSheafData.radical_bot, nilradical_eq_bot, IdealSheafData.vanishingIdeal_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kerFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.Category.opposite CategoryTheory.instCategoryOver IdealSheafData Preorder.smallCategory PartialOrder.toPreorder IdealSheafData.instPartialOrder kerFunctor CategoryTheory.homOfLE Hom.ker CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
kerFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Over AlgebraicGeometry.Scheme instCategory CategoryTheory.Category.opposite CategoryTheory.instCategoryOver IdealSheafData Preorder.smallCategory PartialOrder.toPreorder IdealSheafData.instPartialOrder kerFunctor Hom.ker CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit Opposite.unop CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
ker_eq_top_of_isEmpty 📖	mathematical	—	Hom.ker Top.top IdealSheafData OrderTop.toTop Preorder.toLE PartialOrder.toPreorder IdealSheafData.instPartialOrder IdealSheafData.instOrderTop	—	top_le_iff IdealSheafData.le_ofIdeals_iff AlgebraicGeometry.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensOfIsEmpty
ker_ideal_of_isPullback_of_isOpenImmersion 📖	mathematical	CategoryTheory.IsPullback AlgebraicGeometry.Scheme instCategory	IdealSheafData.ideal Hom.ker Ideal.comap 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 AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Hom.opensFunctor AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Iso.inv Hom.appIso RingHom.instRingHomClass	—	CategoryTheory.MorphismProperty.of_isPullback AlgebraicGeometry.quasiCompact_isStableUnderBaseChange CategoryTheory.IsPullback.flip AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange Ideal.ext AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion RingHom.instRingHomClass AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback CategoryTheory.Iso.inv_comp_eq CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv LE.le.trans Eq.ge Hom.preimage_image_eq le_rfl CategoryTheory.CommSq.w CategoryTheory.IsPullback.toCommSq Hom.app_eq_appLE CategoryTheory.eqToHom_op Hom.appIso_hom' Hom.map_appLE Hom.appLE_comp_appLE Hom.appLE.congr_simp Hom.ker_apply Ideal.comap.congr_simp map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass CategoryTheory.ConcreteCategory.bijective_of_isIso CategoryTheory.Iso.isIso_inv
ker_morphismRestrict_ideal 📖	mathematical	—	IdealSheafData.ideal Opens.toScheme Hom.ker CategoryTheory.Functor.obj Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom Hom.toLRSHom' AlgebraicGeometry.morphismRestrict Set Set.instMembership affineOpens AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Hom.opensFunctor Opens.ι Opens.instIsOpenImmersionι AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion	—	CategoryTheory.MorphismProperty.of_isPullback AlgebraicGeometry.quasiCompact_isStableUnderBaseChange CategoryTheory.IsPullback.flip AlgebraicGeometry.isPullback_morphismRestrict Ideal.ext Opens.instIsOpenImmersionι AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion Eq.le AlgebraicGeometry.image_morphismRestrict_preimage RingHom.instRingHomClass Hom.ker_apply RingHom.ker.congr_simp AlgebraicGeometry.morphismRestrict_app' CategoryTheory.eqToHom_op map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass CategoryTheory.ConcreteCategory.bijective_of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.isIso_op CategoryTheory.instIsIsoEqToHom
ker_of_isAffine 📖	mathematical	—	Hom.ker IdealSheafData.ofIdealTop RingHom.ker 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike RingHom.instRingHomClass CommRingCat.Hom.hom Hom.appTop	—	LE.le.antisymm RingHom.instRingHomClass IdealSheafData.le_of_isAffine LE.le.trans AlgebraicGeometry.isAffineOpen_top Hom.ideal_ker_le CategoryTheory.Functor.map_id Ideal.map_id IdealSheafData.le_ofIdeals_iff RingHom.comap_ker RingHom.ker.congr_simp Hom.naturality map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass
ker_toSpecΓ 📖	mathematical	—	Hom.ker AlgebraicGeometry.Spec 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder toSpecΓ Bot.bot IdealSheafData OrderBot.toBot IdealSheafData.instPartialOrder IdealSheafData.instOrderBot	—	IdealSheafData.ext_of_isAffine AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.isAffineOpen_top RingHom.instRingHomClass Hom.ker_apply AlgebraicGeometry.instQuasiCompactToSpecΓOfCompactSpaceCarrierCarrierCommRingCat RingHom.ker.congr_simp toSpecΓ_appTop RingHom.ker_coe_equiv
nilradical_eq_bot 📖	mathematical	—	nilradical Bot.bot IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder IdealSheafData.instPartialOrder IdealSheafData.instOrderBot	—	IdealSheafData.ext Ideal.ext Ideal.radical_eq_iff Ideal.isRadical_bot AlgebraicGeometry.IsReduced.component_reduced
support_nilradical 📖	mathematical	—	IdealSheafData.support nilradical Top.top TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra Order.Coframe.toCoheytingAlgebra TopologicalSpace.Closeds.instCoframe CoheytingAlgebra.toOrderTop	—	—

AlgebraicGeometry.Scheme.Hom

Definitions

Name	Category	Theorems
ker 📖	CompOp	30 math math: iUnion_support_ker_openCover_map_comp, le_ker_comp, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, AlgebraicGeometry.isSchemeTheoreticallyDominant_iff, AlgebraicGeometry.Scheme.ker_toSpecΓ, AlgebraicGeometry.Scheme.ker_of_isAffine, AlgebraicGeometry.Scheme.IdealSheafData.ker_fst_of_isClosedImmersion, ker_apply, iInf_ker_openCover_map_comp, AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty, ideal_ker_le, ker_eq_bot_of_isIso, ker_eq_top_iff_isEmpty, ker_comp_of_isIso, AlgebraicGeometry.Scheme.kerFunctor_map, iInf_ker_openCover_map_comp_apply, ker_eq_bot, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, ker_comp, ker_toNormalization, AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι, range_subset_ker_support, support_ker, AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot, AlgebraicGeometry.Scheme.IdealSheafData.map_bot, AlgebraicGeometry.Scheme.kerFunctor_obj, toImage_app, AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot, AlgebraicGeometry.Scheme.IdealSheafData.map_ker

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf_ker_openCover_map_comp 📖	mathematical	—	iInf AlgebraicGeometry.Scheme.IdealSheafData CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice AlgebraicGeometry.Scheme.IdealSheafData.instCompleteLattice ker CategoryTheory.PreZeroHypercover.X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	—	le_antisymm iInf_le_iff iInf_ker_openCover_map_comp_apply le_iInf_iff le_iInf le_ker_comp
iInf_ker_openCover_map_comp_apply 📖	mathematical	—	iInf 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 CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AlgebraicGeometry.Scheme.IdealSheafData.ideal ker CategoryTheory.PreZeroHypercover.X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	—	le_antisymm RingHom.instRingHomClass ker_apply TopCat.Presheaf.IsSheaf.section_ext CommRingCat.hasLimits CommRingCat.forget_preservesLimits CommRingCat.forgetReflectIsos AlgebraicGeometry.SheafedSpace.IsSheaf AlgebraicGeometry.Scheme.Cover.exists_eq AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgebraicGeometry.Scheme.instIsOpenImmersionF Set.image_preimage_subset RingEquiv.injective RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass RingEquiv.coe_toRingHom CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom Eq.ge preimage_image_eq appIso_hom' LE.le.trans le_rfl app_eq_appLE appLE_map appLE_comp_appLE CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id ideal_ker_le Ideal.mem_iInf le_iInf le_ker_comp
iUnion_support_ker_openCover_map_comp 📖	mathematical	—	Set.iUnion TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace CategoryTheory.PreZeroHypercover.I₀ AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover AlgebraicGeometry.Scheme.precoverage AlgebraicGeometry.IsOpenImmersion SetLike.coe TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike AlgebraicGeometry.Scheme.IdealSheafData.support ker CategoryTheory.PreZeroHypercover.X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.PreZeroHypercover.f	—	isEmpty_or_nonempty Function.isEmpty AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage Set.iUnion_of_empty AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty Set.iUnion_inter AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter iInf_ker_openCover_map_comp_apply AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty Set.ext TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open AlgebraicGeometry.Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ
ideal_ker_le 📖	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 AlgebraicGeometry.Scheme.IdealSheafData.ideal ker RingHom.ker AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' RingHom RingHom.instFunLike RingHom.instRingHomClass CommRingCat.Hom.hom app	—	AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le
ker_apply 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData.ideal ker 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 AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom toLRSHom' RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike RingHom.instRingHomClass CommRingCat.Hom.hom app	—	RingHom.instRingHomClass le_antisymm AlgebraicGeometry.Scheme.basicOpen_le Ideal.map_le_iff_le_comap RingHom.comap_ker RingHom.ker.congr_simp naturality Ideal.ker_le_comap AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen IsLocalization.exists_mk'_eq IsLocalization.mk'_mem_map_algebraMap_iff Eq.trans_le AlgebraicGeometry.Scheme.preimage_basicOpen IsLocalization.mk'_spec' map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass MulZeroClass.mul_zero AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact AlgebraicGeometry.QuasiCompact.isCompact_preimage TopologicalSpace.Opens.is_open' AlgebraicGeometry.IsAffineOpen.isCompact map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_ideal
ker_comp_of_isIso 📖	mathematical	—	ker CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	LE.le.antisymm' le_ker_comp LE.le.trans CategoryTheory.IsIso.inv_hom_id_assoc
ker_eq_bot_of_isIso 📖	mathematical	—	ker Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder AlgebraicGeometry.Scheme.IdealSheafData.instOrderBot	—	AlgebraicGeometry.Scheme.IdealSheafData.ext Ideal.ext RingHom.instRingHomClass ker_apply AlgebraicGeometry.quasiCompact_of_isIso map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass CategoryTheory.ConcreteCategory.bijective_of_isIso instIsIsoCommRingCatApp
ker_eq_top_iff_isEmpty 📖	mathematical	—	ker Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop Preorder.toLE PartialOrder.toPreorder AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder AlgebraicGeometry.Scheme.IdealSheafData.instOrderTop IsEmpty TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace	—	range_subset_ker_support AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty
le_ker_comp 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder ker CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono comp_app CommRingCat.hom_comp RingHom.instRingHomClass RingHom.comap_ker Ideal.ker_le_comap
range_subset_ker_support 📖	mathematical	—	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset 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' SetLike.coe TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike AlgebraicGeometry.Scheme.IdealSheafData.support ker	—	TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open AlgebraicGeometry.Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ Eq.ge AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter AlgebraicGeometry.Scheme.basicOpen_zero RingHom.instRingHomClass RingHom.mem_ker ideal_ker_le AlgebraicGeometry.Scheme.preimage_basicOpen
support_ker 📖	mathematical	—	SetLike.coe TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike AlgebraicGeometry.Scheme.IdealSheafData.support ker closure 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'	—	subset_antisymm Set.instAntisymmSubset AlgebraicGeometry.Spec.map_surjective RingHom.instRingHomClass AlgebraicGeometry.Scheme.ker_of_isAffine AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop AlgebraicGeometry.Spec_zeroLocus Ideal.coe_comap RingHom.comap_ker PrimeSpectrum.closure_range_comap CommRingCat.hom_comp AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality closure_mono Set.range_comp_subset_range AlgebraicGeometry.HasAffineProperty.iff_of_isAffine AlgebraicGeometry.instHasAffinePropertyQuasiCompactCompactSpaceCarrierCarrierCommRingCat Eq.ge iUnion_support_ker_openCover_map_comp Finite.of_fintype AlgebraicGeometry.Scheme.local_affine AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage AlgebraicGeometry.Scheme.compactSpace_of_isAffine AlgebraicGeometry.Scheme.Cover.exists_eq AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange AlgebraicGeometry.quasiCompact_isStableUnderBaseChange AlgebraicGeometry.isAffineOpen_top AlgebraicGeometry.Scheme.isAffine_affineCover AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter Function.Injective.mem_set_image Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding isOpenEmbedding AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.Scheme.image_zeroLocus AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_hasPullback Set.image_preimage_eq CategoryTheory.ConcreteCategory.bijective_of_isIso CategoryTheory.Iso.isIso_inv Eq.le image_top_eq_opensRange Set.mem_univ image_closure_subset_closure_image continuous Set.mem_image_of_mem AlgebraicGeometry.Scheme.Cover.pullbackHom_map comp_base TopCat.coe_comp Set.range_comp IsClosed.closure_subset_iff TopologicalSpace.Closeds.isClosed range_subset_ker_support

AlgebraicGeometry.Scheme.IdealSheafData

Definitions

Name	Category	Theorems
equivOfIsAffine 📖	CompOp	2 math math: equivOfIsAffine_apply, equivOfIsAffine_symm_apply
gci 📖	CompOp	—
ideal 📖	CompOp	54 math math: ideal_sSup, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, ideal_le_comap_ideal, equivOfIsAffine_apply, ideal_mul, ideal_le_ker_glueDataObjι, AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion, ideal_map, ideal_pow, mem_support_iff_of_mem, range_glueDataObjι_ι, vanishingIdeal_ideal, ideal_bot, mem_supportSet_iff, mem_support_iff, ofIdeals_ideal, le_ofIdeals_iff, AlgebraicGeometry.Scheme.Hom.ker_apply, ideal_comap_of_isOpenImmersion, map_ideal, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, subschemeι_app, ideal_top, isLocalization_away, mkOfMemSupportIff_ideal, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, ofIdealTop_ideal, ker_subschemeι_app, ideal_iInf, range_glueDataObjι, ext_iff, AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal, coe_support_eq_eq_iInter_zeroLocus, supportSet_subset_zeroLocus, zeroLocus_inter_subset_supportSet, map_ideal', ideal_sup, ideal_mono, ideal_iSup, radical_ideal, ideal_inf, coe_support_inter, ideal_ofIdeals_le, mem_supportSet_iff_of_mem, supportSet_inter, ker_glueDataObjι_appTop, ideal_biInf, glueDataObjι_ι, AlgebraicGeometry.Scheme.Hom.toImage_app, strictMono_ideal, ideal_map_of_isAffineHom, map_ideal_basicOpen, le_def, supportSet_eq_iInter_zeroLocus
instAdd 📖	CompOp	3 math math: equivOfIsAffine_apply, equivOfIsAffine_symm_apply, add_eq_sup
instCompleteLattice 📖	CompOp	12 math math: ideal_sSup, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp, support_iSup, mul_inf, ideal_iInf, ideal_sup, ideal_iSup, inf_mul, ideal_biInf, support_sSup, vanishingIdeal_iSup, vanishingIdeal_sSup
instCompleteSemilatticeSup 📖	CompOp	—
instIdemCommSemiring 📖	CompOp	5 math math: radical_sup, comap_sup, instIsOrderedRing, support_sup, add_eq_sup
instMul 📖	CompOp	11 math math: equivOfIsAffine_apply, equivOfIsAffine_symm_apply, ideal_mul, support_mul, radical_mul, bot_mul, mul_top, mul_inf, top_mul, inf_mul, mul_bot
instOne 📖	CompOp	1 math math: one_eq_top
instOrderBot 📖	CompOp	18 math math: radical_bot, zero_eq_bot, AlgebraicGeometry.isSchemeTheoreticallyDominant_iff, AlgebraicGeometry.Scheme.ker_toSpecΓ, ideal_bot, support_eq_top_iff, bot_mul, AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso, AlgebraicGeometry.Scheme.nilradical_eq_bot, AlgebraicGeometry.Scheme.Hom.ker_eq_bot, AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData, AlgebraicGeometry.Scheme.Hom.ker_toNormalization, comap_bot, AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot, map_bot, support_bot, mul_bot, AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot
instOrderTop 📖	CompOp	13 math math: one_eq_top, instIsEmptyCarrierCarrierCommRingCatSubschemeTop, AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty, mul_top, support_eq_bot_iff, AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty, map_top, ideal_top, support_top, top_mul, radical_top, comap_top, vanishingIdeal_bot
instPartialOrder 📖	CompOp	64 math math: one_eq_top, le_of_iSup_eq_top, le_map_iff_comap_le, gc, AlgebraicGeometry.Scheme.Hom.le_ker_comp, le_of_isAffine, radical_bot, equivOfIsAffine_apply, equivOfIsAffine_symm_apply, comap_mono, zero_eq_bot, AlgebraicGeometry.Scheme.kerAdjunction_unit_app, instIsEmptyCarrierCarrierCommRingCatSubschemeTop, AlgebraicGeometry.isSchemeTheoreticallyDominant_iff, le_radical, AlgebraicGeometry.Scheme.ker_toSpecΓ, ideal_bot, le_support_iff_le_vanishingIdeal, le_ofIdeals_iff, AlgebraicGeometry.Scheme.kerAdjunction_counit_app, support_antitone, support_eq_top_iff, bot_mul, AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty, ofIdeals_mono, map_mono, mul_top, AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso, AlgebraicGeometry.Scheme.instFullOppositeIdealSheafDataOverSubschemeFunctor, AlgebraicGeometry.Scheme.nilradical_eq_bot, support_eq_bot_iff, AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty, map_top, subschemeFunctor_obj, ideal_top, AlgebraicGeometry.IsClosedImmersion.isIso_lift, AlgebraicGeometry.Scheme.kerFunctor_map, AlgebraicGeometry.Scheme.Hom.ker_eq_bot, AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData, AlgebraicGeometry.Scheme.Hom.ker_toNormalization, comap_bot, ideal_mono, inclusion_id_assoc, AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot, support_top, top_mul, map_bot, inclusion_id, instIsOrderedRing, AlgebraicGeometry.Scheme.kerFunctor_obj, support_bot, radical_top, mul_bot, comap_top, strictMono_ideal, subschemeFunctor_map, map_gc, comap_map_le, AlgebraicGeometry.IsClosedImmersion.isIso_iff_ker_eq_bot, le_def, vanishingIdeal_bot, le_map_comap, glueDataObjHom_id, vanishingIdeal_antimono
instPowNat 📖	CompOp	3 math math: ideal_pow, support_pow_succ, support_pow
instSemilatticeInf 📖	CompOp	5 math math: radical_mul, radical_inf, map_inf, vanishingIdeal_sup, ideal_inf
instZero 📖	CompOp	1 math math: zero_eq_bot
mkOfMemSupportIff 📖	CompOp	2 math math: coe_support_mkOfMemSupportIff, mkOfMemSupportIff_ideal
ofIdealTop 📖	CompOp	4 math math: equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.ker_of_isAffine, coe_support_ofIdealTop, ofIdealTop_ideal
ofIdeals 📖	CompOp	4 math math: ofIdeals_ideal, le_ofIdeals_iff, ofIdeals_mono, ideal_ofIdeals_le
radical 📖	CompOp	9 math math: radical_sup, radical_bot, support_radical, radical_mul, radical_inf, le_radical, vanishingIdeal_support, radical_ideal, radical_top
support 📖	CompOp	32 math math: AlgebraicGeometry.Scheme.support_nilradical, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, gc, support_radical, support_mul, coe_support_mkOfMemSupportIff, range_glueDataObjι_ι_eq_support_inter, mem_support_iff_of_mem, range_subschemeι, mem_support_iff, le_support_iff_le_vanishingIdeal, coe_support_ofIdealTop, support_antitone, support_eq_top_iff, mem_supportSet_iff_mem_support, support_comap, support_eq_bot_iff, support_iSup, support_pow_succ, coe_support_eq_eq_iInter_zeroLocus, support_map, vanishingIdeal_support, AlgebraicGeometry.Scheme.Hom.range_subset_ker_support, coe_support_inter, AlgebraicGeometry.Scheme.Hom.support_ker, support_top, support_pow, coe_support_vanishingIdeal, support_bot, support_sup, support_sSup, subschemeι_apply
supportSet 📖	CompOp	8 math math: mem_supportSet_iff, mem_supportSet_iff_mem_support, isClosed_supportSet, supportSet_subset_zeroLocus, zeroLocus_inter_subset_supportSet, mem_supportSet_iff_of_mem, supportSet_inter, supportSet_eq_iInter_zeroLocus
vanishingIdeal 📖	CompOp	12 math math: gc, vanishingIdeal_ideal, le_support_iff_le_vanishingIdeal, vanishingIdeal_sup, map_vanishingIdeal, vanishingIdeal_support, vanishingIdeal_top, coe_support_vanishingIdeal, vanishingIdeal_iSup, vanishingIdeal_sSup, vanishingIdeal_bot, vanishingIdeal_antimono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_sup 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instAdd SemilatticeSup.toMax IdemSemiring.toSemilatticeSup IdemCommSemiring.toIdemSemiring instIdemCommSemiring	—	—
bot_mul 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instMul Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot	—	ext Ideal.ext Submodule.bot_mul IsScalarTower.right
coe_support_eq_eq_iInter_zeroLocus 📖	mathematical	—	SetLike.coe TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike support Set.iInter Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.Scheme.zeroLocus Set Set.instMembership Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	supportSet_eq_iInter_zeroLocus
coe_support_inter 📖	mathematical	—	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instInter SetLike.coe TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike support AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.Scheme.zeroLocus Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	supportSet_inter
coe_support_mkOfMemSupportIff 📖	mathematical	Ideal.map 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.Scheme.basicOpen RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.homOfLE AlgebraicGeometry.Scheme.basicOpen_le AlgebraicGeometry.Scheme.affineBasicOpen AlgebraicGeometry.Scheme.zeroLocus SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	TopologicalSpace.Closeds TopologicalSpace.Closeds.instSetLike support mkOfMemSupportIff	—	AlgebraicGeometry.Scheme.basicOpen_le
coe_support_ofIdealTop 📖	mathematical	—	SetLike.coe TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike support ofIdealTop AlgebraicGeometry.Scheme.zeroLocus Top.top AlgebraicGeometry.Scheme.Opens OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
coe_support_vanishingIdeal 📖	mathematical	—	SetLike.coe TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike support vanishingIdeal	—	—
equivOfIsAffine_apply 📖	mathematical	—	DFunLike.coe OrderRingIso AlgebraicGeometry.Scheme.IdealSheafData 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing instMul instAdd Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Submodule.pointwiseAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instPartialOrder Submodule.instPartialOrder EquivLike.toFunLike OrderRingIso.instEquivLike equivOfIsAffine ideal Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.isAffineOpen_top	—	IsScalarTower.right
equivOfIsAffine_symm_apply 📖	mathematical	—	DFunLike.coe OrderRingIso 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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing AlgebraicGeometry.Scheme.IdealSheafData Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Submodule.pointwiseAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instMul instAdd Submodule.instPartialOrder instPartialOrder EquivLike.toFunLike OrderRingIso.instEquivLike OrderRingIso.symm equivOfIsAffine ofIdealTop	—	IsScalarTower.right
ext 📖	—	ideal	—	—	AlgebraicGeometry.Scheme.basicOpen_le
ext_iff 📖	mathematical	—	ideal	—	ext
ext_of_iSup_eq_top 📖	—	iSup AlgebraicGeometry.Scheme.Opens ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice 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.affineOpens Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder ideal	—	—	LE.le.antisymm le_of_iSup_eq_top
ext_of_isAffine 📖	—	ideal AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.isAffineOpen_top	—	—	AlgebraicGeometry.isAffineOpen_top LE.le.antisymm le_of_isAffine Eq.le Eq.ge
gc 📖	mathematical	—	GaloisConnection AlgebraicGeometry.Scheme.IdealSheafData OrderDual TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier PartialOrder.toPreorder instPartialOrder OrderDual.instPreorder TopologicalSpace.Closeds.instPartialOrder support vanishingIdeal	—	le_support_iff_le_vanishingIdeal
ideal_biInf 📖	mathematical	—	ideal iInf AlgebraicGeometry.Scheme.IdealSheafData ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set Set.instMembership Pi.infSet Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	Set.Finite.induction_on iInf_congr_Prop iInf_neg iInf_top iInf_insert
ideal_bot 📖	mathematical	—	ideal Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot Pi.instBotForall Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	—
ideal_iInf 📖	mathematical	—	ideal iInf AlgebraicGeometry.Scheme.IdealSheafData ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Pi.infSet Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	iInf_congr_Prop iInf_pos ideal_biInf Set.finite_univ
ideal_iSup 📖	mathematical	—	ideal iSup AlgebraicGeometry.Scheme.IdealSheafData ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Pi.supSet Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	sSup_range ideal_sSup Set.range_comp
ideal_inf 📖	mathematical	—	ideal AlgebraicGeometry.Scheme.IdealSheafData SemilatticeInf.toMin instSemilatticeInf Pi.instMinForall_mathlib Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instMin NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	—
ideal_le_comap_ideal 📖	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	Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal Ideal.comap RingHom RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Subtype.preorder CategoryTheory.homOfLE RingHom.instRingHomClass	—	RingHom.instRingHomClass Ideal.map_le_iff_le_comap map_ideal le_refl
ideal_mono 📖	mathematical	—	Monotone AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder instPartialOrder Pi.preorder Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule ideal	—	StrictMono.monotone strictMono_ideal
ideal_mul 📖	mathematical	—	ideal AlgebraicGeometry.Scheme.IdealSheafData instMul Pi.instMul Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id	—	—
ideal_ofIdeals_le 📖	mathematical	—	Pi.hasLe Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Preorder.toLE Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule ideal ofIdeals	—	sSup_le Set.forall_mem_image
ideal_pow 📖	mathematical	—	ideal AlgebraicGeometry.Scheme.IdealSheafData instPowNat Pi.instPow Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPowNat Semiring.toModule IsScalarTower.right Algebra.id	—	—
ideal_sSup 📖	mathematical	—	ideal SupSet.sSup AlgebraicGeometry.Scheme.IdealSheafData ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Pi.supSet Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.completeLattice NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Set.image	—	—
ideal_sup 📖	mathematical	—	ideal AlgebraicGeometry.Scheme.IdealSheafData SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Pi.instMaxForall_mathlib Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id	—	—
ideal_top 📖	mathematical	—	ideal Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop Pi.instTopForall Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	—
inf_mul 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	ext add_mul IsScalarTower.right Distrib.rightDistribClass
instIsOrderedRing 📖	mathematical	—	IsOrderedRing AlgebraicGeometry.Scheme.IdealSheafData IdemSemiring.toSemiring IdemCommSemiring.toIdemSemiring instIdemCommSemiring instPartialOrder	—	IdemSemiring.toIsOrderedAddMonoid CanonicallyOrderedAdd.toZeroLEOneClass IdemSemiring.toCanonicallyOrderedAdd MulLeftMono.toPosMulMono CanonicallyOrderedAdd.toMulLeftMono MulRightMono.toMulPosMono covariant_swap_mul_of_covariant_mul
isClosed_supportSet 📖	mathematical	—	IsClosed TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier supportSet	—	TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage AlgebraicGeometry.iSup_affineOpens_eq_top IsClosed.isOpen_compl AlgebraicGeometry.Scheme.zeroLocus_isClosed Function.Injective.image_injective Subtype.val_injective Set.image_preimage_eq_inter_range Subtype.range_coe_subtype supportSet_inter
le_def 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder 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 TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal	—	—
le_ofIdeals_iff 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder ofIdeals Pi.hasLe Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule ideal	—	GaloisConnection.le_iff_le GaloisCoinsertion.gc
le_of_iSup_eq_top 📖	mathematical	iSup AlgebraicGeometry.Scheme.Opens ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice 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.affineOpens Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal	AlgebraicGeometry.Scheme.IdealSheafData instPartialOrder	—	TopologicalSpace.Opens.mem_iSup Eq.ge Set.mem_univ AlgebraicGeometry.exists_basicOpen_le_affine_inter AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen Submodule.le_of_isLocalized_span instIsLocalizedModuleLinearMapOfIsLocalization IsScalarTower.right AlgebraicGeometry.Scheme.basicOpen_le Submodule.restrictScalars_localized' Submodule.restrictScalars.congr_simp Ideal.localized'_eq_map AlgebraicGeometry.IsAffineOpen.basicOpen map_ideal Mathlib.Tactic.DepRewrite.nddcongrArg Ideal.map_mono
le_of_isAffine 📖	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 Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.isAffineOpen_top CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule ideal	AlgebraicGeometry.Scheme.IdealSheafData instPartialOrder	—	AlgebraicGeometry.isAffineOpen_top le_top map_ideal Ideal.map_mono
le_radical 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData Preorder.toLE PartialOrder.toPreorder instPartialOrder radical	—	Ideal.le_radical
le_support_iff_le_vanishingIdeal 📖	mathematical	—	TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Closeds.instPartialOrder support AlgebraicGeometry.Scheme.IdealSheafData instPartialOrder vanishingIdeal	—	TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open AlgebraicGeometry.Scheme.isBasis_affineOpens Set.mem_univ isOpen_univ coe_support_inter Set.image_subset_image_iff Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding AlgebraicGeometry.Scheme.Hom.isOpenEmbedding AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec Set.image_preimage_eq_inter_range AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus AlgebraicGeometry.IsAffineOpen.range_fromSpec
map_ideal 📖	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	Ideal.map CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Subtype.preorder CategoryTheory.homOfLE ideal	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.IsAffineOpen.ideal_ext_iff AlgebraicGeometry.exists_basicOpen_le_affine_inter Eq.trans_le AlgebraicGeometry.Scheme.affineBasicOpen_le Ideal.map_map AlgebraicGeometry.Scheme.basicOpen_le TopCat.Presheaf.germ_res' TopCat.Presheaf.germ_res map_ideal_basicOpen
map_ideal' 📖	mathematical	—	Ideal.map 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 RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Functor.map ideal	—	map_ideal
map_ideal_basicOpen 📖	mathematical	—	Ideal.map 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.Scheme.basicOpen RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.homOfLE AlgebraicGeometry.Scheme.basicOpen_le ideal AlgebraicGeometry.Scheme.affineBasicOpen	—	—
mem_supportSet_iff 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set Set.instMembership supportSet AlgebraicGeometry.Scheme.zeroLocus AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens SetLike.coe Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	Set.ext_iff supportSet_eq_iInter_zeroLocus Set.mem_iInter
mem_supportSet_iff_mem_support 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set Set.instMembership supportSet TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Closeds.instSetLike support	—	—
mem_supportSet_iff_of_mem 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens	supportSet AlgebraicGeometry.Scheme.zeroLocus SetLike.coe Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	Set.iInter_subset supportSet_eq_iInter_zeroLocus zeroLocus_inter_subset_supportSet
mem_support_iff 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SetLike.instMembership TopologicalSpace.Closeds.instSetLike support Set Set.instMembership AlgebraicGeometry.Scheme.zeroLocus AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens SetLike.coe Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	Set.ext_iff supportSet_eq_iInter_zeroLocus Set.mem_iInter
mem_support_iff_of_mem 📖	mathematical	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Scheme.Opens SetLike.instMembership TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens	TopologicalSpace.Closeds TopologicalSpace.Closeds.instSetLike support AlgebraicGeometry.Scheme.zeroLocus SetLike.coe Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	supportSet_inter
mkOfMemSupportIff_ideal 📖	mathematical	Ideal.map 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.Scheme.basicOpen RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.homOfLE AlgebraicGeometry.Scheme.basicOpen_le AlgebraicGeometry.Scheme.affineBasicOpen AlgebraicGeometry.Scheme.zeroLocus SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	ideal mkOfMemSupportIff	—	AlgebraicGeometry.Scheme.basicOpen_le
mul_bot 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instMul Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot	—	ext Ideal.ext Submodule.mul_bot IsScalarTower.right
mul_inf 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	ext mul_add IsScalarTower.right Distrib.leftDistribClass
mul_top 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instMul Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop	—	ext Ideal.ext Ideal.mul_top Ideal.instIsTwoSided_1
ofIdealTop_ideal 📖	mathematical	—	ideal ofIdealTop Ideal.map CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set Set.instMembership AlgebraicGeometry.Scheme.affineOpens RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.Hom.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.homOfLE	—	—
ofIdeals_ideal 📖	mathematical	—	ofIdeals ideal	—	GaloisCoinsertion.u_l_eq
ofIdeals_mono 📖	mathematical	—	Monotone AlgebraicGeometry.Scheme.IdealSheafData Pi.preorder Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule instPartialOrder ofIdeals	—	GaloisConnection.monotone_u GaloisCoinsertion.gc
one_eq_top 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instOne Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop	—	—
radical_bot 📖	mathematical	—	radical Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot AlgebraicGeometry.Scheme.nilradical	—	—
radical_ideal 📖	mathematical	—	ideal radical Ideal.radical 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 CommRing.toCommSemiring CommRingCat.commRing	—	—
radical_inf 📖	mathematical	—	radical AlgebraicGeometry.Scheme.IdealSheafData SemilatticeInf.toMin instSemilatticeInf	—	ext Ideal.radical_inf
radical_mul 📖	mathematical	—	radical AlgebraicGeometry.Scheme.IdealSheafData instMul SemilatticeInf.toMin instSemilatticeInf	—	ext Ideal.radical_mul
radical_sup 📖	mathematical	—	radical AlgebraicGeometry.Scheme.IdealSheafData SemilatticeSup.toMax IdemSemiring.toSemilatticeSup IdemCommSemiring.toIdemSemiring instIdemCommSemiring	—	ext Ideal.radical_sup
radical_top 📖	mathematical	—	radical Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop	—	top_le_iff le_radical
strictMono_ideal 📖	mathematical	—	StrictMono AlgebraicGeometry.Scheme.IdealSheafData PartialOrder.toPreorder instPartialOrder Pi.preorder Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens 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 TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op Set Set.instMembership CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule ideal	—	GaloisCoinsertion.strictMono_l
supportSet_eq_iInter_zeroLocus 📖	mathematical	—	supportSet Set.iInter TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.Elem AlgebraicGeometry.Scheme.Opens AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.Scheme.zeroLocus Set Set.instMembership SetLike.coe Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	—
supportSet_inter 📖	mathematical	—	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instInter supportSet SetLike.coe AlgebraicGeometry.Scheme.Opens TopologicalSpace.Opens.instSetLike AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Set.instMembership AlgebraicGeometry.Scheme.affineOpens AlgebraicGeometry.Scheme.zeroLocus Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	Set.ext mem_supportSet_iff_of_mem
supportSet_subset_zeroLocus 📖	mathematical	—	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset supportSet AlgebraicGeometry.Scheme.zeroLocus AlgebraicGeometry.Scheme.Opens Set.instMembership AlgebraicGeometry.Scheme.affineOpens SetLike.coe Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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	—	Eq.trans_subset supportSet_eq_iInter_zeroLocus Set.iInter_subset
support_antitone 📖	mathematical	—	Antitone AlgebraicGeometry.Scheme.IdealSheafData TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier PartialOrder.toPreorder instPartialOrder TopologicalSpace.Closeds.instPartialOrder support	—	SetLike.coe_subset_coe instIsConcreteLE coe_support_eq_eq_iInter_zeroLocus Set.iInter_mono AlgebraicGeometry.Scheme.zeroLocus_mono
support_bot 📖	mathematical	—	support Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot Top.top TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra Order.Coframe.toCoheytingAlgebra TopologicalSpace.Closeds.instCoframe CoheytingAlgebra.toOrderTop	—	—
support_eq_bot_iff 📖	mathematical	—	support Bot.bot TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Closeds.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop instPartialOrder instOrderTop	—	top_le_iff Eq.trans_subset AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus HasSubset.Subset.trans Set.instIsTransSubset zeroLocus_inter_subset_supportSet Eq.le PrimeSpectrum.zeroLocus_empty_iff_eq_top Set.image_congr
support_eq_top_iff 📖	mathematical	—	support Top.top TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra Order.Coframe.toCoheytingAlgebra TopologicalSpace.Closeds.instCoframe CoheytingAlgebra.toOrderTop Bot.bot AlgebraicGeometry.Scheme.IdealSheafData OrderBot.toBot instPartialOrder instOrderBot	—	top_le_iff le_support_iff_le_vanishingIdeal vanishingIdeal_top AlgebraicGeometry.Scheme.nilradical_eq_bot le_bot_iff
support_iSup 📖	mathematical	—	support iSup AlgebraicGeometry.Scheme.IdealSheafData ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice iInf TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf TopologicalSpace.Closeds.instCompleteLattice	—	GaloisConnection.l_iSup gc
support_mul 📖	mathematical	—	support AlgebraicGeometry.Scheme.IdealSheafData instMul TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Closeds.instCompleteLattice	—	—
support_pow 📖	mathematical	—	support AlgebraicGeometry.Scheme.IdealSheafData instPowNat	—	—
support_pow_succ 📖	mathematical	—	support AlgebraicGeometry.Scheme.IdealSheafData instPowNat	—	—
support_radical 📖	mathematical	—	support radical	—	—
support_sSup 📖	mathematical	—	support SupSet.sSup AlgebraicGeometry.Scheme.IdealSheafData ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice iInf TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf TopologicalSpace.Closeds.instCompleteLattice Set Set.instMembership	—	GaloisConnection.l_sSup gc
support_sup 📖	mathematical	—	support AlgebraicGeometry.Scheme.IdealSheafData SemilatticeSup.toMax IdemSemiring.toSemilatticeSup IdemCommSemiring.toIdemSemiring instIdemCommSemiring TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Closeds.instCompleteLattice	—	GaloisConnection.l_sup gc
support_top 📖	mathematical	—	support Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop Bot.bot TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderBot.toBot SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Closeds.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
top_mul 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instMul Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderTop	—	ext Ideal.ext Ideal.top_mul
vanishingIdeal_antimono 📖	mathematical	TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Closeds.instPartialOrder	AlgebraicGeometry.Scheme.IdealSheafData instPartialOrder vanishingIdeal	—	GaloisConnection.monotone_u gc
vanishingIdeal_bot 📖	mathematical	—	vanishingIdeal Bot.bot TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Closeds.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Top.top AlgebraicGeometry.Scheme.IdealSheafData OrderTop.toTop instPartialOrder instOrderTop	—	GaloisConnection.u_top gc
vanishingIdeal_iSup 📖	mathematical	—	vanishingIdeal iSup TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Closeds.instCompleteLattice iInf AlgebraicGeometry.Scheme.IdealSheafData ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf instCompleteLattice	—	GaloisConnection.u_iInf gc
vanishingIdeal_ideal 📖	mathematical	—	ideal vanishingIdeal PrimeSpectrum.vanishingIdeal 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 CommRing.toCommSemiring CommRingCat.commRing Set.preimage PrimeSpectrum DFunLike.coe ContinuousMap AlgebraicGeometry.Spec ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.IsAffineOpen.fromSpec SetLike.coe TopologicalSpace.Closeds AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier TopologicalSpace.Closeds.instSetLike	—	—
vanishingIdeal_sSup 📖	mathematical	—	vanishingIdeal SupSet.sSup TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Closeds.instCompleteLattice iInf AlgebraicGeometry.Scheme.IdealSheafData ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf instCompleteLattice Set Set.instMembership	—	GaloisConnection.u_sInf gc
vanishingIdeal_sup 📖	mathematical	—	vanishingIdeal TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Closeds.instCompleteLattice AlgebraicGeometry.Scheme.IdealSheafData SemilatticeInf.toMin instSemilatticeInf	—	GaloisConnection.u_inf gc
vanishingIdeal_support 📖	mathematical	—	vanishingIdeal support radical	—	ext PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical Function.Injective.image_injective Topology.IsEmbedding.injective Topology.IsOpenEmbedding.toIsEmbedding AlgebraicGeometry.Scheme.Hom.isOpenEmbedding AlgebraicGeometry.IsAffineOpen.isOpenImmersion_fromSpec Set.image_preimage_eq_inter_range AlgebraicGeometry.IsAffineOpen.range_fromSpec AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus coe_support_inter
vanishingIdeal_top 📖	mathematical	—	vanishingIdeal Top.top TopologicalSpace.Closeds TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra Order.Coframe.toCoheytingAlgebra TopologicalSpace.Closeds.instCoframe CoheytingAlgebra.toOrderTop AlgebraicGeometry.Scheme.nilradical	—	support_bot vanishingIdeal_support AlgebraicGeometry.Scheme.nilradical.eq_1
zeroLocus_inter_subset_supportSet 📖	mathematical	—	Set TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace Set.instHasSubset Set.instInter AlgebraicGeometry.Scheme.zeroLocus AlgebraicGeometry.Scheme.Opens Set.instMembership AlgebraicGeometry.Scheme.affineOpens SetLike.coe Ideal CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.str 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 supportSet	—	supportSet_eq_iInter_zeroLocus Set.subset_iInter Codisjoint.left_le_of_le_inf_right Codisjoint.symm AlgebraicGeometry.Scheme.codisjoint_zeroLocus AlgebraicGeometry.exists_basicOpen_le_affine_inter AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen Eq.trans_le AlgebraicGeometry.Scheme.basicOpen_le Eq.le map_ideal Ideal.mem_map_of_mem IsLocalization.mem_map_algebraMap_iff map_ideal_basicOpen pow_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one AlgebraicGeometry.Scheme.basicOpen_res map_pow AlgebraicGeometry.Scheme.basicOpen_mul AlgebraicGeometry.Scheme.basicOpen_pow IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd inf_of_le_left
zero_eq_bot 📖	mathematical	—	AlgebraicGeometry.Scheme.IdealSheafData instZero Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBot	—	—

AlgebraicGeometry.Scheme.IdealSheafData.Simps

Definitions

Name	Category	Theorems
coe_support 📖	CompOp	—

---

← Back to Index