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.

Further results that need the theory of localizations can be found in Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean.

def Ideal.minimalPrimes {R : Type u_1} [CommSemiring R] (I : Ideal R) : Set (Ideal R)

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

def minimalPrimes (R : Type u_1) [CommSemiring R] : Set (Ideal R)

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

theorem minimalPrimes_eq_minimals {R : Type u_1} [CommSemiring R] : minimalPrimes R = {x : Ideal R | Minimal Ideal.IsPrime x}

theorem Ideal.minimalPrimes_isPrime {R : Type u_1} [CommSemiring R] {I p : Ideal R} (h : p ∈ I.minimalPrimes) : p.IsPrime

theorem Ideal.exists_minimalPrimes_le {R : Type u_1} [CommSemiring R] {I J : Ideal R} [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.minimalPrimes, p ≤ J

theorem Ideal.nonempty_minimalPrimes {R : Type u_1} [CommSemiring R] {I : Ideal R} (h : I ≠ ⊤) : Nonempty ↑I.minimalPrimes

theorem Ideal.eq_bot_of_minimalPrimes_eq_empty {R : Type u_1} [CommSemiring R] {I : Ideal R} (h : I.minimalPrimes = ∅) : I = ⊤

@[simp]

theorem Ideal.radical_minimalPrimes {R : Type u_1} [CommSemiring R] {I : Ideal R} : I.radical.minimalPrimes = I.minimalPrimes

@[simp]

theorem Ideal.sInf_minimalPrimes {R : Type u_1} [CommSemiring R] {I : Ideal R} : sInf I.minimalPrimes = I.radical

theorem Ideal.minimalPrimes_eq_subsingleton {R : Type u_1} [CommSemiring R] {I : Ideal R} (hI : I.IsPrimary) : I.minimalPrimes = {I.radical}

theorem Ideal.minimalPrimes_eq_subsingleton_self {R : Type u_1} [CommSemiring R] {I : Ideal R} [I.IsPrime] : I.minimalPrimes = {I}

theorem IsDomain.minimalPrimes_eq_singleton_bot (R : Type u_1) [CommSemiring R] [IsDomain R] : minimalPrimes R = {⊥}

theorem Ideal.minimalPrimes_top {R : Type u_1} [CommSemiring R] : ⊤.minimalPrimes = ∅

theorem Ideal.minimalPrimes_eq_empty_iff {R : Type u_1} [CommSemiring R] (I : Ideal R) : I.minimalPrimes = ∅ ↔ I = ⊤

theorem Ideal.mem_minimalPrimes_sup {R : Type u_2} [CommRing R] {p I J : Ideal R} [p.IsPrime] (hle : I ≤ p) (h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes) : p ∈ (I ⊔ J).minimalPrimes

theorem Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommRing S] [Algebra R S] {I p : Ideal R} {P : Ideal S} [P.IsPrime] [P.LiesOver p] (hI : p ∈ I.minimalPrimes) {J : Ideal S} (hJP : J ≤ P) (hJ : map (Quotient.mk (map (algebraMap R S) p)) P ∈ (map (Quotient.mk (map (algebraMap R S) p)) J).minimalPrimes) : P ∈ (map (algebraMap R S) I ⊔ J).minimalPrimes

If P lies over p, p is a minimal prime over I and the image of P is a minimal prime over the image of J in S ⧸ p S, then P is a minimal prime over I S ⊔ J.