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} [CommRing 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_3) [CommRing R] : Set (Ideal R)

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

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

@[simp]

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

@[simp]

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

theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Injective ↑f) (p : Ideal R) (H : p ∈ minimalPrimes R) : ∃ p', Ideal.IsPrime p' ∧ Ideal.comap f p' = p

theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {I : Ideal S} (f : R →+* S) (p : Ideal R) (H : p ∈ Ideal.minimalPrimes (Ideal.comap f I)) : ∃ p', Ideal.IsPrime p' ∧ I ≤ p' ∧ Ideal.comap f p' = p

theorem Ideal.exists_minimalPrimes_comap_eq {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {I : Ideal S} (f : R →+* S) (p : Ideal R) (H : p ∈ Ideal.minimalPrimes (Ideal.comap f I)) : ∃ p', p' ∈ Ideal.minimalPrimes I ∧ Ideal.comap f p' = p

theorem Ideal.mimimal_primes_comap_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ↑f) {I : Ideal S} {J : Ideal S} (h : J ∈ Ideal.minimalPrimes I) : Ideal.comap f J ∈ Ideal.minimalPrimes (Ideal.comap f I)

theorem Ideal.comap_minimalPrimes_eq_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Surjective ↑f) (I : Ideal S) : Ideal.minimalPrimes (Ideal.comap f I) = Ideal.comap f '' Ideal.minimalPrimes I

theorem Ideal.minimalPrimes_eq_comap {R : Type u_1} [CommRing R] {I : Ideal R} : Ideal.minimalPrimes I = Ideal.comap (Ideal.Quotient.mk I) '' minimalPrimes (R ⧸ I)

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

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