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} : I ∈ J.minimalPrimes ↔ I.IsPrime ∧ J ≤ I

theorem Ring.KrullDimLE.mem_minimalPrimes_iff_le_of_isPrime {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] {I J : Ideal R} [I.IsPrime] : I ∈ J.minimalPrimes ↔ J ≤ I

theorem Ring.KrullDimLE.minimalPrimes_eq_setOf_isPrime (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] : minimalPrimes R = {I : Ideal R | I.IsPrime}

theorem Ring.KrullDimLE.minimalPrimes_eq_setOf_isMaximal (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] : minimalPrimes R = {I : Ideal R | I.IsMaximal}

theorem Ring.KrullDimLE.isField_of_isDomain {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsDomain R] : IsField R

theorem ringKrullDimZero_iff_ringKrullDim_eq_zero {R : Type u_1} [CommSemiring R] [Nontrivial R] : Ring.KrullDimLE 0 R ↔ ringKrullDim R = 0

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} : M ≤ IsUnit.submonoid R ↔ 0 ∉ M

theorem Ring.KrullDimLE.existsUnique_isPrime (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] : ∃! I : Ideal R, I.IsPrime

theorem Ring.KrullDimLE.eq_maximalIdeal_of_isPrime {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] (J : Ideal R) [J.IsPrime] : J = IsLocalRing.maximalIdeal R

theorem Ring.KrullDimLE.radical_eq_maximalIdeal {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] (I : Ideal R) (hI : I ≠ ⊤) : I.radical = IsLocalRing.maximalIdeal R

theorem Ring.KrullDimLE.subsingleton_primeSpectrum (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] : Subsingleton (PrimeSpectrum R)

theorem Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] {x : R} : IsNilpotent x ↔ x ∈ IsLocalRing.maximalIdeal R

theorem Ring.KrullDimLE.isNilpotent_iff_mem_nonunits {R : Type u_1} [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] {x : R} : IsNilpotent x ↔ x ∈ nonunits R

theorem Ring.KrullDimLE.nilradical_eq_maximalIdeal (R : Type u_1) [CommSemiring R] [KrullDimLE 0 R] [IsLocalRing R] : nilradical R = IsLocalRing.maximalIdeal R

theorem IsLocalRing.of_isMaximal_nilradical (R : Type u_1) [CommSemiring R] [(nilradical R).IsMaximal] : IsLocalRing R

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 := ⋯ }

theorem Ideal.jacobson_eq_radical {R : Type u_1} [CommRing R] (I : Ideal R) [Ring.KrullDimLE 0 R] : I.jacobson = I.radical

@[instance 100]

instance instIsJacobsonRingOfKrullDimLEOfNatNat {R : Type u_1} [CommRing R] [Ring.KrullDimLE 0 R] : IsJacobsonRing R

@[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] : J = K

@[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] : J = IsLocalRing.maximalIdeal R

Alias of Ring.KrullDimLE.eq_maximalIdeal_of_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} : IsNilpotent x ↔ x ∈ IsLocalRing.maximalIdeal R

Alias of Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal.

@[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} : IsNilpotent x ↔ x ∈ nonunits R

Alias of Ring.KrullDimLE.isNilpotent_iff_mem_nonunits.

@[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

• @PrimeSpectrum.primeSpectrum_unique_of_localization_at_minimal = @PrimeSpectrum.unique_of_ringKrullDimLE_zero

@[deprecated IsLocalRing.of_isMaximal_nilradical (since := "2024-11-09")]

theorem LocalRing.of_nilradical_isMaximal (R : Type u_1) [CommSemiring R] [(nilradical R).IsMaximal] : IsLocalRing R

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] : R ≃ₐ[R] 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.

Equations

• localizationEquivSelfOfNilradicalIsMaximal h' = IsLocalization.atUnits R M ⋯