mathlib documentation

ring_theory.graded_algebra.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 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

theorem ideal.is_homogeneous.is_prime_of_homogeneous_mem_or_mem {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_ring A] [algebra R A] [linear_ordered_cancel_add_comm_monoid ι] {𝒜 : ι → submodule R A} [graded_algebra 𝒜] {I : ideal A} (hI : ideal.is_homogeneous 𝒜 I) (I_ne_top : I ) (homogeneous_mem_or_mem : ∀ {x y : A}, set_like.is_homogeneous 𝒜 xset_like.is_homogeneous 𝒜 yx * y Ix I y I) :
theorem ideal.is_homogeneous.is_prime_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_ring A] [algebra R A] [linear_ordered_cancel_add_comm_monoid ι] {𝒜 : ι → submodule R A} [graded_algebra 𝒜] {I : ideal A} (h : ideal.is_homogeneous 𝒜 I) :
I.is_prime I ∀ {x y : A}, set_like.is_homogeneous 𝒜 xset_like.is_homogeneous 𝒜 yx * y Ix I y I
theorem ideal.is_prime.homogeneous_core {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_ring A] [algebra R A] [linear_ordered_cancel_add_comm_monoid ι] {𝒜 : ι → submodule R A} [graded_algebra 𝒜] {I : ideal A} (h : I.is_prime) :
theorem ideal.is_homogeneous.radical_eq {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_ring A] [algebra R A] [linear_ordered_cancel_add_comm_monoid ι] {𝒜 : ι → submodule R A} [graded_algebra 𝒜] {I : ideal A} (hI : ideal.is_homogeneous 𝒜 I) :
theorem ideal.is_homogeneous.radical {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_ring A] [algebra R A] [linear_ordered_cancel_add_comm_monoid ι] {𝒜 : ι → submodule R A} [graded_algebra 𝒜] {I : ideal A} (h : ideal.is_homogeneous 𝒜 I) :
def homogeneous_ideal.radical {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_ring A] [algebra R A] [linear_ordered_cancel_add_comm_monoid ι] {𝒜 : ι → submodule R A} [graded_algebra 𝒜] (I : homogeneous_ideal 𝒜) :

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

Equations
@[simp]
theorem homogeneous_ideal.coe_radical {ι : Type u_1} {R : Type u_2} {A : Type u_3} [comm_semiring R] [comm_ring A] [algebra R A] [linear_ordered_cancel_add_comm_monoid ι] {𝒜 : ι → submodule R A} [graded_algebra 𝒜] (I : homogeneous_ideal 𝒜) :