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

def Ideal.IsHomogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [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.

structure HomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] extends Submodule : Type u_4

• carrier : Set A
• add_mem' : ∀ {a b : A}, a ∈ s.carrier → b ∈ s.carrier → a + b ∈ s.carrier
• zero_mem' : 0 ∈ s.carrier
• smul_mem' : ∀ (c : A) {x : A}, x ∈ s.carrier → c • x ∈ s.carrier
• is_homogeneous' : Ideal.IsHomogeneous 𝒜 s.toSubmodule

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

def HomogeneousIdeal.toIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [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_4} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : Ideal.IsHomogeneous 𝒜 (HomogeneousIdeal.toIdeal I)

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

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

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

@[simp]

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

def Ideal.homogeneousCore' {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [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_4} [Semiring A] [SetLike σ A] (𝒜 : ι → σ) : Monotone (Ideal.homogeneousCore' 𝒜)

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

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

theorem Ideal.isHomogeneous_iff_subset_iInter {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : Ideal.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_4} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] {I : Ideal A} (r : A) (x : A) (hx₁ : SetLike.Homogeneous 𝒜 x) (hx₂ : x ∈ I) (j : ι) : ↑(GradedRing.proj 𝒜 j) (r * x) ∈ I

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

def Ideal.homogeneousCore {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [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_4} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] : Monotone (Ideal.homogeneousCore 𝒜)

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

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

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

@[simp]

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

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

theorem Ideal.IsHomogeneous.iff_exists {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [Semiring A] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [DecidableEq ι] [AddMonoid ι] [GradedRing 𝒜] (I : Ideal A) : Ideal.IsHomogeneous 𝒜 I ↔ ∃ S, I = Ideal.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_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : Ideal.IsHomogeneous 𝒜 ⊥

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance HomogeneousIdeal.instInfSetHomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [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_4} [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_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] : ↑⊥ = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

instance HomogeneousIdeal.instAddHomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [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_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) (J : HomogeneousIdeal 𝒜) : HomogeneousIdeal.toIdeal (I + J) = HomogeneousIdeal.toIdeal I + HomogeneousIdeal.toIdeal J

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

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

instance instMulHomogeneousIdealToSemiring {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [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_4} [CommSemiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) (J : HomogeneousIdeal 𝒜) : HomogeneousIdeal.toIdeal (I * J) = HomogeneousIdeal.toIdeal I * HomogeneousIdeal.toIdeal J

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_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : GaloisConnection HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜)

def Ideal.homogeneousCore.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : GaloisCoinsertion HomogeneousIdeal.toIdeal (Ideal.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_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : Ideal.homogeneousCore 𝒜 I = sSup {J | HomogeneousIdeal.toIdeal J ≤ I}

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

Homogeneous hulls

def Ideal.homogeneousHull {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [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_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : I ≤ HomogeneousIdeal.toIdeal (Ideal.homogeneousHull 𝒜 I)

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

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

@[simp]

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

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

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

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

def Ideal.homogeneousHull.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] : GaloisInsertion (Ideal.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_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (I : Ideal A) : Ideal.homogeneousHull 𝒜 I = sInf {J | I ≤ HomogeneousIdeal.toIdeal J}

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

For a graded ring ⨁ᵢ 𝒜ᵢ graded by a CanonicallyOrderedAddMonoid ι, 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 CanonicallyOrderedAddMonoid. 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_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] (a : A) : a ∈ HomogeneousIdeal.irrelevant 𝒜 ↔ ↑(GradedRing.proj 𝒜 0) a = 0

@[simp]

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