Minimal primes and localization

We provide various results concerning the minimal primes above an ideal that require the theory of localizations.

Main results

• 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.
• IsLocalization.minimalPrimes_comap: If A is a localization of R with respect to the submonoid S, J is an ideal of A, then the minimal primes over the preimage of J (under R →+* A) are exactly the preimages of the minimal primes over J.
• IsLocalization.minimalPrimes_map: If A is a localization of R with respect to the submonoid S, J is an ideal of R, then the minimal primes over the span of the image of J (under R →+* A) are exactly the ideals of A such that the preimage of which is a minimal prime over J.
• Localization.AtPrime.prime_unique_of_minimal: When localizing at a minimal prime ideal I, the resulting ring only has a single prime ideal.

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 IsSMulRegular.notMem_of_mem_minimalPrimes {R : Type u_1} [CommSemiring R] {M : Type u_3} [AddCommMonoid M] [Module R M] {x : R} (reg : IsSMulRegular M x) {p : Ideal R} (hp : p ∈ (Module.annihilator R M).minimalPrimes) : x ∉ p

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 notMem_nonZeroDivisors_of_mem_mem_minimalPrimes {R : Type u_1} [CommSemiring R] {x : R} {q : Ideal R} (hx : x ∈ q) (hq : q ∈ minimalPrimes R) : x ∉ nonZeroDivisors R

An element of a minimal prime is a zero divisor.

theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring 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_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

Stacks Tag 00FK

theorem Ideal.exists_minimalPrimes_comap_eq {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring 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.minimalPrimes_comap_subset {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (f : R →+* S) (J : Ideal S) : (comap f J).minimalPrimes ⊆ comap f '' J.minimalPrimes

theorem Ideal.minimalPrimes_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_map_of_surjective {R : Type u_1} [CommRing R] {S : Type u_3} [CommRing S] {f : R →+* S} (hf : Function.Surjective ⇑f) (I : Ideal R) : (map f I).minimalPrimes = map f '' (I ⊔ RingHom.ker f).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 IsLocalization.minimalPrimes_map {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] (J : Ideal R) : (Ideal.map (algebraMap R A) J).minimalPrimes = Ideal.under R ⁻¹' J.minimalPrimes

theorem IsLocalization.minimalPrimes_comap {R : Type u_1} [CommSemiring R] (S : Submonoid R) (A : Type u_2) [CommSemiring A] [Algebra R A] [IsLocalization S A] (J : Ideal A) : (Ideal.comap (algebraMap R A) J).minimalPrimes = Ideal.comap (algebraMap R A) '' J.minimalPrimes

theorem IsLocalization.AtPrime.radical_map_of_mem_minimalPrimes {R : Type u_1} [CommSemiring R] (A : Type u_2) [CommSemiring A] [Algebra R A] (q : Ideal R) [hqp : q.IsPrime] [IsLocalization.AtPrime A q] (I : Ideal R) (hIq : q ∈ I.minimalPrimes) : (Ideal.map (algebraMap R A) I).radical = Ideal.map (algebraMap R A) q