From c3345c140a9eec04f554c60b0577e27be14a5a68 Mon Sep 17 00:00:00 2001
From: Thomas Browning <tb65536@uw.edu>
Date: Thu, 31 Oct 2024 21:40:17 +0000
Subject: [PATCH] feat(RingTheory/Localization/FractionRing): Lifting
 `AlgEquiv`s to the field of fractions (#17753)

This PR adds some API for lifting `AlgEquiv`s to the field of fractions.
---
 .../RingTheory/Localization/FractionRing.lean | 75 +++++++++++++++++++
 .../WittVector/FrobeniusFractionField.lean    |  2 -
 2 files changed, 75 insertions(+), 2 deletions(-)

diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
index 5ba8201e865fb..a5048ee63fd4a 100644
--- a/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -228,6 +228,81 @@ noncomputable def fieldEquivOfRingEquiv [Algebra B L] [IsFractionRing B L] (h :
         mem_nonZeroDivisors_iff_ne_zero, mem_nonZeroDivisors_iff_ne_zero]
       exact h.symm.map_ne_zero_iff)
 
+@[simp]
+lemma fieldEquivOfRingEquiv_algebraMap [Algebra B L] [IsFractionRing B L] (h : A ≃+* B)
+    (a : A) : fieldEquivOfRingEquiv h (algebraMap A K a) = algebraMap B L (h a) := by
+  simp [fieldEquivOfRingEquiv]
+
+section fieldEquivOfAlgEquiv
+
+variable {A B C D : Type*}
+  [CommRing A] [CommRing B] [CommRing C] [CommRing D]
+  [IsDomain A] [IsDomain B] [IsDomain C] [IsDomain D]
+  [Algebra A B] [Algebra A C] [Algebra A D]
+  (FA FB FC FD : Type*) [Field FA] [Field FB] [Field FC] [Field FD]
+  [Algebra A FA] [Algebra B FB] [Algebra C FC] [Algebra D FD]
+  [IsFractionRing A FA] [IsFractionRing B FB] [IsFractionRing C FC] [IsFractionRing D FD]
+  [Algebra A FB] [IsScalarTower A B FB]
+  [Algebra A FC] [IsScalarTower A C FC]
+  [Algebra A FD] [IsScalarTower A D FD]
+  [Algebra FA FB] [IsScalarTower A FA FB]
+  [Algebra FA FC] [IsScalarTower A FA FC]
+  [Algebra FA FD] [IsScalarTower A FA FD]
+
+/-- An algebra isomorphism of rings induces an algebra isomorphism of fraction fields. -/
+noncomputable def fieldEquivOfAlgEquiv (f : B ≃ₐ[A] C) : FB ≃ₐ[FA] FC where
+  __ := IsFractionRing.fieldEquivOfRingEquiv f.toRingEquiv
+  commutes' x := by
+    obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := A) x
+    simp_rw [map_div₀, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B FB]
+    simp [← IsScalarTower.algebraMap_apply A C FC]
+
+/-- This says that `fieldEquivOfAlgEquiv f` is an extension of `f` (i.e., it agrees with `f` on
+`B`). Whereas `(fieldEquivOfAlgEquiv f).commutes` says that `fieldEquivOfAlgEquiv f` fixes `K`. -/
+@[simp]
+lemma fieldEquivOfAlgEquiv_algebraMap (f : B ≃ₐ[A] C) (b : B) :
+    fieldEquivOfAlgEquiv FA FB FC f (algebraMap B FB b) = algebraMap C FC (f b) :=
+  fieldEquivOfRingEquiv_algebraMap f.toRingEquiv b
+
+variable (A B) in
+@[simp]
+lemma fieldEquivOfAlgEquiv_refl :
+    fieldEquivOfAlgEquiv FA FB FB (AlgEquiv.refl : B ≃ₐ[A] B) = AlgEquiv.refl := by
+  ext x
+  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x
+  simp
+
+lemma fieldEquivOfAlgEquiv_trans (f : B ≃ₐ[A] C) (g : C ≃ₐ[A] D) :
+    fieldEquivOfAlgEquiv FA FB FD (f.trans g) =
+      (fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g) := by
+  ext x
+  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x
+  simp
+
+end fieldEquivOfAlgEquiv
+
+section fieldEquivOfAlgEquivHom
+
+variable {A B : Type*} [CommRing A] [CommRing B] [IsDomain A] [IsDomain B] [Algebra A B]
+  (K L : Type*) [Field K] [Field L]
+  [Algebra A K] [Algebra B L] [IsFractionRing A K] [IsFractionRing B L]
+  [Algebra A L] [IsScalarTower A B L] [Algebra K L] [IsScalarTower A K L]
+
+/-- An algebra automorphism of a ring induces an algebra automorphism of its fraction field.
+
+This is a bundled version of `fieldEquivOfAlgEquiv`. -/
+noncomputable def fieldEquivOfAlgEquivHom : (B ≃ₐ[A] B) →* (L ≃ₐ[K] L) where
+  toFun := fieldEquivOfAlgEquiv K L L
+  map_one' := fieldEquivOfAlgEquiv_refl A B K L
+  map_mul' f g := fieldEquivOfAlgEquiv_trans K L L L g f
+
+@[simp]
+lemma fieldEquivOfAlgEquivHom_apply (f : B ≃ₐ[A] B) :
+    fieldEquivOfAlgEquivHom K L f = fieldEquivOfAlgEquiv K L L f :=
+  rfl
+
+end fieldEquivOfAlgEquivHom
+
 theorem isFractionRing_iff_of_base_ringEquiv (h : R ≃+* P) :
     IsFractionRing R S ↔
       @IsFractionRing P _ S _ ((algebraMap R S).comp h.symm.toRingHom).toAlgebra := by
diff --git a/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean b/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
index 46ee5f96de2b0..d8000a8af9608 100644
--- a/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
+++ b/Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
@@ -242,8 +242,6 @@ theorem exists_frobenius_solution_fractionRing_aux (m n : ℕ) (r' q' : 𝕎 k)
       (IsFractionRing.injective (𝕎 k) (FractionRing (𝕎 k))).ne hq'''
   rw [zpow_sub₀ (FractionRing.p_nonzero p k)]
   field_simp [FractionRing.p_nonzero p k]
-  simp only [IsFractionRing.fieldEquivOfRingEquiv, IsLocalization.ringEquivOfRingEquiv_eq,
-    RingEquiv.coe_ofBijective]
   convert congr_arg (fun x => algebraMap (𝕎 k) (FractionRing (𝕎 k)) x) key using 1
   · simp only [RingHom.map_mul, RingHom.map_pow, map_natCast, frobeniusEquiv_apply]
     ring