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

source

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.

Equations

Ideal.IsHomogeneous 𝒜 I = ∀ (i : ι) ⦃r : A⦄, r ∈ I → ↑(((DirectSum.decompose 𝒜) r) i) ∈ I

Instances For

source

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

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

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

Instances For

source

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.

Equations

HomogeneousIdeal.toIdeal I = I.toSubmodule

Instances For

source

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)

source

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

source

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

Equations

HomogeneousIdeal.setLike = { coe := fun (I : HomogeneousIdeal 𝒜) => ↑(HomogeneousIdeal.toIdeal I), coe_injective' := ⋯ }

source

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

source

@[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

source

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.

Equations

Ideal.homogeneousCore' 𝒜 I = Ideal.span (Subtype.val '' (Subtype.val ⁻¹' ↑I))

Instances For

source

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

Monotone (Ideal.homogeneousCore' 𝒜)

source

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

source

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

source

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

source

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

source

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 ∈ s, SetLike.Homogeneous 𝒜 x) :

Ideal.IsHomogeneous 𝒜 (Ideal.span s)

source

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.

Equations

Ideal.homogeneousCore 𝒜 I = { toSubmodule := Ideal.homogeneousCore' 𝒜 I, is_homogeneous' := ⋯ }

Instances For

source

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 𝒜)

source

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

source

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

source

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

source

@[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

source

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

source

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 : Set ↥(SetLike.homogeneousSubmonoid 𝒜)), 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.

source

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 𝒜 ⊥

source

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 𝒜 ⊤

source

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)

source

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)

source

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)

source

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)

source

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)

source

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)

source

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.IsHomogeneous 𝒜 I) :

Ideal.IsHomogeneous 𝒜 (sSup ℐ)

source

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.IsHomogeneous 𝒜 I) :

Ideal.IsHomogeneous 𝒜 (sInf ℐ)

source

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

PartialOrder (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instPartialOrderHomogeneousIdeal = SetLike.instPartialOrder

source

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

Top (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instTopHomogeneousIdeal = { top := { toSubmodule := ⊤, is_homogeneous' := ⋯ } }

source

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

Bot (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instBotHomogeneousIdeal = { bot := { toSubmodule := ⊥, is_homogeneous' := ⋯ } }

source

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

Sup (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instSupHomogeneousIdeal = { sup := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := HomogeneousIdeal.toIdeal I ⊔ HomogeneousIdeal.toIdeal J, is_homogeneous' := ⋯ } }

source

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

Inf (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instInfHomogeneousIdeal = { inf := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := HomogeneousIdeal.toIdeal I ⊓ HomogeneousIdeal.toIdeal J, is_homogeneous' := ⋯ } }

source

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

SupSet (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instSupSetHomogeneousIdeal = { sSup := fun (S : Set (HomogeneousIdeal 𝒜)) => { toSubmodule := ⨆ s ∈ S, HomogeneousIdeal.toIdeal s, is_homogeneous' := ⋯ } }

source

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

InfSet (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instInfSetHomogeneousIdeal = { sInf := fun (S : Set (HomogeneousIdeal 𝒜)) => { toSubmodule := ⨅ s ∈ S, HomogeneousIdeal.toIdeal s, is_homogeneous' := ⋯ } }

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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 ⊤ = ⊤

source

@[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 ⊥ = ⊥

source

@[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

source

@[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

source

@[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.toIdeal s

source

@[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.toIdeal s

source

@[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)

source

@[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)

source

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)

source

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)

source

@[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 = ⊤

source

@[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 = ⊥

source

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

CompleteLattice (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.completeLattice = Function.Injective.completeLattice HomogeneousIdeal.toIdeal ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

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

Add (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instAddHomogeneousIdeal = { add := fun (x x_1 : HomogeneousIdeal 𝒜) => x ⊔ x_1 }

source

@[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

source

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

Inhabited (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instInhabitedHomogeneousIdeal = { default := ⊥ }

source

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)

source

instance instMulHomogeneousIdealToSemiring {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [CommSemiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] :

Mul (HomogeneousIdeal 𝒜)

Equations

instMulHomogeneousIdealToSemiring = { mul := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := HomogeneousIdeal.toIdeal I * HomogeneousIdeal.toIdeal J, is_homogeneous' := ⋯ } }

source

@[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.

source

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 𝒜)

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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 𝒜 | HomogeneousIdeal.toIdeal J ≤ I}

source

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 A | Ideal.IsHomogeneous 𝒜 J ∧ J ≤ I}

Homogeneous hulls #

source

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.

Equations

Ideal.homogeneousHull 𝒜 I = { toSubmodule := Ideal.span {r : A | ∃ (i : ι) (x : ↥I), ↑(((DirectSum.decompose 𝒜) ↑x) i) = r}, is_homogeneous' := ⋯ }

Instances For

source

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)

source

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 𝒜)

source

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

source

@[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

source

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)

source

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' := ⋯ }

source

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

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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 : HomogeneousIdeal 𝒜 | I ≤ HomogeneousIdeal.toIdeal J}

source

def HomogeneousIdeal.irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [Semiring A] [DecidableEq ι] [CanonicallyOrderedAddCommMonoid ι] [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}.

Equations