Ideal

📁 Source: Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean

Statistics

Metric	Count
Definitions `HomogeneousIdeal`, `completeLattice`, `instAdd`, `instBot`, `instInfSet`, `instInhabited`, `instMax`, `instMin`, `instSupSet`, `instTop`, `irrelevant`, `setLike`, `toIdeal`, `IsHomogeneous`, `homogeneousCore`, `homogeneousCore'`, `gi`, `homogeneousHull`, `gi`, `instMulHomogeneousIdeal`, `instPartialOrderHomogeneousIdeal`	21
Theorems `coe_bot`, `coe_inf`, `coe_sup`, `coe_top`, `eq_bot_iff`, `eq_top_iff`, `ext`, `ext'`, `ext_iff`, `homogeneousHull_toIdeal_eq_self`, `irrelevant_eq_closure`, `irrelevant_eq_iSup`, `irrelevant_eq_span`, `irrelevant_le`, `isHomogeneous`, `mem_iff`, `mem_irrelevant_iff`, `mem_irrelevant_of_mem`, `toAddSubmonoid_irrelevant_le`, `toIdeal_add`, `toIdeal_bot`, `toIdeal_homogeneousCore_eq_self`, `toIdeal_iInf`, `toIdeal_iInf₂`, `toIdeal_iSup`, `toIdeal_iSup₂`, `toIdeal_inf`, `toIdeal_injective`, `toIdeal_irrelevant`, `toIdeal_irrelevant_le`, `toIdeal_mul`, `toIdeal_sInf`, `toIdeal_sSup`, `toIdeal_sup`, `toIdeal_top`, `bot`, `iInf`, `iInf₂`, `iSup`, `iSup₂`, `iff_eq`, `iff_exists`, `inf`, `mem_iff`, `mul`, `sInf`, `sSup`, `sup`, `toIdeal_homogeneousCore_eq_self`, `toIdeal_homogeneousHull_eq_self`, `top`, `homogeneousCore'_eq_sSup`, `homogeneousCore'_le`, `homogeneousCore'_mono`, `gc`, `homogeneousCore_eq_sSup`, `homogeneousCore_mono`, `gc`, `homogeneousHull_eq_iSup`, `homogeneousHull_eq_sInf`, `homogeneousHull_mono`, `homogeneous_span`, `isHomogeneous_iff_forall_subset`, `isHomogeneous_iff_subset_iInter`, `le_toIdeal_homogeneousHull`, `mem_homogeneousCore_of_homogeneous_of_mem`, `mul_homogeneous_element_mem_of_mem`, `toIdeal_homogeneousCore_le`, `toIdeal_homogeneousHull_eq_iSup`	69
Total	90

HomogeneousIdeal

Definitions

