Zero-dimensional rings #
We provide further API for zero-dimensional rings.
Basic definitions and lemmas are provided in Mathlib/RingTheory/KrullDimension/Basic.lean
.
theorem
Ring.KrullDimLE.mem_minimalPrimes_iff
{R : Type u_1}
[CommSemiring R]
[KrullDimLE 0 R]
{I J : Ideal R}
:
theorem
Ring.KrullDimLE.mem_minimalPrimes_iff_le_of_isPrime
{R : Type u_1}
[CommSemiring R]
[KrullDimLE 0 R]
{I J : Ideal R}
[I.IsPrime]
:
theorem
Ring.KrullDimLE.minimalPrimes_eq_setOf_isPrime
(R : Type u_1)
[CommSemiring R]
[KrullDimLE 0 R]
:
theorem
Ring.KrullDimLE.minimalPrimes_eq_setOf_isMaximal
(R : Type u_1)
[CommSemiring R]
[KrullDimLE 0 R]
:
theorem
Ring.KrullDimLE.isField_of_isDomain
{R : Type u_1}
[CommSemiring R]
[KrullDimLE 0 R]
[IsDomain R]
:
IsField R
theorem
Ring.krullDimLE_zero_and_isLocalRing_tfae
(R : Type u_1)
[CommSemiring R]
:
[KrullDimLE 0 R ∧ IsLocalRing R, ∃! I : Ideal R, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x, (nilradical R).IsMaximal].TFAE
@[simp]
theorem
le_isUnit_iff_zero_not_mem
{R : Type u_1}
[CommSemiring R]
[Ring.KrullDimLE 0 R]
[IsLocalRing R]
{M : Submonoid R}
:
theorem
Ring.KrullDimLE.existsUnique_isPrime
(R : Type u_1)
[CommSemiring R]
[KrullDimLE 0 R]
[IsLocalRing R]
:
theorem
Ring.KrullDimLE.eq_maximalIdeal_of_isPrime
{R : Type u_1}
[CommSemiring R]
[KrullDimLE 0 R]
[IsLocalRing R]
(J : Ideal R)
[J.IsPrime]
:
theorem
Ring.KrullDimLE.subsingleton_primeSpectrum
(R : Type u_1)
[CommSemiring R]
[KrullDimLE 0 R]
[IsLocalRing R]
:
theorem
Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal
{R : Type u_1}
[CommSemiring R]
[KrullDimLE 0 R]
[IsLocalRing R]
{x : R}
:
theorem
Ring.KrullDimLE.isNilpotent_iff_mem_nonunits
{R : Type u_1}
[CommSemiring R]
[KrullDimLE 0 R]
[IsLocalRing R]
{x : R}
:
theorem
Ring.KrullDimLE.nilradical_eq_maximalIdeal
(R : Type u_1)
[CommSemiring R]
[KrullDimLE 0 R]
[IsLocalRing R]
:
theorem
IsLocalRing.of_isMaximal_nilradical
(R : Type u_1)
[CommSemiring R]
[(nilradical R).IsMaximal]
:
theorem
Ring.KrullDimLE.of_isMaximal_nilradical
(R : Type u_1)
[CommSemiring R]
[(nilradical R).IsMaximal]
:
KrullDimLE 0 R
theorem
Ring.KrullDimLE.of_isLocalization
{R : Type u_1}
[CommSemiring R]
(p : Ideal R)
(hp : p ∈ minimalPrimes R)
(S : Type u_2)
[CommSemiring S]
[Algebra R S]
[IsLocalization.AtPrime S p]
:
KrullDimLE 0 S
theorem
Ring.KrullDimLE.isField_of_isReduced
{R : Type u_1}
[CommSemiring R]
[KrullDimLE 0 R]
[IsReduced R]
[IsLocalRing R]
:
IsField R
instance
PrimeSpectrum.unique_of_ringKrullDimLE_zero
{R : Type u_1}
[CommSemiring R]
[Ring.KrullDimLE 0 R]
[IsLocalRing R]
:
Unique (PrimeSpectrum R)
Equations
- PrimeSpectrum.unique_of_ringKrullDimLE_zero = { default := IsLocalRing.closedPoint R, uniq := ⋯ }
@[instance 100]
@[deprecated Ring.KrullDimLE.existsUnique_isPrime (since := "2024-12-20")]
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]
:
@[deprecated Ring.KrullDimLE.eq_maximalIdeal_of_isPrime (since := "2024-12-20")]
theorem
Localization.AtPrime.prime_unique_of_minimal
{R : Type u_1}
[CommSemiring R]
[Ring.KrullDimLE 0 R]
[IsLocalRing R]
(J : Ideal R)
[J.IsPrime]
:
@[deprecated Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal (since := "2024-12-20")]
theorem
Localization.AtPrime.nilpotent_iff_mem_maximal_of_minimal
{R : Type u_1}
[CommSemiring R]
[Ring.KrullDimLE 0 R]
[IsLocalRing R]
{x : R}
:
@[deprecated Ring.KrullDimLE.isNilpotent_iff_mem_nonunits (since := "2024-12-20")]
theorem
Localization.AtPrime.nilpotent_iff_not_unit_of_minimal
{R : Type u_1}
[CommSemiring R]
[Ring.KrullDimLE 0 R]
[IsLocalRing R]
{x : R}
:
@[deprecated PrimeSpectrum.unique_of_ringKrullDimLE_zero "Use `PrimeSpectrum.unique_of_ringKrullDimLE_zero` with
`Ring.KrullDimLE.of_isLocalization`" (since := "2024-12-20")]
def
PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal
{R : Type u_1}
[CommSemiring R]
[Ring.KrullDimLE 0 R]
[IsLocalRing R]
:
Unique (PrimeSpectrum R)
Alias of PrimeSpectrum.unique_of_ringKrullDimLE_zero
.
Equations
Instances For
@[deprecated IsLocalRing.of_isMaximal_nilradical (since := "2024-11-09")]
theorem
LocalRing.of_nilradical_isMaximal
(R : Type u_1)
[CommSemiring R]
[(nilradical R).IsMaximal]
:
Alias of IsLocalRing.of_isMaximal_nilradical
.
@[deprecated IsLocalization.atUnits (since := "2024-12-20")]
noncomputable def
localizationEquivSelfOfNilradicalIsMaximal
{R : Type u_1}
[CommSemiring R]
{S : Type u_2}
[CommSemiring S]
[Algebra R S]
{M : Submonoid R}
[h : (nilradical R).IsMaximal]
(h' : 0 ∉ M)
[IsLocalization M S]
:
Let S
be the localization of a commutative semiring R
at a submonoid M
that does not
contain 0. If the nilradical of R
is maximal then there is a R
-algebra isomorphism between
R
and S
.