Maximal ideal of local rings

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

instance LocalRing.maximalIdeal.isMaximal (R : Type u_1) [CommSemiring R] [LocalRing R] : (LocalRing.maximalIdeal R).IsMaximal

Equations

• ⋯ = ⋯

theorem LocalRing.maximal_ideal_unique (R : Type u_1) [CommSemiring R] [LocalRing R] : ∃! I : Ideal R, I.IsMaximal

theorem LocalRing.eq_maximalIdeal {R : Type u_1} [CommSemiring R] [LocalRing R] {I : Ideal R} (hI : I.IsMaximal) : I = LocalRing.maximalIdeal R

theorem LocalRing.le_maximalIdeal {R : Type u_1} [CommSemiring R] [LocalRing R] {J : Ideal R} (hJ : J ≠ ⊤) : J ≤ LocalRing.maximalIdeal R

@[simp]

theorem LocalRing.mem_maximalIdeal {R : Type u_1} [CommSemiring R] [LocalRing R] (x : R) : x ∈ LocalRing.maximalIdeal R ↔ x ∈ nonunits R

theorem LocalRing.not_mem_maximalIdeal {R : Type u_1} [CommSemiring R] [LocalRing R] {x : R} : x ∉ LocalRing.maximalIdeal R ↔ IsUnit x

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

theorem LocalRing.isField_iff_maximalIdeal_eq {R : Type u_1} [CommSemiring R] [LocalRing R] : IsField R ↔ LocalRing.maximalIdeal R = ⊥

theorem LocalRing.maximalIdeal_le_jacobson {R : Type u_1} [CommRing R] [LocalRing R] (I : Ideal R) : LocalRing.maximalIdeal R ≤ I.jacobson

theorem LocalRing.jacobson_eq_maximalIdeal {R : Type u_1} [CommRing R] [LocalRing R] (I : Ideal R) (h : I ≠ ⊤) : I.jacobson = LocalRing.maximalIdeal R

theorem LocalRing.ker_eq_maximalIdeal {R : Type u_1} {K : Type u_3} [CommRing R] [LocalRing R] [Field K] (φ : R →+* K) (hφ : Function.Surjective ⇑φ) : RingHom.ker φ = LocalRing.maximalIdeal R

theorem LocalRing.maximalIdeal_eq_bot {R : Type u_4} [Field R] : LocalRing.maximalIdeal R = ⊥

theorem LocalRing.of_nilradical_isMaximal {R : Type u_4} [CommSemiring R] [h : (nilradical R).IsMaximal] : LocalRing R

noncomputable def localizationEquivSelfOfNilradicalIsMaximal {R : Type u_4} [CommSemiring R] {S : Type u_5} [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 ⋯