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 overI
.minimalPrimes
:minimalPrimes R
is the set of minimal primes ofR
.Ideal.exists_minimalPrimes_le
: Every prime ideal overI
contains a minimal prime overI
.Ideal.radical_minimalPrimes
: The minimal primes overI.radical
are precisely the minimal primes overI
.Ideal.sInf_minimalPrimes
: The intersection of minimal primes overI
isI.radical
.Ideal.exists_minimalPrimes_comap_eq
Ifp
is a minimal prime overf ⁻¹ I
, then it is the preimage of some minimal prime overI
.Ideal.minimalPrimes_eq_comap
: The minimal primes overI
are precisely the preimages of minimal primes ofR ⧸ I
.Localization.AtPrime.prime_unique_of_minimal
: When localizing at a minimal prime idealI
, the resulting ring only has a single prime ideal.
I.minimalPrimes
is the set of ideals that are minimal primes over I
.
Equations
- Ideal.minimalPrimes I = minimals (fun (x x_1 : Ideal R) => x ≤ x_1) {p : Ideal R | Ideal.IsPrime p ∧ I ≤ p}
Instances For
minimalPrimes R
is the set of minimal primes of R
.
This is defined as Ideal.minimalPrimes ⊥
.
Equations
Instances For
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
@[simp]
@[simp]
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
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 ∈ 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)
:
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)
:
theorem
Ideal.minimalPrimes_eq_subsingleton_self
{R : Type u_1}
[CommRing R]
{I : Ideal R}
[Ideal.IsPrime I]
:
Ideal.minimalPrimes I = {I}
theorem
IsLocalization.AtPrime.prime_unique_of_minimal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : Ideal.IsPrime I]
(hMin : I ∈ minimalPrimes R)
{S : Type u_2}
[CommSemiring S]
[Algebra R S]
[IsLocalization.AtPrime S I]
{J : Ideal S}
{K : Ideal S}
[Ideal.IsPrime J]
[Ideal.IsPrime K]
:
J = K
theorem
Localization.AtPrime.prime_unique_of_minimal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : Ideal.IsPrime I]
(hMin : I ∈ minimalPrimes R)
(J : Ideal (Localization (Ideal.primeCompl I)))
[Ideal.IsPrime J]
:
theorem
Localization.AtPrime.nilpotent_iff_mem_maximal_of_minimal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : Ideal.IsPrime I]
(hMin : I ∈ minimalPrimes R)
{x : Localization (Ideal.primeCompl I)}
:
theorem
Localization.AtPrime.nilpotent_iff_not_unit_of_minimal
{R : Type u_1}
[CommSemiring R]
{I : Ideal R}
[hI : Ideal.IsPrime I]
(hMin : I ∈ minimalPrimes R)
{x : Localization (Ideal.primeCompl I)}
:
IsNilpotent x ↔ x ∈ nonunits (Localization (Ideal.primeCompl I))