feat(IsGaloisGroup): add restrictHom

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -939,6 +939,15 @@ theorem Normal.of_map_subtype {K : Subgroup G} {L : Subgroup K}
     (n : (Subgroup.map K.subtype L).Normal) : L.Normal :=
   n.of_map_injective K.subtype_injective
 
+theorem normal_comap_iff_of_surjective {f : G →* N} (hf : Function.Surjective f) {H : Subgroup N} :
+    (H.comap f).Normal ↔ H.Normal := by
+  rw [← normalizer_eq_top_iff, ← comap_normalizer_eq_of_surjective H hf, ← comap_top f,
+    (comap_injective hf).eq_iff, normalizer_eq_top_iff]
+
+theorem _root_.MulEquiv.normal_map_iff {f : G ≃* G'} {H : Subgroup G} :
+    (H.map (f : G →* G')).Normal ↔ H.Normal := by
+  rw [map_equiv_eq_comap_symm, normal_comap_iff_of_surjective f.symm.surjective]
+
 section SubgroupNormal
 
 @[to_additive]

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,18 @@ 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]
+
+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/IntermediateField/Basic.lean

@@ -541,24 +541,24 @@ theorem coe_fieldRange : ↑f.fieldRange = Set.range f :=
 theorem fieldRange_toSubfield : f.fieldRange.toSubfield = (f : L →+* L').fieldRange :=
   rfl
 
-variable {f}
-
+variable {f} in
 @[simp]
 theorem mem_fieldRange {y : L'} : y ∈ f.fieldRange ↔ ∃ x, f x = y :=
   Iff.rfl
 
-/-- An algebra homomorphism between fields restricts to an algebra equivalence onto its range. -/
+/-- The isomorphism from `L` to the field range of the `AlgHom` `f`, sending `x` to `f x`. -/
+@[simps! apply_coe]
 noncomputable def equivFieldRange : L ≃ₐ[K] f.fieldRange :=
-  AlgEquiv.ofBijective
-    (f.codRestrict f.range fun x ↦ mem_fieldRange.mpr ⟨x, rfl⟩)
-    ⟨fun _ _ h ↦ f.injective (congr_arg Subtype.val h),
-     fun ⟨_, hy⟩ ↦ (mem_fieldRange.mp hy).imp fun _ hx => Subtype.ext hx⟩
-
-@[simp]
-theorem equivFieldRange_apply (x : L) : f.equivFieldRange x = f x := rfl
+  .ofBijective f.rangeRestrict ⟨f.rangeRestrict.injective, fun ⟨_, ⟨x, hx⟩⟩ ↦ ⟨x, Subtype.ext hx⟩⟩
 
 end AlgHom
 
+variable (K L L') in
+@[simp]
+theorem IsScalarTower.toAlgHom_fieldRange [Algebra L L'] [IsScalarTower K L L'] :
+    (IsScalarTower.toAlgHom K L L').fieldRange = Set.range (algebraMap L L') := by
+  ext; simp
+
 namespace IntermediateField
 
 /-- The embedding from an intermediate field of `L / K` to `L`. -/

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

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.Field.Subfield.Basic
 public import Mathlib.Algebra.Order.GroupWithZero.Submonoid
 public import Mathlib.Algebra.Order.Ring.Int
 public import Mathlib.Algebra.Ring.CompTypeclasses
+public import Mathlib.GroupTheory.GroupAction.FixingSubgroup
 public import Mathlib.RingTheory.Localization.Basic
 public import Mathlib.RingTheory.SimpleRing.Basic
 
@@ -437,6 +438,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 +454,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 +649,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]
 
@@ -653,6 +678,28 @@ protected theorem smulCommClass [SMulCommClass G A B] : SMulCommClass G K L :=
       IsScalarTower.algebraMap_apply A B L, smul_mul', smul_div₀',
       ← algebraMap.coe_smul', smul_algebraMap]⟩
 
+variable {A B} in
+/-- If `K` is the fraction field of `A` and `L` is the fraction field of `B` with `A ⊆ B`,
+then for `G` acting on `B` and `L`, the fixing subgroup of `A` in `B` equals the fixing subgroup
+of `K` in `L`. -/
+theorem fixingSubgroup_range_algebraMap :
+    fixingSubgroup G (Set.range (algebraMap A B)) =
+      fixingSubgroup G (Set.range (algebraMap K L)) := by
+  ext g
+  simp only [mem_fixingSubgroup_iff, Set.mem_range]
+  refine ⟨?_, ?_⟩
+  · rintro h _ ⟨x, rfl⟩
+    have {x} : g • (algebraMap A L) x = (algebraMap A L) x := by
+      rw [IsScalarTower.algebraMap_apply A B L, ← algebraMap.smul', h _ ⟨x, rfl⟩]
+    obtain ⟨a, b, _, rfl⟩ := IsFractionRing.div_surjective A x
+    simp only [map_div₀, ← IsScalarTower.algebraMap_apply, smul_div₀', this]
+  · rintro h _ ⟨x, rfl⟩
+    apply FaithfulSMul.algebraMap_injective B L
+    rw [algebraMap.smul']
+    apply h
+    use algebraMap A K x
+    rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply]
+
 end MulAction
 
 end IsFractionRing