Documentation

Mathlib.RingTheory.Ideal.MinimalPrime

Minimal primes #

We provide various results concerning the minimal primes above an ideal

Main results #

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

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

Equations
def minimalPrimes (R : Type u_1) [CommSemiring R] :

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

Equations
theorem minimalPrimes_eq_minimals {R : Type u_1} [CommSemiring R] :
minimalPrimes R = {x : Ideal R | Minimal Ideal.IsPrime x}
theorem Ideal.exists_minimalPrimes_le {R : Type u_1} [CommSemiring R] {I : Ideal R} {J : Ideal R} [J.IsPrime] (e : I J) :
pI.minimalPrimes, p J
@[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.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 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.comap f I).minimalPrimes) :
∃ (p' : Ideal S), p'.IsPrime 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.comap f I).minimalPrimes) :
p'I.minimalPrimes, Ideal.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 : Ideal S} {J : Ideal S} (h : J I.minimalPrimes) :
Ideal.comap f J (Ideal.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) :
(Ideal.comap f I).minimalPrimes = Ideal.comap f '' I.minimalPrimes
theorem Ideal.minimalPrimes_eq_comap {R : Type u_1} [CommRing R] {I : Ideal R} :
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 : Ideal S} {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] :
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} :
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} :