Name	Category	Theorems
`completeLattice` 📖	CompOp	—
`instAdd` 📖	CompOp	1 math math: `toIdeal_add`
`instBot` 📖	CompOp	3 math math: `eq_bot_iff`, `coe_bot`, `toIdeal_bot`
`instInfSet` 📖	CompOp	5 math math: `ProjectiveSpectrum.vanishingIdeal_iUnion`, `toIdeal_iInf`, `toIdeal_sInf`, `toIdeal_iInf₂`, `Ideal.homogeneousHull_eq_sInf`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	4 math math: `ProjectiveSpectrum.sup_vanishingIdeal_le`, `coe_sup`, `toIdeal_sup`, `ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal`
`instMin` 📖	CompOp	3 math math: `coe_inf`, `toIdeal_inf`, `ProjectiveSpectrum.vanishingIdeal_union`
`instSupSet` 📖	CompOp	6 math math: `toIdeal_iSup₂`, `toIdeal_sSup`, `Ideal.homogeneousHull_eq_iSup`, `ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal`, `Ideal.homogeneousCore_eq_sSup`, `toIdeal_iSup`
`instTop` 📖	CompOp	4 math math: `toIdeal_top`, `coe_top`, `eq_top_iff`, `ProjectiveSpectrum.vanishingIdeal_univ`
`irrelevant` 📖	CompOp	11 math math: `mem_irrelevant_of_mem`, `toAddSubmonoid_irrelevant_le`, `ProjectiveSpectrum.not_irrelevant_le`, `irrelevant_le`, `mem_irrelevant_iff`, `irrelevant_eq_span`, `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant`, `irrelevant_eq_iSup`, `irrelevant_eq_closure`, `toIdeal_irrelevant_le`, `toIdeal_irrelevant`
`setLike` 📖	CompOp	28 math math: `ProjectiveSpectrum.mem_basicOpen`, `ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal`, `ProjectiveSpectrum.gc_homogeneousIdeal`, `ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal`, `ProjectiveSpectrum.mem_vanishingIdeal`, `mem_irrelevant_of_mem`, `coe_bot`, `AlgebraicGeometry.Proj.mem_basicOpen`, `coe_inf`, `ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal`, `ProjectiveSpectrum.mem_zeroLocus`, `ProjectiveSpectrum.gc_set`, `mem_irrelevant_iff`, `ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply`, `coe_sup`, `ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure`, `AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier`, `coe_top`, `ProjectiveSpectrum.zeroLocus_anti_mono_homogeneousIdeal`, `ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal`, `ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal`, `ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem`, `ProjectiveSpectrum.subset_vanishingIdeal_zeroLocus`, `ProjectiveSpectrum.mem_coe_basicOpen`, `Ideal.mem_homogeneousCore_of_homogeneous_of_mem`, `ProjectiveSpectrum.coe_vanishingIdeal`, `mem_iff`
`toIdeal` 📖	CompOp	64 math math: `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply`, `toIdeal_mul`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv`, `AlgebraicGeometry.Proj.pow_apply`, `AlgebraicGeometry.Proj.mul_apply`, `toIdeal_add`, `toIdeal_iInf`, `AlgebraicGeometry.Proj.one_apply`, `eq_bot_iff`, `toIdeal_homogeneousCore_eq_self`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk`, `AlgebraicGeometry.Proj.sub_apply`, `AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk`, `toIdeal_bot`, `ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal`, `toIdeal_iSup₂`, `ProjectiveSpectrum.isPrime`, `Ideal.homogeneousHull.gc`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime`, `AlgebraicGeometry.germ_comp_stalkToFiberRingHom`, `coe_radical`, `toIdeal_sSup`, `toIdeal_injective`, `toIdeal_sInf`, `Ideal.le_toIdeal_homogeneousHull`, `isHomogeneous`, `AlgebraicGeometry.Proj.zero_apply`, `toIdeal_top`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem'`, `Ideal.IsPrime.homogeneousCore`, `Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self`, `AlgebraicGeometry.Proj.ext_iff`, `ProjectiveSpectrum.gc_ideal`, `toIdeal_sup`, `AlgebraicGeometry.Proj.add_apply`, `Ideal.IsHomogeneous.iff_eq`, `irrelevant_eq_span`, `ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal`, `ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus`, `AlgebraicGeometry.stalkToFiberRingHom_germ`, `toIdeal_iInf₂`, `homogeneousHull_toIdeal_eq_self`, `Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self`, `AlgebraicGeometry.Proj.stalkIso'_germ`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ`, `AlgebraicGeometry.mem_basicOpen_den`, `AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem'`, `Ideal.homogeneousCore_eq_sSup`, `toIdeal_irrelevant_le`, `eq_top_iff`, `AlgebraicGeometry.Proj.res_apply`, `Ideal.toIdeal_homogeneousCore_le`, `Ideal.toIdeal_homogeneousHull_eq_iSup`, `Ideal.homogeneousHull_eq_sInf`, `AlgebraicGeometry.Proj.stalkIso'_symm_mk`, `toIdeal_inf`, `toIdeal_iSup`, `toIdeal_irrelevant`, `mem_iff`, `ext_iff`, `Ideal.homogeneousCore.gc`, `AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`SetLike.coe` `HomogeneousIdeal` `setLike` `Bot.bot` `instBot` `Set` `Set.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `HomogeneousIdeal` `setLike` `instMin` `Set` `Set.instInter`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `HomogeneousIdeal` `setLike` `instMax` `Set` `Set.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Submodule.coe_sup`
`coe_top` 📖	mathematical	—	`SetLike.coe` `HomogeneousIdeal` `setLike` `Top.top` `instTop` `Set.univ`	—	—
`eq_bot_iff` 📖	mathematical	—	`Bot.bot` `HomogeneousIdeal` `instBot` `toIdeal` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`toIdeal_injective`
`eq_top_iff` 📖	mathematical	—	`Top.top` `HomogeneousIdeal` `instTop` `toIdeal` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`toIdeal_injective`
`ext` 📖	—	`toIdeal`	—	—	`toIdeal_injective`
`ext'` 📖	—	`HomogeneousIdeal` `SetLike.instMembership` `setLike`	—	—	`HomogeneousSubmodule.ext'` `SetLike.GradedMul.toGradedSMul` `GradedRing.toGradedMonoid`
`ext_iff` 📖	mathematical	—	`toIdeal`	—	`ext`
`homogeneousHull_toIdeal_eq_self` 📖	mathematical	—	`Ideal.homogeneousHull` `toIdeal`	—	`toIdeal_injective` `Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self` `isHomogeneous`
`irrelevant_eq_closure` 📖	mathematical	—	`Submodule.toAddSubmonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HomogeneousSubmodule.toSubmodule` `AddCommMonoid.toAddMonoid` `GradedRing.toDecomposition` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `irrelevant` `AddSubmonoid.closure` `AddMonoid.toAddZeroClass` `Set.iUnion` `Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `SetLike.coe`	—	`irrelevant_eq_iSup` `le_antisymm` `iSup_le` `AddSubmonoid.subset_closure` `Set.mem_biUnion` `AddSubmonoid.closure_le` `Set.iUnion_subset` `le_biSup`
`irrelevant_eq_iSup` 📖	mathematical	—	`Submodule.toAddSubmonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HomogeneousSubmodule.toSubmodule` `AddCommMonoid.toAddMonoid` `GradedRing.toDecomposition` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `irrelevant` `iSup` `AddSubmonoid` `AddMonoid.toAddZeroClass` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `AddSubmonoid.instCompleteLattice` `Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddSubmonoid.ofClass`	—	`le_antisymm` `AddSubmonoidClass.toZeroMemClass` `DirectSum.sum_support_decompose` `sum_mem` `AddSubmonoid.instAddSubmonoidClass` `DFinsupp.mem_support_iff` `RingHom.instRingHomClass` `AddSubmonoid.mem_iSup_of_mem` `pos_of_ne_zero` `Subtype.prop` `iSup₂_le` `mem_irrelevant_of_mem`
`irrelevant_eq_span` 📖	mathematical	—	`toIdeal` `AddCommMonoid.toAddMonoid` `irrelevant` `Ideal.span` `Set.iUnion` `Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SetLike.coe`	—	`le_antisymm` `Eq.trans_le` `irrelevant_eq_closure` `AddSubmonoid.closure_le` `Ideal.subset_span` `Ideal.span_le` `Set.iUnion_subset` `mem_irrelevant_of_mem`
`irrelevant_le` 📖	mathematical	—	`HomogeneousIdeal` `AddCommMonoid.toAddMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `irrelevant` `AddSubmonoid` `AddMonoid.toAddZeroClass` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddSubmonoid.instPartialOrder` `AddSubmonoid.ofClass` `Submodule.toAddSubmonoid` `Semiring.toModule` `HomogeneousSubmodule.toSubmodule` `GradedRing.toDecomposition` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`toIdeal_irrelevant_le`
`isHomogeneous` 📖	mathematical	—	`Ideal.IsHomogeneous` `toIdeal`	—	`HomogeneousSubmodule.is_homogeneous'`
`mem_iff` 📖	mathematical	—	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `toIdeal` `HomogeneousIdeal` `setLike`	—	—
`mem_irrelevant_iff` 📖	mathematical	—	`HomogeneousIdeal` `AddCommMonoid.toAddMonoid` `SetLike.instMembership` `setLike` `irrelevant` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `AddMonoidHom.instFunLike` `GradedRing.proj` `AddZero.toZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—
`mem_irrelevant_of_mem` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SetLike.instMembership`	`HomogeneousIdeal` `setLike` `irrelevant`	—	`mem_irrelevant_iff` `GradedRing.proj_apply` `DirectSum.decompose_of_mem` `DirectSum.of_eq_of_ne` `ZeroMemClass.coe_zero`
`toAddSubmonoid_irrelevant_le` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `AddSubmonoid.instPartialOrder` `Submodule.toAddSubmonoid` `Semiring.toModule` `HomogeneousSubmodule.toSubmodule` `GradedRing.toDecomposition` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `irrelevant` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddSubmonoid.ofClass`	—	`irrelevant_eq_iSup` `iSup₂_le_iff`
`toIdeal_add` 📖	mathematical	—	`toIdeal` `HomogeneousIdeal` `instAdd` `Ideal` `Submodule.pointwiseAdd` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`toIdeal_bot` 📖	mathematical	—	`toIdeal` `Bot.bot` `HomogeneousIdeal` `instBot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`toIdeal_homogeneousCore_eq_self` 📖	mathematical	—	`Ideal.homogeneousCore` `toIdeal`	—	`ext` `Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self` `isHomogeneous`
`toIdeal_iInf` 📖	mathematical	—	`toIdeal` `iInf` `HomogeneousIdeal` `instInfSet` `Ideal` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`iInf.eq_1` `toIdeal_sInf` `iInf_range`
`toIdeal_iInf₂` 📖	mathematical	—	`toIdeal` `iInf` `HomogeneousIdeal` `instInfSet` `Ideal` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`toIdeal_iInf`
`toIdeal_iSup` 📖	mathematical	—	`toIdeal` `iSup` `HomogeneousIdeal` `instSupSet` `Ideal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`iSup.eq_1` `toIdeal_sSup` `iSup_range`
`toIdeal_iSup₂` 📖	mathematical	—	`toIdeal` `iSup` `HomogeneousIdeal` `instSupSet` `Ideal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`toIdeal_iSup`
`toIdeal_inf` 📖	mathematical	—	`toIdeal` `HomogeneousIdeal` `instMin` `Ideal` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`toIdeal_injective` 📖	mathematical	—	`HomogeneousIdeal` `Ideal` `toIdeal`	—	`HomogeneousSubmodule.toSubmodule_injective` `SetLike.GradedMul.toGradedSMul` `GradedRing.toGradedMonoid`
`toIdeal_irrelevant` 📖	mathematical	—	`toIdeal` `AddCommMonoid.toAddMonoid` `irrelevant` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `GradedRing.projZeroRingHom`	—	—
`toIdeal_irrelevant_le` 📖	mathematical	—	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `toIdeal` `AddCommMonoid.toAddMonoid` `irrelevant` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddSubmonoid.instPartialOrder` `AddSubmonoid.ofClass` `Submodule.toAddSubmonoid`	—	`toAddSubmonoid_irrelevant_le`
`toIdeal_mul` 📖	mathematical	—	`toIdeal` `CommSemiring.toSemiring` `HomogeneousIdeal` `instMulHomogeneousIdeal` `Ideal` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id`	—	—
`toIdeal_sInf` 📖	mathematical	—	`toIdeal` `InfSet.sInf` `HomogeneousIdeal` `instInfSet` `iInf` `Ideal` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instMembership`	—	—
`toIdeal_sSup` 📖	mathematical	—	`toIdeal` `SupSet.sSup` `HomogeneousIdeal` `instSupSet` `iSup` `Ideal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instMembership`	—	—
`toIdeal_sup` 📖	mathematical	—	`toIdeal` `HomogeneousIdeal` `instMax` `Ideal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`toIdeal_top` 📖	mathematical	—	`toIdeal` `Top.top` `HomogeneousIdeal` `instTop` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—

