feat(RingTheory/Localization): R ⧸ pⁿ ≃+* Rₚ ⧸ (maximalIdeal Rₚ)ⁿ

Author: wwylele

Mathlib/Algebra/Ring/Subring/Basic.lean

@@ -915,6 +915,14 @@ def subringCongr (h : s = t) : s ≃+* t :=
     map_mul' := fun _ _ => rfl
     map_add' := fun _ _ => rfl }
 
+@[simp]
+theorem subringCongr_symm (h : s = t) :
+    (subringCongr h).symm = subringCongr (h.symm) := rfl
+
+@[simp]
+theorem coe_subringCongr_apply (h : s = t) (x : s) :
+    (subringCongr h x).val = x.val := rfl
+
 /-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
 `RingHom.range`. -/
 def ofLeftInverse {g : S → R} {f : R →+* S} (h : Function.LeftInverse g f) : R ≃+* f.range :=

Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean

@@ -90,3 +90,10 @@ theorem Ideal.Quotient.isUnit_mk_pow_iff_notMem [I.IsMaximal] {n : ℕ} (hn : n
   let := Ideal.Quotient.field I
   rw [isUnit_mk_pow_iff_isUnit_mk I hn, isUnit_iff_ne_zero]
   exact Ideal.Quotient.eq_zero_iff_mem.not
+
+theorem Ideal.Quotient.notMem_of_isUnit_mk_pow [I.IsMaximal] {n : ℕ} {x : S} (hx : x ∉ I) :
+    IsUnit (mk (I ^ n) x) := by
+  by_cases! hn : n = 0
+  · rw [pow_eq_top_iff.mpr (Or.inr hn)]
+    exact isUnit_of_subsingleton _
+  exact (isUnit_mk_pow_iff_notMem I hn).mpr hx

Mathlib/RingTheory/Localization/AtPrime/Basic.lean

@@ -11,6 +11,7 @@ public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
 public import Mathlib.RingTheory.Localization.Basic
 public import Mathlib.RingTheory.Localization.Ideal
 public import Mathlib.RingTheory.Ideal.MinimalPrime.Basic
+public import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
 
 /-!
 # Localizations of commutative rings at the complement of a prime ideal
@@ -508,6 +509,43 @@ theorem equivQuotMaximalIdeal_symm_apply_mk (x : R) (s : p.primeCompl) :
 @[deprecated (since := "2025-11-13")] alias _root_.equivQuotMaximalIdealOfIsLocalization :=
   equivQuotMaximalIdeal
 
+set_option backward.isDefEq.respectTransparency false in
+/-- The isomorphism `R ⧸ p ^ n ≃+* Rₚ ⧸ maximalIdeal Rₚ ^ n`, where `Rₚ` satisfies
+`IsLocalization.AtPrime Rₚ p`. -/
+noncomputable
+def equivQuotMaximalIdealPow (n : ℕ) : R ⧸ p ^ n ≃+* Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ ^ n := by
+  refine Subring.topEquiv.symm.trans <| -- R ⧸ p ^ n ≃ (⊤ : Subring (R ⧸ p ^ n))
+    (RingEquiv.subringCongr ?_).trans <| -- ⊤ = (R ⧸ p ^ n ← Rₚ / ker).range
+    (IsLocalization.lift fun (u : p.primeCompl) ↦ -- (R ⧸ p ^ n ← Rₚ) => R ⧸ p ^ n ← Rₚ / ker
+      Ideal.Quotient.notMem_of_isUnit_mk_pow _
+      (mem_primeCompl_iff.mp u.prop)).quotientKerEquivRange.symm.trans <|
+    quotEquivOfEq ?_ -- ker = maximalIdeal ^ n
+  · symm
+    rw [RingHom.range_eq_top, IsLocalization.lift_surjective_iff]
+    intro u
+    obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective u
+    exact ⟨⟨x, 1⟩, by simp [hx]⟩
+  · ext x
+    obtain ⟨a, b, rfl⟩ := IsLocalization.exists_mk'_eq p.primeCompl x
+    suffices a ∈ p ^ n ↔ algebraMap R Rₚ a ∈ IsLocalRing.maximalIdeal Rₚ ^ n by
+      simpa [Ideal.Quotient.eq_zero_iff_mem, IsLocalization.mk'_mem_iff]
+    rw [← map_eq_maximalIdeal p Rₚ, ← Ideal.map_pow,
+      algebraMap_mem_map_algebraMap_iff p.primeCompl Rₚ]
+    refine ⟨fun h ↦ ⟨1, by simp, by simp [h]⟩, fun ⟨m, hm, h⟩ ↦ ?_⟩
+    exact (IsMaximal.mul_mem_pow _ h).resolve_left (mem_primeCompl_iff.mp hm)
+
+@[simp]
+theorem equivQuotMaximalIdealPow_apply_mk (n : ℕ) (x : R) :
+    equivQuotMaximalIdealPow p Rₚ n (Ideal.Quotient.mk _ x) =
+    Ideal.Quotient.mk _ (algebraMap R Rₚ x) := by
+  simp only [equivQuotMaximalIdealPow, RingEquiv.coe_trans, Function.comp_apply]
+  rw [← RingEquiv.eq_symm_apply, RingEquiv.symm_apply_eq]
+  simp only [RingHom.quotientKerEquivRange, Ideal.quotEquivOfEq_symm, Ideal.quotEquivOfEq_mk,
+    RingEquiv.coe_trans, Function.comp_apply, RingHom.quotientKerEquivOfSurjective_apply_mk]
+  rw [← RingEquiv.eq_symm_apply]
+  ext
+  simp
+
 variable {Sₚ : Type*} [CommRing S] [Algebra R S] [CommRing Sₚ] [Algebra S Sₚ] [Algebra R Sₚ]
 variable [Algebra Rₚ Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
 variable [IsScalarTower R S Sₚ]