# 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 #

def Ideal.IsHomogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] (I : ) :

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

Equations
• = ∀ (i : ι) ⦃r : A⦄, r I(( r) i) I
Instances For
theorem Ideal.IsHomogeneous.mem_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] {I : } (hI : ) {x : A} :
x I ∀ (i : ι), (( x) i) I
structure HomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] extends :
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.carrierb self.carriera + b self.carrier
• zero_mem' : 0 self.carrier
• smul_mem' : ∀ (c : A) {x : A}, x self.carrierc x self.carrier
• is_homogeneous' : Ideal.IsHomogeneous 𝒜 self.toSubmodule
Instances For
theorem HomogeneousIdeal.is_homogeneous' {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] (self : ) :
Ideal.IsHomogeneous 𝒜 self.toSubmodule
def HomogeneousIdeal.toIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] (I : ) :

Converting a homogeneous ideal to an ideal.

Equations
• I.toIdeal = I.toSubmodule
Instances For
theorem HomogeneousIdeal.isHomogeneous {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] (I : ) :
Ideal.IsHomogeneous 𝒜 I.toIdeal
theorem HomogeneousIdeal.toIdeal_injective {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] :
Function.Injective HomogeneousIdeal.toIdeal
instance HomogeneousIdeal.setLike {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] :
Equations
• HomogeneousIdeal.setLike = { coe := fun (I : ) => I.toIdeal, coe_injective' := }
theorem HomogeneousIdeal.ext {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] {I : } {J : } (h : I.toIdeal = J.toIdeal) :
I = J
theorem HomogeneousIdeal.ext' {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] {I : } {J : } (h : ∀ (i : ι), x𝒜 i, x I x J) :
I = J
@[simp]
theorem HomogeneousIdeal.mem_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] {I : } {x : A} :
x I.toIdeal x I
def Ideal.homogeneousCore' {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] (𝒜 : ισ) (I : ) :

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

Equations
Instances For
theorem Ideal.homogeneousCore'_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] (𝒜 : ισ) :
theorem Ideal.homogeneousCore'_le {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] (𝒜 : ισ) (I : ) :
theorem Ideal.isHomogeneous_iff_forall_subset {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] (I : ) :
∀ (i : ι), I () ⁻¹' I
theorem Ideal.isHomogeneous_iff_subset_iInter {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] (I : ) :
I ⋂ (i : ι), () ⁻¹' I
theorem Ideal.mul_homogeneous_element_mem_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] {I : } (r : A) (x : A) (hx₁ : ) (hx₂ : x I) (j : ι) :
() (r * x) I
theorem Ideal.homogeneous_span {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] (s : Set A) (h : xs, ) :
def Ideal.homogeneousCore {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] (I : ) :

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