Ideal

Definitions

Name	Category	Theorems
`IsHomogeneous` 📖	MathDef	10 math math: `IsHomogeneous.iff_exists`, `isHomogeneous_iff_subset_iInter`, `isHomogeneous_iff_forall_subset`, `IsHomogeneous.bot`, `HomogeneousIdeal.isHomogeneous`, `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.homogeneous`, `IsHomogeneous.iff_eq`, `homogeneousCore'_eq_sSup`, `homogeneous_span`, `IsHomogeneous.top`
`homogeneousCore` 📖	CompOp	9 math math: `HomogeneousIdeal.toIdeal_homogeneousCore_eq_self`, `IsPrime.homogeneousCore`, `IsHomogeneous.iff_eq`, `IsHomogeneous.toIdeal_homogeneousCore_eq_self`, `homogeneousCore_eq_sSup`, `mem_homogeneousCore_of_homogeneous_of_mem`, `homogeneousCore_mono`, `toIdeal_homogeneousCore_le`, `homogeneousCore.gc`
`homogeneousCore'` 📖	CompOp	3 math math: `homogeneousCore'_le`, `homogeneousCore'_eq_sSup`, `homogeneousCore'_mono`
`homogeneousHull` 📖	CompOp	8 math math: `homogeneousHull.gc`, `homogeneousHull_eq_iSup`, `homogeneousHull_mono`, `le_toIdeal_homogeneousHull`, `IsHomogeneous.toIdeal_homogeneousHull_eq_self`, `HomogeneousIdeal.homogeneousHull_toIdeal_eq_self`, `toIdeal_homogeneousHull_eq_iSup`, `homogeneousHull_eq_sInf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homogeneousCore'_eq_sSup` 📖	mathematical	—	`homogeneousCore'` `SupSet.sSup` `Ideal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `setOf` `IsHomogeneous` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`IsLUB.sSup_eq` `IsGreatest.isLUB` `Set.ext` `Set.mem_image` `Set.mem_setOf_eq` `HomogeneousIdeal.isHomogeneous` `Monotone.map_isGreatest` `GaloisConnection.isGreatest_u` `homogeneousCore.gc`
`homogeneousCore'_le` 📖	mathematical	—	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `homogeneousCore'`	—	`span_le` `Set.image_preimage_subset`
`homogeneousCore'_mono` 📖	mathematical	—	`Monotone` `Ideal` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `homogeneousCore'`	—	`span_mono` `Set.image_mono`
`homogeneousCore_eq_sSup` 📖	mathematical	—	`homogeneousCore` `SupSet.sSup` `HomogeneousIdeal` `HomogeneousIdeal.instSupSet` `setOf` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HomogeneousIdeal.toIdeal`	—	`IsLUB.sSup_eq` `IsGreatest.isLUB` `GaloisConnection.isGreatest_u` `homogeneousCore.gc`
`homogeneousCore_mono` 📖	mathematical	—	`Monotone` `Ideal` `HomogeneousIdeal` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instPartialOrderHomogeneousIdeal` `homogeneousCore`	—	`homogeneousCore'_mono`
`homogeneousHull_eq_iSup` 📖	mathematical	—	`homogeneousHull` `iSup` `HomogeneousIdeal` `HomogeneousIdeal.instSupSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `GradedRing.toDecomposition` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `span` `Set.image` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidHom.instFunLike` `GradedRing.proj` `SetLike.coe` `Ideal` `Submodule.setLike` `homogeneous_span`	—	`HomogeneousIdeal.ext` `homogeneous_span` `toIdeal_homogeneousHull_eq_iSup` `HomogeneousIdeal.toIdeal_iSup`
`homogeneousHull_eq_sInf` 📖	mathematical	—	`homogeneousHull` `InfSet.sInf` `HomogeneousIdeal` `HomogeneousIdeal.instInfSet` `setOf` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HomogeneousIdeal.toIdeal`	—	`IsGLB.sInf_eq` `IsLeast.isGLB` `GaloisConnection.isLeast_l` `homogeneousHull.gc`
`homogeneousHull_mono` 📖	mathematical	—	`Monotone` `Ideal` `HomogeneousIdeal` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instPartialOrderHomogeneousIdeal` `homogeneousHull`	—	`span_mono`
`homogeneous_span` 📖	mathematical	`SetLike.IsHomogeneousElem`	`IsHomogeneous` `span`	—	`RingHomSurjective.ids` `LinearMap.mem_range` `Finsupp.span_eq_range_linearCombination` `span.eq_1` `Finsupp.linearCombination_apply` `Finsupp.sum.eq_1` `DirectSum.decompose_sum` `DFinsupp.finset_sum_apply` `AddSubmonoidClass.coe_finset_sum` `sum_mem` `smul_eq_mul` `mul_homogeneous_element_mem_of_mem` `subset_span`
`isHomogeneous_iff_forall_subset` 📖	mathematical	—	`IsHomogeneous` `Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set.preimage` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidHom.instFunLike` `GradedRing.proj`	—	—
`isHomogeneous_iff_subset_iInter` 📖	mathematical	—	`IsHomogeneous` `Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set.iInter` `Set.preimage` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidHom.instFunLike` `GradedRing.proj`	—	`Set.subset_iInter_iff`
`le_toIdeal_homogeneousHull` 📖	mathematical	—	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HomogeneousIdeal.toIdeal` `homogeneousHull`	—	`AddSubmonoidClass.toZeroMemClass` `DirectSum.sum_support_decompose` `sum_mem` `subset_span`
`mem_homogeneousCore_of_homogeneous_of_mem` 📖	mathematical	`SetLike.IsHomogeneousElem` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`HomogeneousIdeal` `HomogeneousIdeal.setLike` `homogeneousCore`	—	`subset_span`
`mul_homogeneous_element_mem_of_mem` 📖	mathematical	`SetLike.IsHomogeneousElem` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidHom.instFunLike` `GradedRing.proj` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`AddSubmonoidClass.toZeroMemClass` `DirectSum.sum_support_decompose` `Finset.sum_mul` `map_sum` `AddMonoidHom.instAddMonoidHomClass` `sum_mem` `SetLike.GradedMul.mul_mem` `SetLike.GradedMonoid.toGradedMul` `GradedRing.toGradedMonoid` `SetLike.coe_mem` `GradedRing.proj_apply` `DirectSum.decompose_of_mem` `DirectSum.coe_of_apply` `mul_mem_left` `zero_mem`
`toIdeal_homogeneousCore_le` 📖	mathematical	—	`Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HomogeneousIdeal.toIdeal` `homogeneousCore`	—	`homogeneousCore'_le`
`toIdeal_homogeneousHull_eq_iSup` 📖	mathematical	—	`HomogeneousIdeal.toIdeal` `homogeneousHull` `iSup` `Ideal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `span` `Set.image` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddMonoidHom.instFunLike` `GradedRing.proj` `SetLike.coe` `Submodule.setLike`	—	`span_iUnion` `Set.ext` `Set.image_congr`

