mathlib3 documentation

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.

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} {σ : 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) :
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) :
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) :
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) :
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) :
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 𝒜) :

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] [linear_ordered_cancel_add_comm_monoid ι] [set_like σ A] [add_submonoid_class σ A] {𝒜 : ι σ} [graded_ring 𝒜] (I : homogeneous_ideal 𝒜) :