refactor(RingTheory/Localization/FractionRing): remove bottom ring and field from IsFractionRing.mulSemiringAction (leanprover-community#40804)

This PR removes the bottom ring and field from `IsFractionRing.mulSemiringAction` since they are unnecessary.

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

Author: tb65536

Mathlib/Algebra/Ring/Action/Group.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.GroupWithZero.Action.Basic
 public import Mathlib.Algebra.Ring.Action.Basic
+public import Mathlib.Algebra.Ring.Aut
 public import Mathlib.Algebra.Ring.Equiv
 
 /-!
@@ -25,7 +26,24 @@ variable (R : Type*) [Semiring R]
 
 /-- Each element of the group defines a semiring isomorphism. -/
 @[simps!]
-def MulSemiringAction.toRingEquiv [MulSemiringAction G R] (x : G) : R ≃+* R :=
-  { DistribMulAction.toAddEquiv R x, MulSemiringAction.toRingHom G R x with }
+def MulSemiringAction.toRingEquiv [MulSemiringAction G R] : G →* (R ≃+* R) where
+  toFun x := { DistribMulAction.toAddEquiv R x, MulSemiringAction.toRingHom G R x with }
+  map_one' := by ext; simp
+  map_mul' x y := by ext; simp [mul_smul]
+
+@[deprecated (since := "2026-06-19")] alias MulSemiringAction.toRingEquiv_apply :=
+MulSemiringAction.toRingEquiv_apply_apply
+
+@[deprecated (since := "2026-06-19")] alias MulSemiringAction.toRingEquiv_symm_apply :=
+MulSemiringAction.toRingEquiv_apply_symm_apply
+
+instance : MulSemiringAction (R ≃+* R) R where
+  smul := (· ·)
+  mul_smul _ _ _ := rfl
+  one_smul _ := rfl
+  smul_zero := map_zero
+  smul_one := map_one
+  smul_add := map_add
+  smul_mul := map_mul
 
 end Semiring

Mathlib/Algebra/Star/UnitaryStarAlgAut.lean

@@ -38,7 +38,7 @@ def conjStarAlgAut : unitary R →* (R ≃⋆ₐ[S] R) where
       dsimp [ConjAct.units_smul_def]
       simp [mul_assoc, ← Unitary.star_eq_inv] }
   map_one' := by ext; simp
-  map_mul' g h := by ext; simp [mul_smul]
+  map_mul' g h := by ext; simp
 
 @[simp] theorem conjStarAlgAut_apply (u : unitary R) (x : R) :
     conjStarAlgAut S R u x = u * x * (star u : R) := rfl

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

@@ -239,21 +239,17 @@ theorem IsGaloisGroup.iff_isFractionRing [Finite G] [IsIntegrallyClosed A] :
 @[deprecated (since := "2026-04-20")] alias FractionRing.mulSemiringAction_of_isGaloisGroup :=
   IsFractionRing.mulSemiringAction
 
-attribute [local instance] FractionRing.liftAlgebra in
 /--
 If `G` is finite and `IsGaloisGroup G A B` with `A` and `B` domains, then `G` is also
 a Galois group for `FractionRing B / FractionRing A` for the action defined by
 `IsFractionRing.mulSemiringAction`.
 -/
-theorem IsGaloisGroup.toFractionRing [IsDomain A] [IsDomain B] [IsTorsionFree A B] [Finite G]
-    [IsGaloisGroup G A B] :
-    letI := IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
+instance IsGaloisGroup.toFractionRing [IsDomain A] [IsDomain B] [IsTorsionFree A B] [Finite G]
+    [IsGaloisGroup G A B] [Algebra (FractionRing A) (FractionRing B)]
+    [IsScalarTower A (FractionRing A) (FractionRing B)] :
+    letI := IsFractionRing.mulSemiringAction G B (FractionRing B)
     IsGaloisGroup G (FractionRing A) (FractionRing B) := by
