# mathlib3documentation

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

## Main statements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

• ideal.is_homogeneous.is_prime_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.is_prime.homogeneous_core: 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.is_homogeneous.radical: for any I : ideal A, if I is homogeneous, then the radical of I is homogeneous as well.
• homogeneous_ideal.radical: for any I : homogeneous_ideal 𝒜, I.radical is the the radical of I as a homogeneous_ideal 𝒜

## Implementation details #

Throughout this file, the indexing type ι of grading is assumed to be a linear_ordered_cancel_add_comm_monoid. This might be stronger than necessary but cancelling property is strictly necessary; for a counterexample of how ideal.is_homogeneous.is_prime_iff fails for a non-cancellative set see counterexample/homogeneous_prime_not_prime.lean.

## Tags #

theorem ideal.is_homogeneous.is_prime_of_homogeneous_mem_or_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I : ideal A} (hI : I) (I_ne_top : I ) (homogeneous_mem_or_mem : {x y : A}, x * y I x I y I) :
theorem ideal.is_homogeneous.is_prime_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I : ideal A} (h : I) :
I.is_prime I {x y : A}, x * y I x I y I
theorem ideal.is_prime.homogeneous_core {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I : ideal A} (h : I.is_prime) :
theorem ideal.is_homogeneous.radical_eq {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I : ideal A} (hI : I) :
theorem ideal.is_homogeneous.radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] {I : ideal A} (h : I) :
def homogeneous_ideal.radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :

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

Equations
@[simp]
theorem homogeneous_ideal.coe_radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [ A] [ A] {𝒜 : ι σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :