Homogeneous ideals of a graded algebra

This file defines homogeneous ideals of GradedRing 𝒜 where 𝒜 : ι → Submodule R A and operations on them.

Main definitions

For any I : Ideal A:

• Ideal.IsHomogeneous 𝒜 I: The property that an ideal is closed under GradedRing.proj.
• HomogeneousIdeal 𝒜: The structure extending ideals which satisfy Ideal.IsHomogeneous.
• Ideal.homogeneousCore I 𝒜: The largest homogeneous ideal smaller than I.
• Ideal.homogeneousHull I 𝒜: The smallest homogeneous ideal larger than I.

Main statements

• HomogeneousIdeal.completeLattice: Ideal.IsHomogeneous is preserved by ⊥, ⊤, ⊔, ⊓, ⨆, ⨅, and so the subtype of homogeneous ideals inherits a complete lattice structure.
• Ideal.homogeneousCore.gi: Ideal.homogeneousCore forms a galois insertion with coercion.
• Ideal.homogeneousHull.gi: Ideal.homogeneousHull forms a galois insertion with coercion.

Implementation notes

We introduce Ideal.homogeneousCore' earlier than might be expected so that we can get access to Ideal.IsHomogeneous.iff_exists as quickly as possible.

Tags

graded algebra, homogeneous

@[reducible, inline]

abbrev Ideal.IsHomogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : Prop

An I : Ideal A is homogeneous if for every r ∈ I, all homogeneous components of r are in I.

theorem Ideal.IsHomogeneous.mem_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : Ideal A} (hI : IsHomogeneous 𝒜 I) {x : A} : x ∈ I ↔ ∀ (i : ι), ↑(((DirectSum.decompose 𝒜) x) i) ∈ I

@[reducible, inline]

abbrev HomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] : Type u_3

For any Semiring A, we collect the homogeneous ideals of A into a type.

@[reducible, inline]

abbrev HomogeneousIdeal.toIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : Ideal A

Converting a homogeneous ideal to an ideal.

theorem HomogeneousIdeal.isHomogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : Ideal.IsHomogeneous 𝒜 I.toIdeal

theorem HomogeneousIdeal.toIdeal_injective {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] : Function.Injective toIdeal

instance HomogeneousIdeal.setLike {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] : SetLike (HomogeneousIdeal 𝒜) A

theorem HomogeneousIdeal.ext {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I J : HomogeneousIdeal 𝒜} (h : I.toIdeal = J.toIdeal) : I = J

theorem HomogeneousIdeal.ext_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I J : HomogeneousIdeal 𝒜} : I = J ↔ I.toIdeal = J.toIdeal

theorem HomogeneousIdeal.ext' {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I J : HomogeneousIdeal 𝒜} (h : ∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J) : I = J

@[simp]

theorem HomogeneousIdeal.mem_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : HomogeneousIdeal 𝒜} {x : A} : x ∈ I.toIdeal ↔ x ∈ I

def Ideal.homogeneousCore' {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] (𝒜 : ι → σ) (I : Ideal A) : Ideal A

For any I : Ideal A, not necessarily homogeneous, I.homogeneousCore' 𝒜 is the largest homogeneous ideal of A contained in I, as an ideal.

theorem Ideal.homogeneousCore'_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] (𝒜 : ι → σ) : Monotone (homogeneousCore' 𝒜)

theorem Ideal.homogeneousCore'_le {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] (𝒜 : ι → σ) (I : Ideal A) : homogeneousCore' 𝒜 I ≤ I

