ring_theory.graded_algebra.radical

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 #

homogeneous, radical

source

theorem ideal.is_homogeneous.is_prime_of_homogeneous_mem_or_mem {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [linear_ordered_cancel_add_comm_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] {I : ideal A} (hI : ideal.is_homogeneous 𝒜 I) (I_ne_top : I ≠ ⊤) (homogeneous_mem_or_mem : ∀ {x y : A}, set_like.is_homogeneous 𝒜 x → set_like.is_homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I) :

I.is_prime

source

theorem ideal.is_homogeneous.is_prime_iff {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [linear_ordered_cancel_add_comm_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] {I : ideal A} (h : ideal.is_homogeneous 𝒜 I) :

I.is_prime ↔ I ≠ ⊤ ∧ ∀ {x y : A}, set_like.is_homogeneous 𝒜 x → set_like.is_homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I

source

theorem ideal.is_prime.homogeneous_core {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [linear_ordered_cancel_add_comm_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] {I : ideal A} (h : I.is_prime) :

(ideal.homogeneous_core 𝒜 I).to_ideal.is_prime

source

theorem ideal.is_homogeneous.radical_eq {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [linear_ordered_cancel_add_comm_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] {I : ideal A} (hI : ideal.is_homogeneous 𝒜 I) :

I.radical = has_Inf.Inf {J : ideal A | ideal.is_homogeneous 𝒜 J ∧ I ≤ J ∧ J.is_prime}

source

theorem ideal.is_homogeneous.radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [linear_ordered_cancel_add_comm_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] {I : ideal A} (h : ideal.is_homogeneous 𝒜 I) :

ideal.is_homogeneous 𝒜 I.radical

source

def homogeneous_ideal.radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [linear_ordered_cancel_add_comm_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :

homogeneous_ideal 𝒜

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

Equations

I.radical = {to_submodule := I.to_ideal.radical, is_homogeneous' := _}

source

@[simp]

theorem homogeneous_ideal.coe_radical {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [comm_ring A] [linear_ordered_cancel_add_comm_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι → σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :

I.radical.to_ideal = I.to_ideal.radical