Homogeneous ideals of a graded algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

For any I : ideal A:

• ideal.is_homogeneous 𝒜 I: The property that an ideal is closed under graded_ring.proj.
• homogeneous_ideal 𝒜: The structure extending ideals which satisfy ideal.is_homogeneous
• ideal.homogeneous_core I 𝒜: The largest homogeneous ideal smaller than I.
• ideal.homogeneous_hull I 𝒜: The smallest homogeneous ideal larger than I.

Main statements #

• homogeneous_ideal.complete_lattice: ideal.is_homogeneous is preserved by ⊥, ⊤, ⊔, ⊓, ⨆, ⨅, and so the subtype of homogeneous ideals inherits a complete lattice structure.
• ideal.homogeneous_core.gi: ideal.homogeneous_core forms a galois insertion with coercion.
• ideal.homogeneous_hull.gi: ideal.homogeneous_hull forms a galois insertion with coercion.

Implementation notes #

We introduce ideal.homogeneous_core' earlier than might be expected so that we can get access to ideal.is_homogeneous.iff_exists as quickly as possible.

Tags #

def ideal.is_homogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
Prop

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

Equations
structure homogeneous_ideal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] :
Type u_4
• to_submodule : A
• is_homogeneous' :

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

Instances for homogeneous_ideal
def homogeneous_ideal.to_ideal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :

Converting a homogeneous ideal to an ideal

Equations
Instances for homogeneous_ideal.to_ideal
theorem homogeneous_ideal.is_homogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :
theorem homogeneous_ideal.to_ideal_injective {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] :
@[protected, instance]
def homogeneous_ideal.set_like {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] :
Equations
@[ext]
theorem homogeneous_ideal.ext {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] {I J : homogeneous_ideal 𝒜} (h : I.to_ideal = J.to_ideal) :
I = J
@[simp]
theorem homogeneous_ideal.mem_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] {I : homogeneous_ideal 𝒜} {x : A} :
def ideal.homogeneous_core' {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] (𝒜 : ι σ) (I : ideal A) :

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