-  let := IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
-  have : SMulDistribClass G B (FractionRing B) := ⟨fun g b x ↦ by
-    rw [Algebra.smul_def', Algebra.smul_def', smul_mul']
-    congr
-    exact IsFractionRing.fieldEquivOfAlgEquiv_algebraMap (FractionRing A) _ _ _ b⟩
+  let := IsFractionRing.mulSemiringAction G B (FractionRing B)
   apply IsGaloisGroup.to_isFractionRing G A B _ _
 
 open NumberField
@@ -314,7 +310,7 @@ protected theorem finite (R B : Type*) [CommRing R] [CommRing B] [Algebra R B] [
   [IsDomain B] [MulSemiringAction G B] [IsGaloisGroup G R B] : Finite G := by
   let A : Subring B := (algebraMap R B).range
   let := FractionRing.liftAlgebra A (FractionRing B)
-  let := IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
+  let := IsFractionRing.mulSemiringAction G B (FractionRing B)
   let : Algebra R A := (algebraMap R B).rangeRestrict.toAlgebra
   have : IsScalarTower R A B := IsScalarTower.of_algebraMap_eq' rfl
   have : Module.Finite A B := Module.Finite.of_restrictScalars_finite R A B
@@ -331,9 +327,9 @@ theorem card_eq_finrank' (A B : Type*) [CommRing A] [CommRing B] [Algebra A B] [
     Nat.card G = Module.finrank A B := by
   have := IsDomain.of_faithfulSMul A B
   let := FractionRing.liftAlgebra A (FractionRing B)
-  let := IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
+  let := IsFractionRing.mulSemiringAction G B (FractionRing B)
   have : Algebra.IsIntegral A B := IsGaloisGroup.isInvariant.isIntegral A B G
-  rw [(IsGaloisGroup.toFractionRing G A B).card_eq_finrank,
+  rw [IsGaloisGroup.card_eq_finrank G (FractionRing A) (FractionRing B),
     Algebra.IsAlgebraic.finrank_of_isFractionRing A (FractionRing A) B (FractionRing B)]
 
 /-- If `G` is a finite Galois group for `L/K`, then `G` is isomorphic to `Gal(L/K)`. -/
@@ -374,10 +370,8 @@ noncomputable def mulEquivCongr [Finite G] [Finite G'] (A B : Type*) [CommRing A
   haveI : IsDomain A := (FaithfulSMul.algebraMap_injective A B).isDomain
   letI K := FractionRing A
   letI L := FractionRing B
-  letI : MulSemiringAction G L := IsFractionRing.mulSemiringAction G A B K L
-  letI : MulSemiringAction G' L := IsFractionRing.mulSemiringAction G' A B K L
-  haveI : IsGaloisGroup G K L := IsGaloisGroup.toFractionRing G A B
-  haveI : IsGaloisGroup G' K L := IsGaloisGroup.toFractionRing G' A B
+  letI : MulSemiringAction G L := IsFractionRing.mulSemiringAction G B L
+  letI : MulSemiringAction G' L := IsFractionRing.mulSemiringAction G' B L
   mulEquivCongr' G G' K L
 
 attribute [local instance] FractionRing.liftAlgebra in
@@ -389,10 +383,8 @@ theorem mulEquivCongr_apply_smul [Finite G] [Finite G'] (A B : Type*) [CommRing
   haveI : IsDomain A := (FaithfulSMul.algebraMap_injective A B).isDomain
   letI K := FractionRing A
   letI L := FractionRing B
-  letI : MulSemiringAction G L := IsFractionRing.mulSemiringAction G A B K L
-  letI : MulSemiringAction G' L := IsFractionRing.mulSemiringAction G' A B K L
-  haveI : IsGaloisGroup G K L := IsGaloisGroup.toFractionRing G A B
-  haveI : IsGaloisGroup G' K L := IsGaloisGroup.toFractionRing G' A B
+  letI : MulSemiringAction G L := IsFractionRing.mulSemiringAction G B L
+  letI : MulSemiringAction G' L := IsFractionRing.mulSemiringAction G' B L
   apply FaithfulSMul.algebraMap_injective B L
   rw [algebraMap.smul', algebraMap.smul']
   exact mulEquivCongr'_apply_smul G G' K L g _
@@ -576,8 +568,7 @@ theorem fixingSubgroup_range_algebraMap [Finite G] (A B C : Type*) (H : Subgroup
   have : IsDomain A := (FaithfulSMul.algebraMap_injective A C).isDomain
   let K := FractionRing A
   let L := FractionRing C
-  let : MulSemiringAction G L := IsFractionRing.mulSemiringAction G A C K L
-  have : IsGaloisGroup G K L := IsGaloisGroup.toFractionRing G A C
+  let : MulSemiringAction G L := IsFractionRing.mulSemiringAction G C L
   have : IsGaloisGroup H (FractionRing B) L := IsGaloisGroup.toFractionRing H B C
   rw [← fixingSubgroup_range_algebraMap' G K L H (FractionRing B)]
   ext g

Mathlib/NumberTheory/RamificationInertia/Galois.lean

@@ -244,9 +244,9 @@ variable {A B : Type*} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B]
 include G GAC GBC in
 theorem ncard_primesOver_mul_ncard_primesOver :
     (p.primesOver B).ncard * (P.primesOver C).ncard = (p.primesOver C).ncard := by
-  let := IsFractionRing.mulSemiringAction G A B (FractionRing A) (FractionRing B)
-  let := IsFractionRing.mulSemiringAction GAC A C (FractionRing A) (FractionRing C)
-  let := IsFractionRing.mulSemiringAction GBC B C (FractionRing B) (FractionRing C)
+  let := IsFractionRing.mulSemiringAction G B (FractionRing B)
+  let := IsFractionRing.mulSemiringAction GAC C (FractionRing C)
+  let := IsFractionRing.mulSemiringAction GBC C (FractionRing C)
   have : p.ramificationIdxIn C * p.inertiaDegIn C ≠ 0 :=
     mul_ne_zero (ramificationIdxIn_ne_zero GAC) (inertiaDegIn_ne_zero GAC)
   rw [← Nat.mul_left_inj this, ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn p C GAC]

Mathlib/RingTheory/Localization/FractionRing.lean

@@ -437,6 +437,10 @@ lemma ringEquivOfRingEquiv_algebraMap
     (a : A) : ringEquivOfRingEquiv h (algebraMap A K a) = algebraMap B L (h a) := by
   simp
 
+@[simp]
+lemma ringEquivOfRingEquiv_refl :
+    ringEquivOfRingEquiv (.refl A) = .refl K := by ext; simp
+
 @[simp]
 lemma ringEquivOfRingEquiv_symm :
     (ringEquivOfRingEquiv h : K ≃+* L).symm = ringEquivOfRingEquiv h.symm := rfl
@@ -449,6 +453,26 @@ theorem ringEquivOfRingEquiv_comp {C : Type*} (M : Type*) [CommRing C]
   ext a
   simp [IsLocalization.map_map]
 
+variable (A K)
+
+/-- A ring automorphism of a ring induces an ring automorphism of its fraction field.
+
+This is a bundled version of `ringEquivOfRingEquiv`. -/
+noncomputable def ringEquivOfRingEquivHom : (A ≃+* A) →* (K ≃+* K) where
+  toFun := ringEquivOfRingEquiv
+  map_one' := ringEquivOfRingEquiv_refl
+  map_mul' f g := ringEquivOfRingEquiv_comp K K K g f
+
+@[simp]
+lemma ringEquivOfRingEquivHom_apply (f : A ≃+* A) :
+    ringEquivOfRingEquivHom A K f = ringEquivOfRingEquiv f :=
+  rfl
+
+lemma ringEquivOfRingEquivHom_injective : Function.Injective (ringEquivOfRingEquivHom A K) := by
+  intro f g h
+  ext b
+  simpa using RingEquiv.ext_iff.mp h (algebraMap A K b)
+
 end ringEquivOfRingEquiv
 
 section semilinearEquivOfRingEquiv
@@ -624,21 +648,21 @@ variable (G A B K L : Type*) [Group G] [CommRing A] [CommRing B] [MulSemiringAct
 /-- Given a `MulSemiringAction G B`, extend the action of `G` on `B` to a `MulSemiringAction G L`
 on the fraction field `L` of `B`. -/
 @[implicit_reducible]
-noncomputable def mulSemiringAction [SMulCommClass G A B] :
+noncomputable def mulSemiringAction :
     MulSemiringAction G L :=
   MulSemiringAction.compHom L
-    ((fieldEquivOfAlgEquivHom K L).comp (MulSemiringAction.toAlgAut G A B))
+    ((ringEquivOfRingEquivHom B L).comp (MulSemiringAction.toRingEquiv G B))
 
 /-- The action of `G` on the fraction field `L` of `B` given by `IsFractionRing.mulSemiringAction`
 is compatible with the embedding `B ⊆ L`. -/
-instance smulDistribClass [SMulCommClass G A B] :
-    letI := mulSemiringAction G A B K L
+instance smulDistribClass :
+    letI := mulSemiringAction G B L
     SMulDistribClass G B L :=
-  let := mulSemiringAction G A B K L
+  let := mulSemiringAction G B L
   ⟨fun g b x ↦ by
     rw [Algebra.smul_def', Algebra.smul_def', smul_mul']
     congr
-    apply fieldEquivOfAlgEquiv_algebraMap⟩
+    apply ringEquivOfRingEquiv_algebraMap⟩
 
 variable [MulSemiringAction G L] [SMulDistribClass G B L]