theorem Ideal.isHomogeneous_iff_forall_subset {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : IsHomogeneous 𝒜 I ↔ ∀ (i : ι), ↑I ⊆ ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑I

theorem Ideal.isHomogeneous_iff_subset_iInter {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : IsHomogeneous 𝒜 I ↔ ↑I ⊆ ⋂ (i : ι), ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑I

theorem Ideal.mul_homogeneous_element_mem_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : Ideal A} (r x : A) (hx₁ : SetLike.IsHomogeneousElem 𝒜 x) (hx₂ : x ∈ I) (j : ι) : (GradedRing.proj 𝒜 j) (r * x) ∈ I

theorem Ideal.homogeneous_span {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (s : Set A) (h : ∀ x ∈ s, SetLike.IsHomogeneousElem 𝒜 x) : IsHomogeneous 𝒜 (span s)

def Ideal.homogeneousCore {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : HomogeneousIdeal 𝒜

For any I : Ideal A, not necessarily homogeneous, I.homogeneousCore' 𝒜 is the largest homogeneous ideal of A contained in I.

theorem Ideal.homogeneousCore_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] : Monotone (homogeneousCore 𝒜)

theorem Ideal.toIdeal_homogeneousCore_le {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : (homogeneousCore 𝒜 I).toIdeal ≤ I

theorem Ideal.mem_homogeneousCore_of_homogeneous_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : Ideal A} {x : A} (h : SetLike.IsHomogeneousElem 𝒜 x) (hmem : x ∈ I) : x ∈ homogeneousCore 𝒜 I

theorem Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : Ideal A} (h : IsHomogeneous 𝒜 I) : (homogeneousCore 𝒜 I).toIdeal = I

@[simp]

theorem HomogeneousIdeal.toIdeal_homogeneousCore_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : Ideal.homogeneousCore 𝒜 I.toIdeal = I

theorem Ideal.IsHomogeneous.iff_eq {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : IsHomogeneous 𝒜 I ↔ (homogeneousCore 𝒜 I).toIdeal = I

theorem Ideal.IsHomogeneous.iff_exists {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : IsHomogeneous 𝒜 I ↔ ∃ (S : Set ↥(SetLike.homogeneousSubmonoid 𝒜)), I = span (Subtype.val '' S)

Operations

In this section, we show that Ideal.IsHomogeneous is preserved by various notations, then use these results to provide these notation typeclasses for HomogeneousIdeal.

theorem Ideal.IsHomogeneous.bot {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : IsHomogeneous 𝒜 ⊥

theorem Ideal.IsHomogeneous.top {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : IsHomogeneous 𝒜 ⊤

theorem Ideal.IsHomogeneous.inf {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I J : Ideal A} (HI : IsHomogeneous 𝒜 I) (HJ : IsHomogeneous 𝒜 J) : IsHomogeneous 𝒜 (I ⊓ J)

theorem Ideal.IsHomogeneous.sup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I J : Ideal A} (HI : IsHomogeneous 𝒜 I) (HJ : IsHomogeneous 𝒜 J) : IsHomogeneous 𝒜 (I ⊔ J)

theorem Ideal.IsHomogeneous.iSup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {κ : Sort u_4} {f : κ → Ideal A} (h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)) : IsHomogeneous 𝒜 (⨆ (i : κ), f i)

theorem Ideal.IsHomogeneous.iInf {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {κ : Sort u_4} {f : κ → Ideal A} (h : ∀ (i : κ), IsHomogeneous 𝒜 (f i)) : IsHomogeneous 𝒜 (⨅ (i : κ), f i)

theorem Ideal.IsHomogeneous.iSup₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {κ : Sort u_4} {κ' : κ → Sort u_5} {f : (i : κ) → κ' i → Ideal A} (h : ∀ (i : κ) (j : κ' i), IsHomogeneous 𝒜 (f i j)) : IsHomogeneous 𝒜 (⨆ (i : κ), ⨆ (j : κ' i), f i j)

theorem Ideal.IsHomogeneous.iInf₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {κ : Sort u_4} {κ' : κ → Sort u_5} {f : (i : κ) → κ' i → Ideal A} (h : ∀ (i : κ) (j : κ' i), IsHomogeneous 𝒜 (f i j)) : IsHomogeneous 𝒜 (⨅ (i : κ), ⨅ (j : κ' i), f i j)

theorem Ideal.IsHomogeneous.sSup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {ℐ : Set (Ideal A)} (h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I) : IsHomogeneous 𝒜 (SupSet.sSup ℐ)

theorem Ideal.IsHomogeneous.sInf {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {ℐ : Set (Ideal A)} (h : ∀ I ∈ ℐ, IsHomogeneous 𝒜 I) : IsHomogeneous 𝒜 (InfSet.sInf ℐ)

instance HomogeneousIdeal.instPartialOrder {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : PartialOrder (HomogeneousIdeal 𝒜)

instance HomogeneousIdeal.instTop {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : Top (HomogeneousIdeal 𝒜)

instance HomogeneousIdeal.instBot {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : Bot (HomogeneousIdeal 𝒜)

instance HomogeneousIdeal.instMax {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : Max (HomogeneousIdeal 𝒜)

instance HomogeneousIdeal.instMin {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : Min (HomogeneousIdeal 𝒜)

instance HomogeneousIdeal.instSupSet {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : SupSet (HomogeneousIdeal 𝒜)

instance HomogeneousIdeal.instInfSet {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : InfSet (HomogeneousIdeal 𝒜)

@[simp]

theorem HomogeneousIdeal.coe_top {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : ↑⊤ = Set.univ

@[simp]

theorem HomogeneousIdeal.coe_bot {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : ↑⊥ = 0

@[simp]

theorem HomogeneousIdeal.coe_sup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I J : HomogeneousIdeal 𝒜) : ↑(I ⊔ J) = ↑I + ↑J

@[simp]

theorem HomogeneousIdeal.coe_inf {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I J : HomogeneousIdeal 𝒜) : ↑(I ⊓ J) = ↑I ∩ ↑J

@[simp]

theorem HomogeneousIdeal.toIdeal_top {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : ⊤.toIdeal = ⊤

@[simp]

theorem HomogeneousIdeal.toIdeal_bot {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : ⊥.toIdeal = ⊥

@[simp]

theorem HomogeneousIdeal.toIdeal_sup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I J : HomogeneousIdeal 𝒜) : (I ⊔ J).toIdeal = I.toIdeal ⊔ J.toIdeal

@[simp]

theorem HomogeneousIdeal.toIdeal_inf {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I J : HomogeneousIdeal 𝒜) : (I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal

@[simp]

theorem HomogeneousIdeal.toIdeal_sSup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (ℐ : Set (HomogeneousIdeal 𝒜)) : (sSup ℐ).toIdeal = ⨆ s ∈ ℐ, s.toIdeal

@[simp]

theorem HomogeneousIdeal.toIdeal_sInf {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (ℐ : Set (HomogeneousIdeal 𝒜)) : (sInf ℐ).toIdeal = ⨅ s ∈ ℐ, s.toIdeal

@[simp]

theorem HomogeneousIdeal.toIdeal_iSup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {κ : Sort u_4} (s : κ → HomogeneousIdeal 𝒜) : (⨆ (i : κ), s i).toIdeal = ⨆ (i : κ), (s i).toIdeal

@[simp]

theorem HomogeneousIdeal.toIdeal_iInf {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {κ : Sort u_4} (s : κ → HomogeneousIdeal 𝒜) : (⨅ (i : κ), s i).toIdeal = ⨅ (i : κ), (s i).toIdeal

theorem HomogeneousIdeal.toIdeal_iSup₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {κ : Sort u_4} {κ' : κ → Sort u_5} (s : (i : κ) → κ' i → HomogeneousIdeal 𝒜) : (⨆ (i : κ), ⨆ (j : κ' i), s i j).toIdeal = ⨆ (i : κ), ⨆ (j : κ' i), (s i j).toIdeal

theorem HomogeneousIdeal.toIdeal_iInf₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {κ : Sort u_4} {κ' : κ → Sort u_5} (s : (i : κ) → κ' i → HomogeneousIdeal 𝒜) : (⨅ (i : κ), ⨅ (j : κ' i), s i j).toIdeal = ⨅ (i : κ), ⨅ (j : κ' i), (s i j).toIdeal

@[simp]

theorem HomogeneousIdeal.eq_top_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : I = ⊤ ↔ I.toIdeal = ⊤

@[simp]

theorem HomogeneousIdeal.eq_bot_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : I = ⊥ ↔ I.toIdeal = ⊥

instance HomogeneousIdeal.completeLattice {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : CompleteLattice (HomogeneousIdeal 𝒜)

instance HomogeneousIdeal.instAdd {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : Add (HomogeneousIdeal 𝒜)

@[simp]

theorem HomogeneousIdeal.toIdeal_add {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I J : HomogeneousIdeal 𝒜) : (I + J).toIdeal = I.toIdeal + J.toIdeal

instance HomogeneousIdeal.instInhabited {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : Inhabited (HomogeneousIdeal 𝒜)

theorem Ideal.IsHomogeneous.mul {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommSemiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I J : Ideal A} (HI : IsHomogeneous 𝒜 I) (HJ : IsHomogeneous 𝒜 J) : IsHomogeneous 𝒜 (I * J)

instance instMulHomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommSemiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : Mul (HomogeneousIdeal 𝒜)

@[simp]

theorem HomogeneousIdeal.toIdeal_mul {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommSemiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I J : HomogeneousIdeal 𝒜) : (I * J).toIdeal = I.toIdeal * J.toIdeal

Homogeneous core

Note that many results about the homogeneous core came earlier in this file, as they are helpful for building the lattice structure.

theorem Ideal.homogeneousCore.gc {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : GaloisConnection HomogeneousIdeal.toIdeal (homogeneousCore 𝒜)

def Ideal.homogeneousCore.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : GaloisCoinsertion HomogeneousIdeal.toIdeal (homogeneousCore 𝒜)

toIdeal : HomogeneousIdeal 𝒜 → Ideal A and Ideal.homogeneousCore 𝒜 forms a galois coinsertion.

theorem Ideal.homogeneousCore_eq_sSup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : homogeneousCore 𝒜 I = sSup {J : HomogeneousIdeal 𝒜 | J.toIdeal ≤ I}

theorem Ideal.homogeneousCore'_eq_sSup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : homogeneousCore' 𝒜 I = sSup {J : Ideal A | IsHomogeneous 𝒜 J ∧ J ≤ I}

Homogeneous hulls

def Ideal.homogeneousHull {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : HomogeneousIdeal 𝒜

For any I : Ideal A, not necessarily homogeneous, I.homogeneousHull 𝒜 is the smallest homogeneous ideal containing I.

theorem Ideal.le_toIdeal_homogeneousHull {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : I ≤ (homogeneousHull 𝒜 I).toIdeal

theorem Ideal.homogeneousHull_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : Monotone (homogeneousHull 𝒜)

theorem Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I : Ideal A} (h : IsHomogeneous 𝒜 I) : (homogeneousHull 𝒜 I).toIdeal = I

@[simp]

theorem HomogeneousIdeal.homogeneousHull_toIdeal_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : Ideal.homogeneousHull 𝒜 I.toIdeal = I

theorem Ideal.toIdeal_homogeneousHull_eq_iSup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : (homogeneousHull 𝒜 I).toIdeal = ⨆ (i : ι), span (⇑(GradedRing.proj 𝒜 i) '' ↑I)

theorem Ideal.homogeneousHull_eq_iSup {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : homogeneousHull 𝒜 I = ⨆ (i : ι), { toSubmodule := span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }

theorem Ideal.homogeneousHull.gc {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : GaloisConnection (homogeneousHull 𝒜) HomogeneousIdeal.toIdeal

def Ideal.homogeneousHull.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : GaloisInsertion (homogeneousHull 𝒜) HomogeneousIdeal.toIdeal

Ideal.homogeneousHull 𝒜 and toIdeal : HomogeneousIdeal 𝒜 → Ideal A form a galois insertion.

theorem Ideal.homogeneousHull_eq_sInf {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : homogeneousHull 𝒜 I = sInf {J : HomogeneousIdeal 𝒜 | I ≤ J.toIdeal}

def HomogeneousIdeal.irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : HomogeneousIdeal 𝒜

For a graded ring ⨁ᵢ 𝒜ᵢ graded by a CanonicallyOrderedAddCommMonoid ι, the irrelevant ideal refers to ⨁_{i>0} 𝒜ᵢ, or equivalently {a | a₀ = 0}. This definition is used in Proj construction where ι is always ℕ so the irrelevant ideal is simply elements with 0 as 0-th coordinate.

Future work

Here in the definition, ι is assumed to be CanonicallyOrderedAddCommMonoid. However, the notion of irrelevant ideal makes sense in a more general setting by defining it as the ideal of elements with 0 as i-th coordinate for all i ≤ 0, i.e. {a | ∀ (i : ι), i ≤ 0 → aᵢ = 0}.

@[simp]

theorem HomogeneousIdeal.mem_irrelevant_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (a : A) : a ∈ irrelevant 𝒜 ↔ (GradedRing.proj 𝒜 0) a = 0

@[simp]

theorem HomogeneousIdeal.toIdeal_irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [Semiring A] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : (irrelevant 𝒜).toIdeal = RingHom.ker (GradedRing.projZeroRingHom 𝒜)