# Documentation

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 #

theorem Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } (hI : ) (I_ne_top : I ) (homogeneous_mem_or_mem : ∀ {x y : A}, x * y Ix I y I) :
theorem Ideal.IsHomogeneous.isPrime_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } (h : ) :
I ∀ {x y : A}, x * y Ix I y I
theorem Ideal.IsPrime.homogeneousCore {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } (h : ) :
theorem Ideal.IsHomogeneous.radical_eq {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } (hI : ) :
= sInf {J | I J }
theorem Ideal.IsHomogeneous.radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [] [SetLike σ A] [] {𝒜 : ισ} [] {I : } (h : ) :
def HomogeneousIdeal.radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) :

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

Instances For
@[simp]
theorem HomogeneousIdeal.coe_radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [] [SetLike σ A] [] {𝒜 : ισ} [] (I : ) :