Equations
• = { toSubmodule := , is_homogeneous' := }
Instances For
theorem Ideal.homogeneousCore_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] :
theorem Ideal.toIdeal_homogeneousCore_le {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] (I : ) :
().toIdeal I
theorem Ideal.mem_homogeneousCore_of_homogeneous_of_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] {I : } {x : A} (h : ) (hmem : x I) :
theorem Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] {I : } (h : ) :
().toIdeal = I
@[simp]
theorem HomogeneousIdeal.toIdeal_homogeneousCore_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] {𝒜 : ισ} [] [] [] (I : ) :
Ideal.homogeneousCore 𝒜 I.toIdeal = I
theorem Ideal.IsHomogeneous.iff_eq {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] (I : ) :
().toIdeal = I
theorem Ideal.IsHomogeneous.iff_exists {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [SetLike σ A] [] (𝒜 : ισ) [] [] [] (I : ) :
∃ (S : ), I = Ideal.span (Subtype.val '' S)

### Operations #

In this section, we show that Ideal.IsHomogeneous is preserved by various notations, then use these results to provide these notation typeclasses for HomogeneousIdeal.

theorem Ideal.IsHomogeneous.bot {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
theorem Ideal.IsHomogeneous.top {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
theorem Ideal.IsHomogeneous.inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } {J : } (HI : ) (HJ : ) :
theorem Ideal.IsHomogeneous.sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } {J : } (HI : ) (HJ : ) :
theorem Ideal.IsHomogeneous.iSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {κ : Sort u_5} {f : κ} (h : ∀ (i : κ), Ideal.IsHomogeneous 𝒜 (f i)) :
Ideal.IsHomogeneous 𝒜 (⨆ (i : κ), f i)
theorem Ideal.IsHomogeneous.iInf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {κ : Sort u_5} {f : κ} (h : ∀ (i : κ), Ideal.IsHomogeneous 𝒜 (f i)) :
Ideal.IsHomogeneous 𝒜 (⨅ (i : κ), f i)
theorem Ideal.IsHomogeneous.iSup₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {κ : Sort u_5} {κ' : κSort u_6} {f : (i : κ) → κ' i} (h : ∀ (i : κ) (j : κ' i), Ideal.IsHomogeneous 𝒜 (f i j)) :
Ideal.IsHomogeneous 𝒜 (⨆ (i : κ), ⨆ (j : κ' i), f i j)
theorem Ideal.IsHomogeneous.iInf₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {κ : Sort u_5} {κ' : κSort u_6} {f : (i : κ) → κ' i} (h : ∀ (i : κ) (j : κ' i), Ideal.IsHomogeneous 𝒜 (f i j)) :
Ideal.IsHomogeneous 𝒜 (⨅ (i : κ), ⨅ (j : κ' i), f i j)
theorem Ideal.IsHomogeneous.sSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {ℐ : Set ()} (h : I, ) :
theorem Ideal.IsHomogeneous.sInf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {ℐ : Set ()} (h : I, ) :
instance HomogeneousIdeal.instPartialOrder {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instPartialOrder = SetLike.instPartialOrder
instance HomogeneousIdeal.instTop {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instTop = { top := { toSubmodule := , is_homogeneous' := } }
instance HomogeneousIdeal.instBot {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instBot = { bot := { toSubmodule := , is_homogeneous' := } }
instance HomogeneousIdeal.instSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instSup = { sup := fun (I J : ) => { toSubmodule := I.toIdeal J.toIdeal, is_homogeneous' := } }
instance HomogeneousIdeal.instInf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instInf = { inf := fun (I J : ) => { toSubmodule := I.toIdeal J.toIdeal, is_homogeneous' := } }
instance HomogeneousIdeal.instSupSet {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instSupSet = { sSup := fun (S : ) => { toSubmodule := sS, s.toIdeal, is_homogeneous' := } }
instance HomogeneousIdeal.instInfSet {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instInfSet = { sInf := fun (S : ) => { toSubmodule := sS, s.toIdeal, is_homogeneous' := } }
@[simp]
theorem HomogeneousIdeal.coe_top {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
= Set.univ
@[simp]
theorem HomogeneousIdeal.coe_bot {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
= 0
@[simp]
theorem HomogeneousIdeal.coe_sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) (J : ) :
(I J) = I + J
@[simp]
theorem HomogeneousIdeal.coe_inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) (J : ) :
(I J) = I J
@[simp]
theorem HomogeneousIdeal.toIdeal_top {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
.toIdeal =
@[simp]
theorem HomogeneousIdeal.toIdeal_bot {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
.toIdeal =
@[simp]
theorem HomogeneousIdeal.toIdeal_sup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) (J : ) :
(I J).toIdeal = I.toIdeal J.toIdeal
@[simp]
theorem HomogeneousIdeal.toIdeal_inf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) (J : ) :
(I J).toIdeal = I.toIdeal J.toIdeal
@[simp]
theorem HomogeneousIdeal.toIdeal_sSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (ℐ : ) :
(sSup ).toIdeal = s, s.toIdeal
@[simp]
theorem HomogeneousIdeal.toIdeal_sInf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (ℐ : ) :
(sInf ).toIdeal = s, s.toIdeal
@[simp]
theorem HomogeneousIdeal.toIdeal_iSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {κ : Sort u_5} (s : κ) :
(⨆ (i : κ), s i).toIdeal = ⨆ (i : κ), (s i).toIdeal
@[simp]
theorem HomogeneousIdeal.toIdeal_iInf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {κ : Sort u_5} (s : κ) :
(⨅ (i : κ), s i).toIdeal = ⨅ (i : κ), (s i).toIdeal
theorem HomogeneousIdeal.toIdeal_iSup₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {κ : Sort u_5} {κ' : κSort u_6} (s : (i : κ) → κ' i) :
(⨆ (i : κ), ⨆ (j : κ' i), s i j).toIdeal = ⨆ (i : κ), ⨆ (j : κ' i), (s i j).toIdeal
theorem HomogeneousIdeal.toIdeal_iInf₂ {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {κ : Sort u_5} {κ' : κSort u_6} (s : (i : κ) → κ' i) :
(⨅ (i : κ), ⨅ (j : κ' i), s i j).toIdeal = ⨅ (i : κ), ⨅ (j : κ' i), (s i j).toIdeal
@[simp]
theorem HomogeneousIdeal.eq_top_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) :
I = I.toIdeal =
@[simp]
theorem HomogeneousIdeal.eq_bot_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) :
I = I.toIdeal =
instance HomogeneousIdeal.completeLattice {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
instance HomogeneousIdeal.instAdd {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instAdd = { add := fun (x x_1 : ) => x x_1 }
@[simp]
theorem HomogeneousIdeal.toIdeal_add {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) (J : ) :
(I + J).toIdeal = I.toIdeal + J.toIdeal
instance HomogeneousIdeal.instInhabited {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• HomogeneousIdeal.instInhabited = { default := }
theorem Ideal.IsHomogeneous.mul {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } {J : } (HI : ) (HJ : ) :
instance instMulHomogeneousIdeal {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] :
Equations
• instMulHomogeneousIdeal = { mul := fun (I J : ) => { toSubmodule := I.toIdeal * J.toIdeal, is_homogeneous' := } }
@[simp]
theorem HomogeneousIdeal.toIdeal_mul {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) (J : ) :
(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.

theorem Ideal.homogeneousCore.gc {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
GaloisConnection HomogeneousIdeal.toIdeal
def Ideal.homogeneousCore.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
GaloisCoinsertion HomogeneousIdeal.toIdeal

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
theorem Ideal.homogeneousCore_eq_sSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (I : ) :
= sSup {J : | J.toIdeal I}
theorem Ideal.homogeneousCore'_eq_sSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (I : ) :
= sSup {J : | J I}

### Homogeneous hulls #

def Ideal.homogeneousHull {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (I : ) :

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

Equations
• = { toSubmodule := Ideal.span {r : A | ∃ (i : ι) (x : I), (( x) i) = r}, is_homogeneous' := }
Instances For
theorem Ideal.le_toIdeal_homogeneousHull {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (I : ) :
I ().toIdeal
theorem Ideal.homogeneousHull_mono {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
theorem Ideal.IsHomogeneous.toIdeal_homogeneousHull_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } (h : ) :
().toIdeal = I
@[simp]
theorem HomogeneousIdeal.homogeneousHull_toIdeal_eq_self {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) :
Ideal.homogeneousHull 𝒜 I.toIdeal = I
theorem Ideal.toIdeal_homogeneousHull_eq_iSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (I : ) :
().toIdeal = ⨆ (i : ι), Ideal.span (() '' I)
theorem Ideal.homogeneousHull_eq_iSup {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (I : ) :
= ⨆ (i : ι), { toSubmodule := Ideal.span (() '' I), is_homogeneous' := }
theorem Ideal.homogeneousHull.gc {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
GaloisConnection HomogeneousIdeal.toIdeal
def Ideal.homogeneousHull.gi {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
GaloisInsertion 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
theorem Ideal.homogeneousHull_eq_sInf {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [] [SetLike σ A] [] (𝒜 : ισ) [] (I : ) :
= sInf {J : | I J.toIdeal}
def HomogeneousIdeal.irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] :

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
• = { toSubmodule := , is_homogeneous' := }
Instances For
@[simp]
theorem HomogeneousIdeal.mem_irrelevant_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] (a : A) :
() a = 0
@[simp]
theorem HomogeneousIdeal.toIdeal_irrelevant {ι : Type u_1} {σ : Type u_2} {A : Type u_4} [] [] [SetLike σ A] [] (𝒜 : ισ) [] :
.toIdeal =