mathlib3 documentation

ring_theory.graded_algebra.homogeneous_ideal

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:

Main statements #

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 #

graded algebra, homogeneous

def ideal.is_homogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ 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
def homogeneous_ideal.to_ideal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ 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] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :
@[protected, instance]
def homogeneous_ideal.set_like {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ 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] [set_like σ A] [add_submonoid_class σ 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] [set_like σ A] [add_submonoid_class σ 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] [set_like σ 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] [set_like σ A] (𝒜 : ι σ) :
theorem ideal.homogeneous_core'_le {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] (𝒜 : ι σ) (I : ideal A) :
theorem ideal.is_homogeneous_iff_forall_subset {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
theorem ideal.is_homogeneous_iff_subset_Inter {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
theorem ideal.mul_homogeneous_element_mem_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] {I : ideal A} (r x : A) (hx₁ : set_like.is_homogeneous 𝒜 x) (hx₂ : x I) (j : ι) :
(graded_ring.proj 𝒜 j) (r * x) I
theorem ideal.is_homogeneous_span {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (s : set A) (h : (x : A), x s set_like.is_homogeneous 𝒜 x) :
def ideal.homogeneous_core {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ 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] [set_like σ A] [add_submonoid_class σ 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] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
theorem ideal.mem_homogeneous_core_of_is_homogeneous_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] {I : ideal A} {x : A} (h : set_like.is_homogeneous 𝒜 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] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] {I : ideal A} (h : ideal.is_homogeneous 𝒜 I) :
@[simp]
theorem homogeneous_ideal.to_ideal_homogeneous_core_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ 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] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :
theorem ideal.is_homogeneous.iff_exists {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [decidable_eq ι] [add_monoid ι] [graded_ring 𝒜] (I : ideal A) :

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 ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] :
theorem ideal.is_homogeneous.top {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] :
theorem ideal.is_homogeneous.inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {I J : ideal A} (HI : ideal.is_homogeneous 𝒜 I) (HJ : ideal.is_homogeneous 𝒜 J) :
theorem ideal.is_homogeneous.sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {I J : ideal A} (HI : ideal.is_homogeneous 𝒜 I) (HJ : ideal.is_homogeneous 𝒜 J) :
@[protected]
theorem ideal.is_homogeneous.supr {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {f : κ ideal A} (h : (i : κ), ideal.is_homogeneous 𝒜 (f i)) :
ideal.is_homogeneous 𝒜 ( (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {f : κ ideal A} (h : (i : κ), ideal.is_homogeneous 𝒜 (f i)) :
ideal.is_homogeneous 𝒜 ( (i : κ), f i)
theorem ideal.is_homogeneous.supr₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {κ' : κ Sort u_5} {f : Π (i : κ), κ' i ideal A} (h : (i : κ) (j : κ' i), ideal.is_homogeneous 𝒜 (f i j)) :
ideal.is_homogeneous 𝒜 ( (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {κ' : κ Sort u_5} {f : Π (i : κ), κ' i ideal A} (h : (i : κ) (j : κ' i), ideal.is_homogeneous 𝒜 (f i j)) :
ideal.is_homogeneous 𝒜 ( (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {ℐ : set (ideal A)} (h : (I : ideal A), I ideal.is_homogeneous 𝒜 I) :
theorem ideal.is_homogeneous.Inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {ℐ : set (ideal A)} (h : (I : ideal A), I ideal.is_homogeneous 𝒜 I) :
@[protected, instance]
def homogeneous_ideal.partial_order {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
@[simp]
theorem homogeneous_ideal.to_ideal_inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
@[simp]
theorem homogeneous_ideal.to_ideal_Sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (ℐ : set (homogeneous_ideal 𝒜)) :
(has_Sup.Sup ℐ).to_ideal = (s : homogeneous_ideal 𝒜) (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (ℐ : set (homogeneous_ideal 𝒜)) :
(has_Inf.Inf ℐ).to_ideal = (s : homogeneous_ideal 𝒜) (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} (s : κ homogeneous_ideal 𝒜) :
( (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} (s : κ homogeneous_ideal 𝒜) :
( (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {κ' : κ Sort u_5} (s : Π (i : κ), κ' i homogeneous_ideal 𝒜) :
( (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {κ : Sort u_3} {κ' : κ Sort u_5} (s : Π (i : κ), κ' i homogeneous_ideal 𝒜) :
( (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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :
@[simp]
theorem homogeneous_ideal.eq_bot_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :
@[protected, instance]
def homogeneous_ideal.complete_lattice {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[protected, instance]
def homogeneous_ideal.has_add {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_ideal 𝒜) :
@[protected, instance]
def homogeneous_ideal.inhabited {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
theorem ideal.is_homogeneous.mul {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [comm_semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {I J : ideal A} (HI : ideal.is_homogeneous 𝒜 I) (HJ : ideal.is_homogeneous 𝒜 J) :
@[protected, instance]
def homogeneous_ideal.has_mul {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [comm_semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] :
Equations
@[simp]
theorem homogeneous_ideal.to_ideal_mul {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [comm_semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (I J : homogeneous_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.

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 ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
theorem ideal.homogeneous_core'_eq_Sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :

Homogeneous hulls #

def ideal.homogeneous_hull {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
theorem ideal.homogeneous_hull_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] {I : ideal A} (h : ideal.is_homogeneous 𝒜 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 ι] [set_like σ A] [add_submonoid_class σ 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 ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
theorem ideal.homogeneous_hull_eq_supr {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :

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 ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] (I : ideal A) :
def homogeneous_ideal.irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [semiring A] [decidable_eq ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ 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 ι] [canonically_ordered_add_monoid ι] [set_like σ A] [add_submonoid_class σ A] (𝒜 : ι σ) [graded_ring 𝒜] (a : A) :