feat(FieldTheory/Galois/IsGaloisGroup): IsGaloisGroup instance for FixedPoints.subalgebra (leanprover-community#39095)

This PR generalizes the existing `IsGaloisGroup` instance for `FixedPoints.intermediateField` to `FixedPoints.subalgebra`.

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

Author: tb65536

Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

@@ -91,14 +91,23 @@ def FixedPoints.subsemiring : Subsemiring B' where
   __ := FixedPoints.addSubmonoid G B'
   __ := FixedPoints.submonoid G B'
 
+instance : SMulCommClass G (FixedPoints.subsemiring B' G) B' :=
+  inferInstanceAs (SMulCommClass G (FixedPoints.submonoid G B') B')
+
 /-- The set of fixed points under a group action, as a subring. -/
 def FixedPoints.subring : Subring B where
   __ := FixedPoints.addSubgroup G B
   __ := FixedPoints.submonoid G B
 
+instance : SMulCommClass G (FixedPoints.subring B G) B :=
+  inferInstanceAs (SMulCommClass G (FixedPoints.subsemiring B G) B)
+
 /-- The set of fixed points under a group action, as a subalgebra. -/
 def FixedPoints.subalgebra : Subalgebra A B' where
   __ := FixedPoints.subsemiring B' G
   algebraMap_mem' r g := smul_algebraMap g r
 
+instance : SMulCommClass G (FixedPoints.subalgebra A B' G) B' :=
+  inferInstanceAs (SMulCommClass G (FixedPoints.subsemiring B' G) B')
+
 end MulSemiringAction

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

@@ -270,12 +270,17 @@ theorem map_mulEquivAlgEquiv_fixingSubgroup
 
 variable (H H' : Subgroup G) (F F' : IntermediateField K L)
 
-instance subgroup [hGKL : IsGaloisGroup G K L] :
-    IsGaloisGroup H (FixedPoints.intermediateField H : IntermediateField K L) L where
+instance (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
+    [MulSemiringAction G S] [hGKL : IsGaloisGroup G R S] :
+    IsGaloisGroup H (FixedPoints.subalgebra R S H) S where
   faithful := have := hGKL.faithful; inferInstance
-  commutes := inferInstanceAs <| SMulCommClass H (FixedPoints.subfield H L) L
+  commutes := inferInstance
   isInvariant := ⟨fun x h ↦ ⟨⟨x, h⟩, rfl⟩⟩
 
+instance subgroup [hGKL : IsGaloisGroup G K L] :
+    IsGaloisGroup H (FixedPoints.intermediateField H : IntermediateField K L) L :=
+  inferInstanceAs (IsGaloisGroup H (FixedPoints.subalgebra K L H) L)
+
 open IntermediateField in
 theorem fixedPoints_of_isGaloisGroup [hGKL : IsGaloisGroup G K L] [hHFL : IsGaloisGroup H F L] :
     FixedPoints.intermediateField H = F := by

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -190,6 +190,9 @@ def FixedPoints.submonoid : Submonoid α where
 lemma FixedPoints.mem_submonoid (a : α) : a ∈ submonoid M α ↔ ∀ m : M, m • a = a :=
   Iff.rfl
 
+instance : SMulCommClass M (FixedPoints.submonoid M α) α where
+  smul_comm g x y := by simp_rw [Submonoid.smul_def, smul_eq_mul, smul_mul', x.2 g]
+
 end Monoid
 
 section Group
@@ -208,6 +211,9 @@ scoped notation α "^*" M:51 => FixedPoints.subgroup M α
 lemma mem_subgroup (a : α) : a ∈ α^*M ↔ ∀ m : M, m • a = a :=
   Iff.rfl
 
+instance : SMulCommClass M (FixedPoints.subgroup M α) α :=
+  inferInstanceAs (SMulCommClass M (FixedPoints.submonoid M α) α)
+
 @[simp]
 lemma subgroup_toSubmonoid : (α^*M).toSubmonoid = submonoid M α :=
   rfl