This file contains a proof that the radical of any homogeneous ideal is a homogeneous ideal

Main statements

• Ideal.IsHomogeneous.isPrime_iff: for any I : Ideal A, if I is homogeneous, then I is prime if and only if I is homogeneously prime, i.e. I ≠ ⊤ and if x, y are homogeneous elements such that x * y ∈ I, then at least one of x,y is in I.
• Ideal.IsPrime.homogeneousCore: for any I : Ideal A, if I is prime, then I.homogeneous_core 𝒜 (i.e. the largest homogeneous ideal contained in I) is also prime.
• Ideal.IsHomogeneous.radical: for any I : Ideal A, if I is homogeneous, then the radical of I is homogeneous as well.
• HomogeneousIdeal.radical: for any I : HomogeneousIdeal 𝒜, I.radical is the radical of I as a HomogeneousIdeal 𝒜.

Implementation details

Throughout this file, the indexing type ι of grading is assumed to be a LinearOrderedCancelAddCommMonoid. This might be stronger than necessary but cancelling property is strictly necessary; for a counterexample of how Ideal.IsHomogeneous.isPrime_iff fails for a non-cancellative set see Counterexamples/HomogeneousPrimeNotPrime.lean.

Tags

homogeneous, radical

theorem Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommRing A] [LinearOrderedCancelAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I : Ideal A} (hI : Ideal.IsHomogeneous 𝒜 I) (I_ne_top : I ≠ ⊤) (homogeneous_mem_or_mem : ∀ {x y : A}, SetLike.Homogeneous 𝒜 x → SetLike.Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I) : Ideal.IsPrime I

theorem Ideal.IsHomogeneous.isPrime_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommRing A] [LinearOrderedCancelAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I : Ideal A} (h : Ideal.IsHomogeneous 𝒜 I) : Ideal.IsPrime I ↔ I ≠ ⊤ ∧ ∀ {x y : A}, SetLike.Homogeneous 𝒜 x → SetLike.Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I

theorem Ideal.IsPrime.homogeneousCore {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommRing A] [LinearOrderedCancelAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I : Ideal A} (h : Ideal.IsPrime I) : Ideal.IsPrime (HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜 I))

theorem Ideal.IsHomogeneous.radical_eq {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommRing A] [LinearOrderedCancelAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I : Ideal A} (hI : Ideal.IsHomogeneous 𝒜 I) : Ideal.radical I = sInf {J : Ideal A | Ideal.IsHomogeneous 𝒜 J ∧ I ≤ J ∧ Ideal.IsPrime J}

theorem Ideal.IsHomogeneous.radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommRing A] [LinearOrderedCancelAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] {I : Ideal A} (h : Ideal.IsHomogeneous 𝒜 I) : Ideal.IsHomogeneous 𝒜 (Ideal.radical I)

def HomogeneousIdeal.radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommRing A] [LinearOrderedCancelAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : HomogeneousIdeal 𝒜

The radical of a homogenous ideal, as another homogenous ideal.

Equations

• HomogeneousIdeal.radical I = { toSubmodule := Ideal.radical (HomogeneousIdeal.toIdeal I), is_homogeneous' := (_ : Ideal.IsHomogeneous 𝒜 (Ideal.radical (HomogeneousIdeal.toIdeal I))) }

@[simp]

theorem HomogeneousIdeal.coe_radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [CommRing A] [LinearOrderedCancelAddCommMonoid ι] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ι → σ} [GradedRing 𝒜] (I : HomogeneousIdeal 𝒜) : HomogeneousIdeal.toIdeal (HomogeneousIdeal.radical I) = Ideal.radical (HomogeneousIdeal.toIdeal I)