# Documentation

Mathlib.RingTheory.Ideal.MinimalPrime

# 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.
def Ideal.minimalPrimes {R : Type u_1} [] (I : ) :
Set ()

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

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

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

Instances For
theorem Ideal.exists_minimalPrimes_le {R : Type u_1} [] {I : } {J : } [] (e : I J) :
p, p J
@[simp]
theorem Ideal.radical_minimalPrimes {R : Type u_1} [] {I : } :
@[simp]
theorem Ideal.sInf_minimalPrimes {R : Type u_1} [] {I : } :
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', 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 ) :
p', 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 ) :
p', Ideal.comap f p' = p
theorem Ideal.mimimal_primes_comap_of_surjective {R : Type u_1} {S : Type u_2} [] [] {f : R →+* S} (hf : ) {I : } {J : } (h : ) :
theorem Ideal.comap_minimalPrimes_eq_of_surjective {R : Type u_1} {S : Type u_2} [] [] {f : R →+* S} (hf : ) (I : ) :
theorem Ideal.minimalPrimes_eq_comap {R : Type u_1} [] {I : } :
theorem Ideal.minimalPrimes_eq_subsingleton {R : Type u_1} [] {I : } (hI : ) :
theorem Ideal.minimalPrimes_eq_subsingleton_self {R : Type u_1} [] {I : } [] :
= {I}