Ideal.IsHomogeneous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot` 📖	mathematical	—	`Ideal.IsHomogeneous` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`DirectSum.decompose_zero` `DirectSum.zero_apply` `Ideal.zero_mem`
`iInf` 📖	mathematical	`Ideal.IsHomogeneous`	`iInf` `Ideal` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`iInf₂` 📖	mathematical	`Ideal.IsHomogeneous`	`iInf` `Ideal` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`iInf`
`iSup` 📖	mathematical	`Ideal.IsHomogeneous`	`iSup` `Ideal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`GradedRing.toGradedMonoid` `Set.image_iUnion` `Ideal.span_iUnion`
`iSup₂` 📖	mathematical	`Ideal.IsHomogeneous`	`iSup` `Ideal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`iSup`
`iff_eq` 📖	mathematical	—	`Ideal.IsHomogeneous` `HomogeneousIdeal.toIdeal` `Ideal.homogeneousCore`	—	`toIdeal_homogeneousCore_eq_self` `HomogeneousSubmodule.is_homogeneous'`
`iff_exists` 📖	mathematical	—	`Ideal.IsHomogeneous` `Ideal.span` `Set.image` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `SetLike.homogeneousSubmonoid` `GradedRing.toGradedMonoid`	—	`GradedRing.toGradedMonoid` `iff_eq` `GaloisConnection.exists_eq_l` `GaloisConnection.compose` `Set.image_preimage` `GaloisInsertion.gc`
`inf` 📖	mathematical	`Ideal.IsHomogeneous`	`Ideal` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`mem_iff` 📖	mathematical	`Ideal.IsHomogeneous`	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFinsupp.instDFunLike` `Equiv` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `EquivLike.toFunLike` `Equiv.instEquivLike` `DirectSum.decompose` `GradedRing.toDecomposition`	—	`DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff` `Submodule.addSubmonoidClass`
`mul` 📖	mathematical	`Ideal.IsHomogeneous` `CommSemiring.toSemiring`	`Ideal` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `GradedRing.toGradedMonoid` `iff_exists` `IsScalarTower.left` `Ideal.span_mul_span'` `Ideal.instIsTwoSided` `Set.image_mul` `MonoidHomClass.toMulHomClass` `MonoidHom.instMonoidHomClass`
`sInf` 📖	mathematical	`Ideal.IsHomogeneous`	`InfSet.sInf` `Ideal` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`sInf_eq_iInf` `iInf₂`
`sSup` 📖	mathematical	`Ideal.IsHomogeneous`	`SupSet.sSup` `Ideal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`sSup_eq_iSup` `iSup₂`
`sup` 📖	mathematical	`Ideal.IsHomogeneous`	`Ideal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`GradedRing.toGradedMonoid` `iff_exists` `Set.image_union` `Submodule.span_union`
`toIdeal_homogeneousCore_eq_self` 📖	mathematical	`Ideal.IsHomogeneous`	`HomogeneousIdeal.toIdeal` `Ideal.homogeneousCore`	—	`le_antisymm` `Ideal.homogeneousCore'_le` `AddSubmonoidClass.toZeroMemClass` `DirectSum.sum_support_decompose` `Ideal.sum_mem` `Ideal.subset_span` `SetLike.isHomogeneousElem_coe`
`toIdeal_homogeneousHull_eq_self` 📖	mathematical	`Ideal.IsHomogeneous`	`HomogeneousIdeal.toIdeal` `Ideal.homogeneousHull`	—	`le_antisymm` `Ideal.span_le` `Subtype.prop` `Ideal.le_toIdeal_homogeneousHull`
`top` 📖	mathematical	—	`Ideal.IsHomogeneous` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—

