Documentation

Mathlib.RingTheory.GradedAlgebra.Radical

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

Main statements #

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 𝒜 xSetLike.Homogeneous 𝒜 yx * y Ix 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 𝒜 xSetLike.Homogeneous 𝒜 yx * y Ix 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 𝒜) :

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

Equations
  • I.radical = { toSubmodule := I.toIdeal.radical, is_homogeneous' := }
Instances For
    @[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