# Minimal primes #

We provide various results concerning the minimal primes above an ideal

## Main results #

• Ideal.minimalPrimes: I.minimalPrimes is the set of ideals that are minimal primes over I.
• minimalPrimes: minimalPrimes R is the set of minimal primes of R.
• Ideal.exists_minimalPrimes_le: Every prime ideal over I contains a minimal prime over I.
• Ideal.radical_minimalPrimes: The minimal primes over I.radical are precisely the minimal primes over I.
• Ideal.sInf_minimalPrimes: The intersection of minimal primes over I is I.radical.
• Ideal.exists_minimalPrimes_comap_eq If p is a minimal prime over f ⁻¹ I, then it is the preimage of some minimal prime over I.
• Ideal.minimalPrimes_eq_comap: The minimal primes over I are precisely the preimages of minimal primes of R ⧸ I.
• Localization.AtPrime.prime_unique_of_minimal: When localizing at a minimal prime ideal I, the resulting ring only has a single prime ideal.
def Ideal.minimalPrimes {R : Type u_1} [] (I : ) :
Set ()

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

Equations
Instances For
def minimalPrimes (R : Type u_1) [] :
Set ()

minimalPrimes R is the set of minimal primes of R. This is defined as Ideal.minimalPrimes ⊥.

Equations
• = .minimalPrimes
Instances For
theorem minimalPrimes_eq_minimals {R : Type u_1} [] :
= minimals (fun (x x_1 : ) => x x_1) (setOf Ideal.IsPrime)
theorem Ideal.exists_minimalPrimes_le {R : Type u_1} [] {I : } {J : } [J.IsPrime] (e : I J) :
pI.minimalPrimes, p J
@[simp]
theorem Ideal.radical_minimalPrimes {R : Type u_1} [] {I : } :
@[simp]
theorem Ideal.sInf_minimalPrimes {R : Type u_1} [] {I : } :
sInf I.minimalPrimes = I.radical
theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {R : Type u_1} {S : Type u_2} [] [] {f : R →+* S} (hf : ) (p : ) (H : ) :
∃ (p' : ), p'.IsPrime Ideal.comap f p' = p
theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {R : Type u_1} {S : Type u_2} [] [] {I : } (f : R →+* S) (p : ) (H : p ().minimalPrimes) :
∃ (p' : ), p'.IsPrime I p' Ideal.comap f p' = p
theorem Ideal.exists_minimalPrimes_comap_eq {R : Type u_1} {S : Type u_2} [] [] {I : } (f : R →+* S) (p : ) (H : p ().minimalPrimes) :
p'I.minimalPrimes, Ideal.comap f p' = p
theorem Ideal.minimal_primes_comap_of_surjective {R : Type u_1} {S : Type u_2} [] [] {f : R →+* S} (hf : ) {I : } {J : } (h : J I.minimalPrimes) :
().minimalPrimes
theorem Ideal.comap_minimalPrimes_eq_of_surjective {R : Type u_1} {S : Type u_2} [] [] {f : R →+* S} (hf : ) (I : ) :
().minimalPrimes = '' I.minimalPrimes
theorem Ideal.minimalPrimes_eq_comap {R : Type u_1} [] {I : } :
I.minimalPrimes = '' minimalPrimes (R I)
theorem Ideal.minimalPrimes_eq_subsingleton {R : Type u_1} [] {I : } (hI : I.IsPrimary) :