# Maximal ideal of local rings #

We prove basic properties of the maximal ideal of a local ring.

source
@[simp]
theorem IsLocalRing.mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] (x : R) :
x ∈ maximalIdeal R ↔ x ∈ nonunits R
source
instance IsLocalRing.maximalIdeal.isMaximal (R : Type u_1) [CommSemiring R] [IsLocalRing R] :
(maximalIdeal R).IsMaximal
source
theorem IsLocalRing.isMaximal_iff (R : Type u_1) [CommSemiring R] [IsLocalRing R] {I : Ideal R} :
I.IsMaximal ↔ I = maximalIdeal R
source
theorem IsLocalRing.maximal_ideal_unique (R : Type u_1) [CommSemiring R] [IsLocalRing R] :
∃! I : Ideal R, I.IsMaximal
source
theorem IsLocalRing.eq_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {I : Ideal R} (hI : I.IsMaximal) :
I = maximalIdeal R
source
instance IsLocalRing.instUniqueMaximalSpectrum {R : Type u_1} [CommSemiring R] [IsLocalRing R] :
Unique (MaximalSpectrum R)

The maximal spectrum of a local ring is a singleton.

Equations

- IsLocalRing.instUniqueMaximalSpectrum = { default := { asIdeal := IsLocalRing.maximalIdeal R, isMaximal := ⋯ }, uniq := ⋯ }

source
theorem IsLocalRing.of_singleton_maximalSpectrum {R : Type u_1} [CommSemiring R] [Subsingleton (MaximalSpectrum R)] [Nonempty (MaximalSpectrum R)] :
IsLocalRing R

If the maximal spectrum of a ring is a singleton, then the ring is local.

source
theorem IsLocalRing.le_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {J : Ideal R} (hJ : J ≠ ⊤) :
J ≤ maximalIdeal R
source
theorem IsLocalRing.le_maximalIdeal_of_isPrime {R : Type u_1} [CommSemiring R] [IsLocalRing R] (p : Ideal R) [hp : p.IsPrime] :
p ≤ maximalIdeal R
source
theorem IsLocalRing.notMem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {x : R} :
x ∉ maximalIdeal R ↔ IsUnit x

An element `x` of a commutative local semiring is not contained in the maximal ideal iff it is a unit.

source
@[deprecated IsLocalRing.notMem_maximalIdeal (since := "2025-05-23")]
theorem IsLocalRing.not_mem_maximalIdeal {R : Type u_1} [CommSemiring R] [IsLocalRing R] {x : R} :
x ∉ maximalIdeal R ↔ IsUnit x

Alias of `IsLocalRing.notMem_maximalIdeal`.

An element `x` of a commutative local semiring is not contained in the maximal ideal iff it is a unit.

source
theorem IsLocalRing.isField_iff_maximalIdeal_eq {R : Type u_1} [CommSemiring R] [IsLocalRing R] :
IsField R ↔ maximalIdeal R = ⊥
source
theorem IsLocalRing.maximalIdeal_le_jacobson {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) :
maximalIdeal R ≤ I.jacobson
source
theorem IsLocalRing.jacobson_eq_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) (h : I ≠ ⊤) :
I.jacobson = maximalIdeal R
source
theorem IsLocalRing.ringJacobson_eq_maximalIdeal (R : Type u_1) [CommRing R] [IsLocalRing R] :
Ring.jacobson R = maximalIdeal R
source
theorem IsLocalRing.ker_eq_maximalIdeal {R : Type u_1} {K : Type u_3} [CommRing R] [IsLocalRing R] [DivisionRing K] (φ : R →+* K) (hφ : Function.Surjective ⇑φ) :
RingHom.ker φ = maximalIdeal R
source
theorem IsLocalRing.maximalIdeal_eq_bot {R : Type u_4} [Field R] :
maximalIdeal R = ⊥
source
theorem Subsemiring.isLocalRing_of_unit {R : Type u_1} [Semiring R] [IsLocalRing R] (S : Subsemiring R) (h_unit : ∀ (x : R) (hx : x ∈ S), IsUnit x → IsUnit ⟨x, hx⟩) :
IsLocalRing ↥S
source
theorem Subring.isLocalRing_of_unit {R : Type u_1} [Ring R] [IsLocalRing R] (S : Subring R) (h_unit : ∀ (x : R) (hx : x ∈ S), IsUnit x → IsUnit ⟨x, hx⟩) :
IsLocalRing ↥S