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) : I.IsPrime

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

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) : I.radical = sInf {J : Ideal A | Ideal.IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}

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 𝒜 I.radical

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 homogeneous ideal, as another homogeneous ideal.

Equations

• I.radical = { toSubmodule := I.toIdeal.radical, is_homogeneous' := ⋯ }

@[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 𝒜) : I.radical.toIdeal = I.toIdeal.radical