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

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

x ∈ I ↔ ∀ (i : ι), ↑(((DirectSum.decompose 𝒜) x) i) ∈ I

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

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

Ideal.IsHomogeneous 𝒜 self.toSubmodule

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

I.toIdeal = 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 𝒜 I.toIdeal

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 𝒜) => ↑I.toIdeal, 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 : I.toIdeal = J.toIdeal) :

I = J

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 : ∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ 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 ∈ I.toIdeal ↔ 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) :

(Ideal.homogeneousCore 𝒜 I).toIdeal ≤ 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) :

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

PartialOrder (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instPartialOrder = SetLike.instPartialOrder

source

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

Top (HomogeneousIdeal 𝒜)

Equations

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

source

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

Bot (HomogeneousIdeal 𝒜)

Equations

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

source

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

Sup (HomogeneousIdeal 𝒜)

Equations

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

source

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

Inf (HomogeneousIdeal 𝒜)

Equations

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

source

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

SupSet (HomogeneousIdeal 𝒜)

Equations

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

source

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

InfSet (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instInfSet = { sInf := fun (S : Set (HomogeneousIdeal 𝒜)) => { toSubmodule := ⨅ s ∈ S, s.toIdeal, 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 𝒜] :

⊤.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 𝒜] :

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

(I ⊔ J).toIdeal = I.toIdeal ⊔ J.toIdeal

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

(I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal

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

(sSup ℐ).toIdeal = ⨆ s ∈ ℐ, s.toIdeal

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

(sInf ℐ).toIdeal = ⨅ s ∈ ℐ, s.toIdeal

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

(⨆ (i : κ), s i).toIdeal = ⨆ (i : κ), (s i).toIdeal

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

(⨅ (i : κ), s i).toIdeal = ⨅ (i : κ), (s i).toIdeal

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

(⨆ (i : κ), ⨆ (j : κ' i), s i j).toIdeal = ⨆ (i : κ), ⨆ (j : κ' i), (s i j).toIdeal

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

(⨅ (i : κ), ⨅ (j : κ' i), s i j).toIdeal = ⨅ (i : κ), ⨅ (j : κ' i), (s i j).toIdeal

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 = ⊤ ↔ I.toIdeal = ⊤

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 = ⊥ ↔ I.toIdeal = ⊥

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.instAdd {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [Semiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] :

Add (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instAdd = { 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 𝒜) :

(I + J).toIdeal = I.toIdeal + J.toIdeal

source

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

Inhabited (HomogeneousIdeal 𝒜)

Equations

HomogeneousIdeal.instInhabited = { 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 instMulHomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [CommSemiring A] [DecidableEq ι] [AddMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] :

Mul (HomogeneousIdeal 𝒜)

Equations

instMulHomogeneousIdeal = { mul := fun (I J : HomogeneousIdeal 𝒜) => { toSubmodule := I.toIdeal * J.toIdeal, 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 𝒜) :

(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.

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 𝒜 | J.toIdeal ≤ 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 ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal

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

(Ideal.homogeneousHull 𝒜 I).toIdeal = 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 𝒜 I.toIdeal = 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) :

(Ideal.homogeneousHull 𝒜 I).toIdeal = ⨆ (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 ≤ J.toIdeal}

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