Equations
theorem ideal.homogeneous_core'_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] (𝒜 : ι σ) :
theorem ideal.homogeneous_core'_le {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] (𝒜 : ι σ) (I : ideal A) :
theorem ideal.is_homogeneous_iff_forall_subset {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
(i : ι), I i) ⁻¹' I
theorem ideal.is_homogeneous_iff_subset_Inter {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
I (i : ι), i) ⁻¹' I
theorem ideal.mul_homogeneous_element_mem_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] {I : ideal A} (r x : A) (hx₁ : x) (hx₂ : x I) (j : ι) :
j) (r * x) I
theorem ideal.is_homogeneous_span {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (s : set A) (h : (x : A), x s ) :
def ideal.homogeneous_core {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :

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

Equations
theorem ideal.homogeneous_core_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] :
theorem ideal.to_ideal_homogeneous_core_le {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
I
theorem ideal.mem_homogeneous_core_of_is_homogeneous_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] {I : ideal A} {x : A} (h : x) (hmem : x I) :
theorem ideal.is_homogeneous.to_ideal_homogeneous_core_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] {I : ideal A} (h : I) :
= I
@[simp]
theorem homogeneous_ideal.to_ideal_homogeneous_core_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :
theorem ideal.is_homogeneous.iff_eq {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
= I
theorem ideal.is_homogeneous.iff_exists {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [ A] [ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
(S : , I = ideal.span (coe '' S)

Operations #

In this section, we show that ideal.is_homogeneous is preserved by various notations, then use these results to provide these notation typeclasses for homogeneous_ideal.

theorem ideal.is_homogeneous.bot {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :
theorem ideal.is_homogeneous.top {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :
theorem ideal.is_homogeneous.inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I J : ideal A} (HI : I) (HJ : J) :
(I J)
theorem ideal.is_homogeneous.sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I J : ideal A} (HI : I) (HJ : J) :
(I J)
@[protected]
theorem ideal.is_homogeneous.supr {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {f : κ } (h : (i : κ), (f i)) :
( (i : κ), f i)
@[protected]
theorem ideal.is_homogeneous.infi {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {f : κ } (h : (i : κ), (f i)) :
( (i : κ), f i)
theorem ideal.is_homogeneous.supr₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {κ' : κ Sort u_5} {f : Π (i : κ), κ' i } (h : (i : κ) (j : κ' i), (f i j)) :
( (i : κ) (j : κ' i), f i j)
theorem ideal.is_homogeneous.infi₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {κ' : κ Sort u_5} {f : Π (i : κ), κ' i } (h : (i : κ) (j : κ' i), (f i j)) :
( (i : κ) (j : κ' i), f i j)
theorem ideal.is_homogeneous.Sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {ℐ : set (ideal A)} (h : (I : ideal A), I ) :
theorem ideal.is_homogeneous.Inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {ℐ : set (ideal A)} (h : (I : ideal A), I ) :
@[protected, instance]
def homogeneous_ideal.partial_order {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[protected, instance]
def homogeneous_ideal.has_top {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[protected, instance]
def homogeneous_ideal.has_bot {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[protected, instance]
def homogeneous_ideal.has_sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[protected, instance]
def homogeneous_ideal.has_inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[protected, instance]
def homogeneous_ideal.has_Sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[protected, instance]
def homogeneous_ideal.has_Inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[simp]
theorem homogeneous_ideal.coe_top {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
@[simp]
theorem homogeneous_ideal.coe_bot {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
@[simp]
theorem homogeneous_ideal.coe_sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
(I J) = I + J
@[simp]
theorem homogeneous_ideal.coe_inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
(I J) = I J
@[simp]
theorem homogeneous_ideal.to_ideal_top {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
@[simp]
theorem homogeneous_ideal.to_ideal_bot {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
@[simp]
theorem homogeneous_ideal.to_ideal_sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
(I J).to_ideal =
@[simp]
theorem homogeneous_ideal.to_ideal_inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
(I J).to_ideal =
@[simp]
theorem homogeneous_ideal.to_ideal_Sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (ℐ : set ) :
(has_Sup.Sup ℐ).to_ideal = (s : (H : s ℐ), s.to_ideal
@[simp]
theorem homogeneous_ideal.to_ideal_Inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (ℐ : set ) :
(has_Inf.Inf ℐ).to_ideal = (s : (H : s ℐ), s.to_ideal
@[simp]
theorem homogeneous_ideal.to_ideal_supr {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} (s : κ ) :
( (i : κ), s i).to_ideal = (i : κ), (s i).to_ideal
@[simp]
theorem homogeneous_ideal.to_ideal_infi {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} (s : κ ) :
( (i : κ), s i).to_ideal = (i : κ), (s i).to_ideal
@[simp]
theorem homogeneous_ideal.to_ideal_supr₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {κ' : κ Sort u_5} (s : Π (i : κ), κ' i ) :
( (i : κ) (j : κ' i), s i j).to_ideal = (i : κ) (j : κ' i), (s i j).to_ideal
@[simp]
theorem homogeneous_ideal.to_ideal_infi₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {κ' : κ Sort u_5} (s : Π (i : κ), κ' i ) :
( (i : κ) (j : κ' i), s i j).to_ideal = (i : κ) (j : κ' i), (s i j).to_ideal
@[simp]
theorem homogeneous_ideal.eq_top_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :
I =
@[simp]
theorem homogeneous_ideal.eq_bot_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :
I =
@[protected, instance]
def homogeneous_ideal.complete_lattice {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
• homogeneous_ideal.complete_lattice = homogeneous_ideal.complete_lattice._proof_1 homogeneous_ideal.complete_lattice._proof_2 homogeneous_ideal.complete_lattice._proof_3 homogeneous_ideal.complete_lattice._proof_4 homogeneous_ideal.complete_lattice._proof_5 homogeneous_ideal.complete_lattice._proof_6 homogeneous_ideal.complete_lattice._proof_7
@[protected, instance]
def homogeneous_ideal.has_add {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[simp]
theorem homogeneous_ideal.to_ideal_add {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
(I + J).to_ideal =
@[protected, instance]
def homogeneous_ideal.inhabited {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
theorem ideal.is_homogeneous.mul {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I J : ideal A} (HI : I) (HJ : J) :
(I * J)
@[protected, instance]
def homogeneous_ideal.has_mul {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[simp]
theorem homogeneous_ideal.to_ideal_mul {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
(I * J).to_ideal =

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.homogeneous_core.gc {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :
def ideal.homogeneous_core.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :

to_ideal : homogeneous_ideal 𝒜 → ideal A and ideal.homogeneous_core 𝒜 forms a galois coinsertion

Equations
theorem ideal.homogeneous_core_eq_Sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
= has_Sup.Sup {J : | J.to_ideal I}
theorem ideal.homogeneous_core'_eq_Sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
= has_Sup.Sup {J : | J I}

Homogeneous hulls #

def ideal.homogeneous_hull {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :

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

Equations
theorem ideal.le_to_ideal_homogeneous_hull {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
I
theorem ideal.homogeneous_hull_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :
theorem ideal.is_homogeneous.to_ideal_homogeneous_hull_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I : ideal A} (h : I) :
= I
@[simp]
theorem homogeneous_ideal.homogeneous_hull_to_ideal_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :
theorem ideal.to_ideal_homogeneous_hull_eq_supr {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
= (i : ι), ideal.span ( i) '' I)
theorem ideal.homogeneous_hull_eq_supr {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
theorem ideal.homogeneous_hull.gc {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :
def ideal.homogeneous_hull.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :

ideal.homogeneous_hull 𝒜 and to_ideal : homogeneous_ideal 𝒜 → ideal A form a galois insertion

Equations
theorem ideal.homogeneous_hull_eq_Inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
= has_Inf.Inf {J : | I J.to_ideal}
def homogeneous_ideal.irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :

For a graded ring ⨁ᵢ 𝒜ᵢ graded by a canonically_ordered_add_monoid ι, 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 canonically_ordered_add_monoid. 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
@[simp]
theorem homogeneous_ideal.mem_irrelevant_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] (a : A) :
0) a = 0
@[simp]
theorem homogeneous_ideal.to_ideal_irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [ A] [ A] (𝒜 : ι σ) [graded_ring 𝒜] :