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
Instances For
    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
    Instances For
      theorem minimalPrimes_eq_minimals {R : Type u_1} [CommSemiring R] :
      minimalPrimes R = minimals (fun (x x_1 : Ideal R) => x x_1) (setOf Ideal.IsPrime)
      theorem Ideal.exists_minimalPrimes_le {R : Type u_1} [CommSemiring R] {I : Ideal R} {J : Ideal R} [Ideal.IsPrime J] (e : I J) :
      ∃ p ∈ Ideal.minimalPrimes I, p J
      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), 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 S), 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' ∈ Ideal.minimalPrimes I, Ideal.comap f p' = p