# mathlib3documentation

ring_theory.ideal.minimal_prime

# 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.
def ideal.minimal_primes {R : Type u_1} [comm_ring R] (I : ideal R) :

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

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

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

Equations
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
@[simp]
theorem ideal.radical_minimal_primes {R : Type u_1} [comm_ring R] {I : ideal R} :
@[simp]
theorem ideal.Inf_minimal_primes {R : Type u_1} [comm_ring R] {I : ideal R} :
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 ) :
(p' : ideal S), p'.is_prime p' = p
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 I).minimal_primes) :
(p' : ideal S), p'.is_prime I p' p' = p
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 I).minimal_primes) :
(p' : ideal S) (H : p' I.minimal_primes), p' = p
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) :
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) :