feat(RingTheory/LocalRing/ResidueField/Fiber): the localization of Ideal.Fiber is a quotient (leanprover-community#39196)

This PR proves that the localization of `Ideal.Fiber` is a quotient. This will be applied in leanprover-community#39189 to prove the ramification-inertia formula for finite flat extensions.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

@@ -96,6 +96,53 @@ noncomputable def Fiber.algEquivQuotient :
         simp [Localization.tensorLeftAlgEquiv_apply_one_tmul p.primeCompl])
       commutes' := by simp }
 
+/-- `p.Fiber S` is isomorphic to the quotient `Sₚ ⧸ pSₚ`. -/
+noncomputable def Fiber.algEquivAux₁ :
+    letI Sp := Localization (algebraMapSubmonoid S p.primeCompl)
+    letI pS := p.map (algebraMap R S)
+    letI : Algebra S (p.Fiber S) := rightAlgebra
+    p.Fiber S ≃ₐ[S] Sp ⧸ pS.map (algebraMap S Sp) :=
+  letI : Algebra S (p.Fiber S) := rightAlgebra
+  (Fiber.algEquivQuotient p).trans <| quotientEquivAlgOfEq S <| by
+    rw [← Localization.AtPrime.map_eq_maximalIdeal, map_map, ← IsScalarTower.algebraMap_eq,
+      IsScalarTower.algebraMap_eq R S, ← map_map]
+
+/-- The localization of the fiber `p.Fiber S` is isomorphic to a quotient of a localization. -/
+noncomputable def Fiber.algEquivAux₂ (q : Ideal (p.Fiber S)) [q.IsPrime] :
+    letI r := q.comap includeRight
+    letI Sr := Localization.AtPrime r
+    letI pS := p.map (algebraMap R S)
+    Localization.AtPrime q ≃ₐ[R] Sr ⧸ pS.map (algebraMap S Sr) :=
+  letI : Algebra S (p.Fiber S) := rightAlgebra
+  letI Sp := Localization (algebraMapSubmonoid S p.primeCompl)
+  letI pS := p.map (algebraMap R S)
+  letI SpS := S ⧸ pS
+  letI r := q.comap includeRight
+  letI Sr := Localization.AtPrime r
+  letI e₁ : p.Fiber S ≃ₐ[S] Sp ⧸ pS.map (algebraMap S Sp) := algEquivAux₁ p
+  letI q' : Ideal (Sp ⧸ pS.map (algebraMap S Sp)) := q.comap e₁.symm
+  haveI : (q'.under SpS).LiesOver r := under_liesOver_of_liesOver SpS q' (q.under S)
+  haveI : algebraMapSubmonoid SpS r.primeCompl = (q'.under SpS).primeCompl :=
+    algebraMapSubmonoid_primeCompl_of_liesOver_surjective (q'.under SpS) r Quotient.mk_surjective
+  haveI : IsLocalization (algebraMapSubmonoid SpS r.primeCompl) (Localization.AtPrime q') := by
+    convert IsLocalization.isLocalization_isLocalization_atPrime_isLocalization
+      (algebraMapSubmonoid SpS (algebraMapSubmonoid S p.primeCompl)) (Localization.AtPrime q') q'
+  haveI := IsScalarTower.to₁₃₄ R S SpS (Localization.AtPrime q')
+  haveI := IsScalarTower.to₁₃₄ R S SpS (Sr ⧸ pS.map (algebraMap S Sr))
+  ((Localization.localAlgEquiv q' q e₁.symm rfl).symm.restrictScalars R).trans
+    ((IsLocalization.algEquiv (algebraMapSubmonoid SpS r.primeCompl) (Localization.AtPrime q')
+      (Sr ⧸ pS.map (algebraMap S Sr))).restrictScalars R)
+
+/-- The localization of the fiber `p.Fiber S` is isomorphic to a quotient of a localization. -/
+noncomputable def Fiber.localizationAlgEquivQuotient (q : Ideal (p.Fiber S)) [q.IsPrime]
+    [Algebra (Localization.AtPrime p) (Localization.AtPrime (q.comap includeRight))]
+    [Localization.AtPrime.IsLiesOverAlgebra p (q.comap includeRight)] :
+    letI r := q.comap includeRight
+    letI Sr := Localization.AtPrime r
+    Localization.AtPrime q ≃ₐ[Localization.AtPrime p] Sr ⧸ p.map (algebraMap R Sr) :=
+  ((algEquivAux₂ p q).extendScalarsOfIsLocalization (Localization.AtPrime p) p.primeCompl).trans
+    (quotientEquivAlgOfEq (Localization.AtPrime p) (map_map _ _))
+
 end Ideal
 
 @[deprecated (since := "2026-05-11")] alias Fiber.algEquivQuotient := Ideal.Fiber.algEquivQuotient

Mathlib/RingTheory/Localization/Basic.lean

@@ -684,4 +684,37 @@ theorem IsLocalization.algHom_ext {R A L B : Type*}
     f = g :=
   IsLocalization.algHom_ext W h
 
+section extend
+
+variable {R A B : Type*} [CommRing R] [CommRing A] [CommRing B]
+  (S : Type*) [CommRing S] [Algebra R S] (M : Submonoid R) [IsLocalization M S]
+  [Algebra R A] [Algebra S A] [IsScalarTower R S A]
+  [Algebra R B] [Algebra S B] [IsScalarTower R S B]
+
+/-- For an algebra homomorphism `f : A →ₐ[R] B`, if `A` and `B` are algebras over a localization
+`S` of `R`, then `f` is automatically an `S`-algebra homomorphism. -/
+def AlgHom.extendScalarsOfIsLocalization (f : A →ₐ[R] B) : A →ₐ[S] B where
+  __ := f
+  commutes' := by
+    let f := f.comp (IsScalarTower.toAlgHom R S A)
+    let g := IsScalarTower.toAlgHom R S B
+    have : f.toRingHom.comp (algebraMap R S) = g.toRingHom.comp (algebraMap R S) := by simp
+    suffices f = g by rwa [DFunLike.ext_iff] at this
+    apply IsLocalization.algHom_ext M
+    rwa [DFunLike.ext_iff] at this ⊢
+
+@[simp]
+theorem AlgHom.extendScalarsOfIsLocalization_apply (f : A →ₐ[R] B) (a : A) :
+    f.extendScalarsOfIsLocalization S M a = f a :=
+  rfl
+
+/-- For an algebra isomorphism `f : A ≃ₐ[R] B`, if `A` and `B` are algebras over a localization
+`S` of `R`, then `f` is automatically an `S`-algebra isomorphism. -/
+@[simps]
+def AlgEquiv.extendScalarsOfIsLocalization (f : A ≃ₐ[R] B) : A ≃ₐ[S] B where
+  __ := f.toAlgHom.extendScalarsOfIsLocalization S M
+  __ := f
+
+end extend
+
 end Algebra