feat (LocalRing/MaximalIdeal/Basic): add LocalRing.not_mem_maximalIdeal and nilradmax_localization_IsSelf

Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

@@ -53,6 +53,13 @@ theorem le_maximalIdeal {J : Ideal R} (hJ : J ≠ ⊤) : J ≤ maximalIdeal R :=
 theorem mem_maximalIdeal (x) : x ∈ maximalIdeal R ↔ x ∈ nonunits R :=
   Iff.rfl
 
+/--
+An element `x` of a commutative local semiring is not contained in the maximal ideal
+iff it is a unit.
+-/
+theorem not_mem_maximalIdeal (x : R) : x ∉ maximalIdeal R ↔ IsUnit x := by
+  simp only [mem_maximalIdeal, mem_nonunits_iff, not_not]
+
 theorem isField_iff_maximalIdeal_eq : IsField R ↔ maximalIdeal R = ⊥ :=
   not_iff_not.mp
     ⟨Ring.ne_bot_of_isMaximal_of_not_isField inferInstance, fun h =>
@@ -99,3 +106,31 @@ end LocalRing
 
 theorem LocalRing.maximalIdeal_eq_bot {R : Type*} [Field R] : LocalRing.maximalIdeal R = ⊥ :=
   LocalRing.isField_iff_maximalIdeal_eq.mp (Field.toIsField R)
+
+section Nilrad_max_localization
+
+open Ideal
+
+variable {R : Type*} [CommSemiring R] {S : Type*} [CommSemiring S] [Algebra R S] {M : Submonoid R}
+
+/--
+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`. -/
+noncomputable def nilradmaxlocalizationIsSelf (h : (nilradical R).IsMaximal) (h' : (0 : R) ∉ M)
+    [IsLocalization M S] : R ≃ₐ[R] S := by
+  have : LocalRing R := by
+    refine LocalRing.of_unique_max_ideal ⟨nilradical R, h, fun I hI ↦ ?_⟩
+    rw [nilradical_eq_sInf] at h ⊢
+    exact (IsMaximal.eq_of_le h hI.ne_top (sInf_le hI.isPrime)).symm
+  have : ∀ m ∈ M, IsUnit m := by
+    intro m hm
+    apply (LocalRing.not_mem_maximalIdeal m).mp
+    rw [← LocalRing.eq_maximalIdeal h]
+    intro hm'
+    obtain ⟨k, hk⟩ := mem_nilradical.mp hm'
+    rw [← hk] at h'
+    exact h' (Submonoid.pow_mem M hm k)
+  exact IsLocalization.atUnits _ _ this
+
+end Nilrad_max_localization