Minimal primes #

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

We provide various results concerning the minimal primes above an ideal

Main results #

ideal.minimal_primes: I.minimal_primes is the set of ideals that are minimal primes over I.
minimal_primes: minimal_primes R is the set of minimal primes of R.
ideal.exists_minimal_primes_le: Every prime ideal over I contains a minimal prime over I.
ideal.radical_minimal_primes: The minimal primes over I.radical are precisely the minimal primes over I.
ideal.Inf_minimal_primes: The intersection of minimal primes over I is I.radical.
ideal.exists_minimal_primes_comap_eq If p is a minimal prime over f ⁻¹ I, then it is the preimage of some minimal prime over I.
ideal.minimal_primes_eq_comap: The minimal primes over I are precisely the preimages of minimal primes of R ⧸ I.

source

def ideal.minimal_primes {R : Type u_1} [comm_ring R] (I : ideal R) :

set (ideal R)

I.minimal_primes is the set of ideals that are minimal primes over I.

Equations

I.minimal_primes = minimals has_le.le {p : ideal R | p.is_prime ∧ I ≤ p}

source

def minimal_primes (R : Type u_1) [comm_ring R] :

set (ideal R)

minimal_primes R is the set of minimal primes of R. This is defined as ideal.minimal_primes ⊥.

Equations

minimal_primes R = ⊥.minimal_primes

source

theorem ideal.exists_minimal_primes_le {R : Type u_1} [comm_ring R] {I J : ideal R} [J.is_prime] (e : I ≤ J) :

∃ (p : ideal R) (H : p ∈ I.minimal_primes), p ≤ J

source

@[simp]

theorem ideal.radical_minimal_primes {R : Type u_1} [comm_ring R] {I : ideal R} :

I.radical.minimal_primes = I.minimal_primes

source

@[simp]

theorem ideal.Inf_minimal_primes {R : Type u_1} [comm_ring R] {I : ideal R} :

has_Inf.Inf I.minimal_primes = I.radical

source

theorem ideal.exists_comap_eq_of_mem_minimal_primes_of_injective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.injective ⇑f) (p : ideal R) (H : p ∈ minimal_primes R) :

∃ (p' : ideal S), p'.is_prime ∧ ideal.comap f p' = p

source

theorem ideal.exists_comap_eq_of_mem_minimal_primes {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal S} (f : R →+* S) (p : ideal R) (H : p ∈ (ideal.comap f I).minimal_primes) :

∃ (p' : ideal S), p'.is_prime ∧ I ≤ p' ∧ ideal.comap f p' = p

source

theorem ideal.exists_minimal_primes_comap_eq {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {I : ideal S} (f : R →+* S) (p : ideal R) (H : p ∈ (ideal.comap f I).minimal_primes) :

∃ (p' : ideal S) (H : p' ∈ I.minimal_primes), ideal.comap f p' = p

source

theorem ideal.mimimal_primes_comap_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective ⇑f) {I J : ideal S} (h : J ∈ I.minimal_primes) :

ideal.comap f J ∈ (ideal.comap f I).minimal_primes

source

theorem ideal.comap_minimal_primes_eq_of_surjective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] {f : R →+* S} (hf : function.surjective ⇑f) (I : ideal S) :

(ideal.comap f I).minimal_primes = ideal.comap f '' I.minimal_primes

source

theorem ideal.minimal_primes_eq_comap {R : Type u_1} [comm_ring R] {I : ideal R} :

I.minimal_primes = ideal.comap (ideal.quotient.mk I) '' minimal_primes (R ⧸ I)

source

theorem ideal.minimal_primes_eq_subsingleton {R : Type u_1} [comm_ring R] {I : ideal R} (hI : I.is_primary) :

I.minimal_primes = {I.radical}

source

theorem ideal.minimal_primes_eq_subsingleton_self {R : Type u_1} [comm_ring R] {I : ideal R} [I.is_prime] :

I.minimal_primes = {I}