Ideal.homogeneousCore

Definitions

Name	Category	Theorems
`gi` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gc` 📖	mathematical	—	`GaloisConnection` `HomogeneousIdeal` `Ideal` `PartialOrder.toPreorder` `instPartialOrderHomogeneousIdeal` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `HomogeneousIdeal.toIdeal` `Ideal.homogeneousCore`	—	`Ideal.homogeneousCore_mono` `HomogeneousIdeal.toIdeal_homogeneousCore_eq_self` `le_trans` `Ideal.homogeneousCore'_le`

Ideal.homogeneousHull

Definitions

Name	Category	Theorems
`gi` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gc` 📖	mathematical	—	`GaloisConnection` `Ideal` `HomogeneousIdeal` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `instPartialOrderHomogeneousIdeal` `Ideal.homogeneousHull` `HomogeneousIdeal.toIdeal`	—	`le_trans` `Ideal.le_toIdeal_homogeneousHull` `Ideal.homogeneousHull_mono` `HomogeneousIdeal.homogeneousHull_toIdeal_eq_self`

(root)

Definitions

Name	Category	Theorems
`HomogeneousIdeal` 📖	CompOp	59 math math: `ProjectiveSpectrum.mem_basicOpen`, `HomogeneousIdeal.toIdeal_mul`, `ProjectiveSpectrum.subset_zeroLocus_vanishingIdeal`, `ProjectiveSpectrum.gc_homogeneousIdeal`, `ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal`, `ProjectiveSpectrum.vanishingIdeal_iUnion`, `HomogeneousIdeal.toIdeal_add`, `HomogeneousIdeal.toIdeal_iInf`, `ProjectiveSpectrum.sup_vanishingIdeal_le`, `ProjectiveSpectrum.mem_vanishingIdeal`, `HomogeneousIdeal.eq_bot_iff`, `HomogeneousIdeal.mem_irrelevant_of_mem`, `HomogeneousIdeal.coe_bot`, `HomogeneousIdeal.toIdeal_bot`, `HomogeneousIdeal.toIdeal_iSup₂`, `AlgebraicGeometry.Proj.mem_basicOpen`, `ProjectiveSpectrum.not_irrelevant_le`, `HomogeneousIdeal.coe_inf`, `ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal`, `Ideal.homogeneousHull.gc`, `ProjectiveSpectrum.as_ideal_le_as_ideal`, `HomogeneousIdeal.toIdeal_sSup`, `ProjectiveSpectrum.as_ideal_lt_as_ideal`, `HomogeneousIdeal.irrelevant_le`, `ProjectiveSpectrum.mem_zeroLocus`, `ProjectiveSpectrum.gc_set`, `HomogeneousIdeal.mem_irrelevant_iff`, `Ideal.homogeneousHull_eq_iSup`, `HomogeneousIdeal.toIdeal_injective`, `HomogeneousIdeal.toIdeal_sInf`, `Ideal.homogeneousHull_mono`, `HomogeneousIdeal.toIdeal_top`, `ProjectiveSpectrum.vanishingIdeal_anti_mono`, `ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus`, `AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply`, `HomogeneousIdeal.coe_sup`, `HomogeneousIdeal.toIdeal_sup`, `ProjectiveSpectrum.zeroLocus_vanishingIdeal_eq_closure`, `AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier`, `HomogeneousIdeal.coe_top`, `HomogeneousIdeal.toIdeal_iInf₂`, `ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal`, `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant`, `ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal`, `ProjectiveSpectrum.mem_compl_zeroLocus_iff_notMem`, `ProjectiveSpectrum.subset_vanishingIdeal_zeroLocus`, `ProjectiveSpectrum.mem_coe_basicOpen`, `Ideal.homogeneousCore_eq_sSup`, `Ideal.mem_homogeneousCore_of_homogeneous_of_mem`, `Ideal.homogeneousCore_mono`, `HomogeneousIdeal.eq_top_iff`, `Ideal.homogeneousHull_eq_sInf`, `HomogeneousIdeal.toIdeal_inf`, `ProjectiveSpectrum.coe_vanishingIdeal`, `HomogeneousIdeal.toIdeal_iSup`, `HomogeneousIdeal.mem_iff`, `ProjectiveSpectrum.vanishingIdeal_union`, `Ideal.homogeneousCore.gc`, `ProjectiveSpectrum.vanishingIdeal_univ`
`instMulHomogeneousIdeal` 📖	CompOp	2 math math: `HomogeneousIdeal.toIdeal_mul`, `ProjectiveSpectrum.zeroLocus_mul_homogeneousIdeal`
`instPartialOrderHomogeneousIdeal` 📖	CompOp	13 math math: `ProjectiveSpectrum.gc_homogeneousIdeal`, `ProjectiveSpectrum.sup_vanishingIdeal_le`, `ProjectiveSpectrum.not_irrelevant_le`, `Ideal.homogeneousHull.gc`, `ProjectiveSpectrum.as_ideal_le_as_ideal`, `ProjectiveSpectrum.as_ideal_lt_as_ideal`, `HomogeneousIdeal.irrelevant_le`, `Ideal.homogeneousHull_mono`, `ProjectiveSpectrum.vanishingIdeal_anti_mono`, `ProjectiveSpectrum.homogeneousIdeal_le_vanishingIdeal_zeroLocus`, `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.relevant`, `Ideal.homogeneousCore_mono`, `Ideal.homogeneousCore.gc`

---

← Back to Index