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

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

Equations

• I.minimalPrimes = {p : Ideal R | Minimal (fun (q : Ideal R) => q.IsPrime ∧ I ≤ q) p}

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 ⊥.

Equations

• minimalPrimes R = ⊥.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.iUnion_minimalPrimes {R : Type u_1} [CommSemiring R] {I : Ideal R} : ⋃ p ∈ I.minimalPrimes, ↑p = {x : R | ∃ y ∉ I.radical, x * y ∈ I.radical}

theorem Ideal.exists_mul_mem_of_mem_minimalPrimes {R : Type u_1} [CommSemiring R] {I p : Ideal R} (hp : p ∈ I.minimalPrimes) {x : R} (hx : x ∈ p) : ∃ y ∉ I, x * y ∈ I

theorem Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes {R : Type u_1} [CommSemiring R] {p : Ideal R} (hp : p ∈ minimalPrimes R) : Disjoint ↑p ↑(nonZeroDivisors R)

minimal primes are contained in zero divisors.

theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Ideal R) (H : p ∈ minimalPrimes R) : ∃ (p' : Ideal S), p'.IsPrime ∧ 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 ∈ (comap f I).minimalPrimes) : ∃ (p' : Ideal S), p'.IsPrime ∧ I ≤ p' ∧ 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 ∈ (comap f I).minimalPrimes) : ∃ p' ∈ I.minimalPrimes, comap f p' = p

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

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) : (comap f I).minimalPrimes = comap f '' I.minimalPrimes

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

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

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

theorem IsLocalization.AtPrime.prime_unique_of_minimal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] (hMin : I ∈ minimalPrimes R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization.AtPrime S I] {J K : Ideal S} [J.IsPrime] [K.IsPrime] : J = K

theorem Localization.AtPrime.prime_unique_of_minimal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] (hMin : I ∈ minimalPrimes R) (J : Ideal (Localization I.primeCompl)) [J.IsPrime] : J = IsLocalRing.maximalIdeal (Localization I.primeCompl)

theorem Localization.AtPrime.nilpotent_iff_mem_maximal_of_minimal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] (hMin : I ∈ minimalPrimes R) {x : Localization I.primeCompl} : IsNilpotent x ↔ x ∈ IsLocalRing.maximalIdeal (Localization I.primeCompl)

theorem Localization.AtPrime.nilpotent_iff_not_unit_of_minimal {R : Type u_1} [CommSemiring R] {I : Ideal R} [hI : I.IsPrime] (hMin : I ∈ minimalPrimes R) {x : Localization I.primeCompl} : IsNilpotent x ↔ x ∈ nonunits (Localization I.primeCompl)

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 = ⊤