refactor(GroupTheory/GroupAction/Basic): re-organise, rename, and make some variables implicit (#7786)

- Re-organise the namespace and section structure of GroupTheory/GroupAction/Basic.lean.
- Remove the namespaces `MulAction.Stabilizer` and `AddAction.Stabilizer`, renaming `MulAction.Stabilizer.submonoid` to `MulAction.stabilizerSubmonoid`.
- Make variables for the monoid/group/set implicit when an element or subset is used in the statement.

Author: wupr

Mathlib/CategoryTheory/Action.lean

@@ -113,12 +113,12 @@ variable {X} (x : X)
 
 /-- The stabilizer of a point is isomorphic to the endomorphism monoid at the
   corresponding point. In fact they are definitionally equivalent. -/
-def stabilizerIsoEnd : Stabilizer.submonoid M x ≃* @End (ActionCategory M X) _ x :=
+def stabilizerIsoEnd : stabilizerSubmonoid M x ≃* @End (ActionCategory M X) _ x :=
   MulEquiv.refl _
 #align category_theory.action_category.stabilizer_iso_End CategoryTheory.ActionCategory.stabilizerIsoEnd
 
 @[simp]
-theorem stabilizerIsoEnd_apply (f : Stabilizer.submonoid M x) :
+theorem stabilizerIsoEnd_apply (f : stabilizerSubmonoid M x) :
     (stabilizerIsoEnd M x) f = f :=
   rfl
 #align category_theory.action_category.stabilizer_iso_End_apply CategoryTheory.ActionCategory.stabilizerIsoEnd_apply

Mathlib/FieldTheory/Fixed.lean

@@ -45,7 +45,7 @@ variable (F : Type v) [Field F] [MulSemiringAction M F] [MulSemiringAction G F]
 
 /-- The subfield of F fixed by the field endomorphism `m`. -/
 def FixedBy.subfield : Subfield F where
-  carrier := fixedBy M F m
+  carrier := fixedBy F m
   zero_mem' := smul_zero m
   add_mem' hx hy := (smul_add m _ _).trans <| congr_arg₂ _ hx hy
   neg_mem' hx := (smul_neg m _).trans <| congr_arg _ hx

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -37,7 +37,11 @@ open Function
 
 namespace MulAction
 
-variable (M : Type u) {α : Type v} [Monoid M] [MulAction M α]
+variable (M : Type u) [Monoid M] (α : Type v) [MulAction M α]
+
+section Orbit
+
+variable {α}
 
 /-- The orbit of an element under an action. -/
 @[to_additive "The orbit of an element under an action."]
@@ -55,8 +59,8 @@ theorem mem_orbit_iff {a₁ a₂ : α} : a₂ ∈ orbit M a₁ ↔ ∃ x : M, x
 #align add_action.mem_orbit_iff AddAction.mem_orbit_iff
 
 @[to_additive (attr := simp)]
-theorem mem_orbit (a : α) (x : M) : x • a ∈ orbit M a :=
-  ⟨x, rfl⟩
+theorem mem_orbit (a : α) (m : M) : m • a ∈ orbit M a :=
+  ⟨m, rfl⟩
 #align mul_action.mem_orbit MulAction.mem_orbit
 #align add_action.mem_orbit AddAction.mem_orbit
 
@@ -102,7 +106,17 @@ theorem orbit.coe_smul {a : α} {m : M} {a' : orbit M a} : ↑(m • a') = m •
 #align mul_action.orbit.coe_smul MulAction.orbit.coe_smul
 #align add_action.orbit.coe_vadd AddAction.orbit.coe_vadd
 
-variable (M) (α)
+variable (M)
+
+@[to_additive]
+theorem orbit_eq_univ [IsPretransitive M α] (a : α) : orbit M a = Set.univ :=
+  (surjective_smul M a).range_eq
+#align mul_action.orbit_eq_univ MulAction.orbit_eq_univ
+#align add_action.orbit_eq_univ AddAction.orbit_eq_univ
+
+end Orbit
+
+section FixedPoints
 
 /-- The set of elements fixed under the whole action. -/
 @[to_additive "The set of elements fixed under the whole action."]
@@ -111,21 +125,25 @@ def fixedPoints : Set α :=
 #align mul_action.fixed_points MulAction.fixedPoints
 #align add_action.fixed_points AddAction.fixedPoints
 
+variable {M}
+
 /-- `fixedBy m` is the set of elements fixed by `m`. -/
 @[to_additive "`fixedBy m` is the set of elements fixed by `m`."]
 def fixedBy (m : M) : Set α :=
   { x | m • x = x }
 #align mul_action.fixed_by MulAction.fixedBy
 #align add_action.fixed_by AddAction.fixedBy
 
+variable (M)
+
 @[to_additive]
-theorem fixed_eq_iInter_fixedBy : fixedPoints M α = ⋂ m : M, fixedBy M α m :=
+theorem fixed_eq_iInter_fixedBy : fixedPoints M α = ⋂ m : M, fixedBy α m :=
   Set.ext fun _ =>
     ⟨fun hx => Set.mem_iInter.2 fun m => hx m, fun hx m => (Set.mem_iInter.1 hx m : _)⟩
 #align mul_action.fixed_eq_Inter_fixed_by MulAction.fixed_eq_iInter_fixedBy
 #align add_action.fixed_eq_Inter_fixed_by AddAction.fixed_eq_iInter_fixedBy
 
-variable {M}
+variable {M α}
 
 @[to_additive (attr := simp)]
 theorem mem_fixedPoints {a : α} : a ∈ fixedPoints M α ↔ ∀ m : M, m • a = a :=
@@ -134,7 +152,7 @@ theorem mem_fixedPoints {a : α} : a ∈ fixedPoints M α ↔ ∀ m : M, m • a
 #align add_action.mem_fixed_points AddAction.mem_fixedPoints
 
 @[to_additive (attr := simp)]
-theorem mem_fixedBy {m : M} {a : α} : a ∈ fixedBy M α m ↔ m • a = a :=
+theorem mem_fixedBy {m : M} {a : α} : a ∈ fixedBy α m ↔ m • a = a :=
   Iff.rfl
 #align mul_action.mem_fixed_by MulAction.mem_fixedBy
 #align add_action.mem_fixed_by AddAction.mem_fixedBy
@@ -148,36 +166,6 @@ theorem mem_fixedPoints' {a : α} : a ∈ fixedPoints M α ↔ ∀ a', a' ∈ or
 #align mul_action.mem_fixed_points' MulAction.mem_fixedPoints'
 #align add_action.mem_fixed_points' AddAction.mem_fixedPoints'
 
-variable (M) {α}
-
-/-- The stabilizer of a point `a` as a submonoid of `M`. -/
-@[to_additive "The stabilizer of m point `a` as an additive submonoid of `M`."]
-def Stabilizer.submonoid (a : α) : Submonoid M where
-  carrier := { m | m • a = a }
-  one_mem' := one_smul _ a
-  mul_mem' {m m'} (ha : m • a = a) (hb : m' • a = a) :=
-    show (m * m') • a = a by rw [← smul_smul, hb, ha]
-#align mul_action.stabilizer.submonoid MulAction.Stabilizer.submonoid
-#align add_action.stabilizer.add_submonoid AddAction.Stabilizer.addSubmonoid
-
-@[to_additive (attr := simp)]
-theorem mem_stabilizer_submonoid_iff {a : α} {m : M} : m ∈ Stabilizer.submonoid M a ↔ m • a = a :=
-  Iff.rfl
-#align mul_action.mem_stabilizer_submonoid_iff MulAction.mem_stabilizer_submonoid_iff
-#align add_action.mem_stabilizer_add_submonoid_iff AddAction.mem_stabilizer_addSubmonoid_iff
-
-@[to_additive]
-instance [DecidableEq α] (a : α) : DecidablePred (· ∈ Stabilizer.submonoid M a) :=
-  fun _ => inferInstanceAs <| Decidable (_ = _)
-
-@[to_additive]
-theorem orbit_eq_univ [IsPretransitive M α] (a : α) : orbit M a = Set.univ :=
-  (surjective_smul M a).range_eq
-#align mul_action.orbit_eq_univ MulAction.orbit_eq_univ
-#align add_action.orbit_eq_univ AddAction.orbit_eq_univ
-
-variable {M}
-
 @[to_additive mem_fixedPoints_iff_card_orbit_eq_one]
 theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] :
     a ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1 := by
@@ -192,34 +180,56 @@ theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] :
 #align mul_action.mem_fixed_points_iff_card_orbit_eq_one MulAction.mem_fixedPoints_iff_card_orbit_eq_one
 #align add_action.mem_fixed_points_iff_card_orbit_eq_zero AddAction.mem_fixedPoints_iff_card_orbit_eq_one
 
-end MulAction
+end FixedPoints
 
-namespace MulAction
+section Stabilizers
 
-variable (G : Type u) {α : Type v} [Group G] [MulAction G α]
+variable {α}
 
-/-- The stabilizer of an element under an action, i.e. what sends the element to itself.
-A subgroup. -/
-@[to_additive
-      "The stabilizer of an element under an action, i.e. what sends the element to itself.
-      An additive subgroup."]
-def stabilizer (a : α) : Subgroup G :=
-  { Stabilizer.submonoid G a with
-    inv_mem' := fun {m} (ha : m • a = a) => show m⁻¹ • a = a by rw [inv_smul_eq_iff, ha] }
-#align mul_action.stabilizer MulAction.stabilizer
-#align add_action.stabilizer AddAction.stabilizer
+/-- The stabilizer of a point `a` as a submonoid of `M`. -/
+@[to_additive "The stabilizer of a point `a` as an additive submonoid of `M`."]
+def stabilizerSubmonoid (a : α) : Submonoid M where
+  carrier := { m | m • a = a }
+  one_mem' := one_smul _ a
+  mul_mem' {m m'} (ha : m • a = a) (hb : m' • a = a) :=
+    show (m * m') • a = a by rw [← smul_smul, hb, ha]
+#align mul_action.stabilizer.submonoid MulAction.stabilizerSubmonoid
+#align add_action.stabilizer.add_submonoid AddAction.stabilizerAddSubmonoid
 
-variable {G}
+variable {M}
+
+@[to_additive]
+instance [DecidableEq α] (a : α) : DecidablePred (· ∈ stabilizerSubmonoid M a) :=
+  fun _ => inferInstanceAs <| Decidable (_ = _)
 
 @[to_additive (attr := simp)]
-theorem mem_stabilizer_iff {g : G} {a : α} : g ∈ stabilizer G a ↔ g • a = a :=
+theorem mem_stabilizerSubmonoid_iff {a : α} {m : M} : m ∈ stabilizerSubmonoid M a ↔ m • a = a :=
   Iff.rfl
-#align mul_action.mem_stabilizer_iff MulAction.mem_stabilizer_iff
-#align add_action.mem_stabilizer_iff AddAction.mem_stabilizer_iff
+#align mul_action.mem_stabilizer_submonoid_iff MulAction.mem_stabilizerSubmonoid_iff
+#align add_action.mem_stabilizer_add_submonoid_iff AddAction.mem_stabilizerAddSubmonoid_iff
 
-@[to_additive]
-instance [DecidableEq α] (a : α) : DecidablePred (· ∈ stabilizer G a) :=
-  fun _ => inferInstanceAs <| Decidable (_ = _)
+end Stabilizers
+
+end MulAction
+
+/-- `smul` by a `k : M` over a ring is injective, if `k` is not a zero divisor.
+The general theory of such `k` is elaborated by `IsSMulRegular`.
+The typeclass that restricts all terms of `M` to have this property is `NoZeroSMulDivisors`. -/
+theorem smul_cancel_of_non_zero_divisor {M R : Type*} [Monoid M] [NonUnitalNonAssocRing R]
+    [DistribMulAction M R] (k : M) (h : ∀ x : R, k • x = 0 → x = 0) {a b : R} (h' : k • a = k • b) :
+    a = b := by
+  rw [← sub_eq_zero]
+  refine' h _ _
+  rw [smul_sub, h', sub_self]
+#align smul_cancel_of_non_zero_divisor smul_cancel_of_non_zero_divisor
+
+namespace MulAction
+
+variable (G : Type u) [Group G] (α : Type v) [MulAction G α]
+
+section Orbit
+
+variable {G α}
 
 @[to_additive (attr := simp)]
 theorem smul_orbit (g : G) (a : α) : g • orbit G a = orbit G a :=
@@ -254,8 +264,6 @@ theorem orbit_eq_iff {a b : α} : orbit G a = orbit G b ↔ a ∈ orbit G b :=
 #align mul_action.orbit_eq_iff MulAction.orbit_eq_iff
 #align add_action.orbit_eq_iff AddAction.orbit_eq_iff
 
-variable (G)
-
 @[to_additive]
 theorem mem_orbit_smul (g : G) (a : α) : a ∈ orbit G (g • a) := by
   simp only [orbit_smul, mem_orbit_self]
@@ -268,7 +276,7 @@ theorem smul_mem_orbit_smul (g h : G) (a : α) : g • a ∈ orbit G (h • a) :
 #align mul_action.smul_mem_orbit_smul MulAction.smul_mem_orbit_smul
 #align add_action.vadd_mem_orbit_vadd AddAction.vadd_mem_orbit_vadd
 
-variable (α)
+variable (G α)
 
 /-- The relation 'in the same orbit'. -/
 @[to_additive "The relation 'in the same orbit'."]
@@ -420,7 +428,34 @@ def selfEquivSigmaOrbits : α ≃ Σω : Ω, orbit G ω.out' :=
 #align mul_action.self_equiv_sigma_orbits MulAction.selfEquivSigmaOrbits
 #align add_action.self_equiv_sigma_orbits AddAction.selfEquivSigmaOrbits
 
-variable {G α}
+end Orbit
+
+section Stabilizer
+
+variable {α}
+
+/-- The stabilizer of an element under an action, i.e. what sends the element to itself.
+A subgroup. -/
+@[to_additive
+      "The stabilizer of an element under an action, i.e. what sends the element to itself.
+      An additive subgroup."]
+def stabilizer (a : α) : Subgroup G :=
+  { stabilizerSubmonoid G a with
+    inv_mem' := fun {m} (ha : m • a = a) => show m⁻¹ • a = a by rw [inv_smul_eq_iff, ha] }
+#align mul_action.stabilizer MulAction.stabilizer
+#align add_action.stabilizer AddAction.stabilizer
+
+variable {G}
+
+@[to_additive]
+instance [DecidableEq α] (a : α) : DecidablePred (· ∈ stabilizer G a) :=
+  fun _ => inferInstanceAs <| Decidable (_ = _)
+
+@[to_additive (attr := simp)]
+theorem mem_stabilizer_iff {a : α} {g : G} : g ∈ stabilizer G a ↔ g • a = a :=
+  Iff.rfl
+#align mul_action.mem_stabilizer_iff MulAction.mem_stabilizer_iff
+#align add_action.mem_stabilizer_iff AddAction.mem_stabilizer_iff
 
 /-- If the stabilizer of `a` is `S`, then the stabilizer of `g • a` is `gSg⁻¹`. -/
 theorem stabilizer_smul_eq_stabilizer_map_conj (g : G) (a : α) :
@@ -440,11 +475,13 @@ noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : (orbitRel
   (MulEquiv.subgroupCongr this).trans ((MulAut.conj g).subgroupMap <| stabilizer G b).symm
 #align mul_action.stabilizer_equiv_stabilizer_of_orbit_rel MulAction.stabilizerEquivStabilizerOfOrbitRel
 
+end Stabilizer
+
 end MulAction
 
 namespace AddAction
 
-variable (G : Type u) (α : Type v) [AddGroup G] [AddAction G α]
+variable (G : Type u) [AddGroup G] (α : Type v) [AddAction G α]
 
 /-- If the stabilizer of `x` is `S`, then the stabilizer of `g +ᵥ x` is `g + S + (-g)`. -/
 theorem stabilizer_vadd_eq_stabilizer_map_conj (g : G) (a : α) :
@@ -466,14 +503,3 @@ noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : (orbitRel
 #align add_action.stabilizer_equiv_stabilizer_of_orbit_rel AddAction.stabilizerEquivStabilizerOfOrbitRel
 
 end AddAction
-
-/-- `smul` by a `k : M` over a ring is injective, if `k` is not a zero divisor.
-The general theory of such `k` is elaborated by `IsSMulRegular`.
-The typeclass that restricts all terms of `M` to have this property is `NoZeroSMulDivisors`. -/
-theorem smul_cancel_of_non_zero_divisor {M R : Type*} [Monoid M] [NonUnitalNonAssocRing R]
-    [DistribMulAction M R] (k : M) (h : ∀ x : R, k • x = 0 → x = 0) {a b : R} (h' : k • a = k • b) :
-    a = b := by
-  rw [← sub_eq_zero]
-  refine' h _ _
-  rw [smul_sub, h', sub_self]
-#align smul_cancel_of_non_zero_divisor smul_cancel_of_non_zero_divisor

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -307,9 +307,9 @@ theorem card_eq_sum_card_group_div_card_stabilizer [Fintype α] [Fintype β] [Fi
       "**Burnside's lemma** : a (noncomputable) bijection between the disjoint union of all
       `{x ∈ X | g • x = x}` for `g ∈ G` and the product `G × X/G`, where `G` is an additive group
       acting on `X` and `X/G`denotes the quotient of `X` by the relation `orbitRel G X`. "]
-noncomputable def sigmaFixedByEquivOrbitsProdGroup : (Σa : α, fixedBy α β a) ≃ Ω × α :=
+noncomputable def sigmaFixedByEquivOrbitsProdGroup : (Σa : α, fixedBy β a) ≃ Ω × α :=
   calc
-    (Σa : α, fixedBy α β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
+    (Σa : α, fixedBy β a) ≃ { ab : α × β // ab.1 • ab.2 = ab.2 } :=
       (Equiv.subtypeProdEquivSigmaSubtype _).symm
     _ ≃ { ba : β × α // ba.2 • ba.1 = ba.1 } := (Equiv.prodComm α β).subtypeEquiv fun _ => Iff.rfl
     _ ≃ Σb : β, stabilizer α b :=
@@ -333,8 +333,8 @@ elements fixed by each `g ∈ G` is the number of orbits. -/
 @[to_additive
       "**Burnside's lemma** : given a finite additive group `G` acting on a set `X`,
       the average number of elements fixed by each `g ∈ G` is the number of orbits. "]
-theorem sum_card_fixedBy_eq_card_orbits_mul_card_group [Fintype α] [∀ a, Fintype <| fixedBy α β a]
-    [Fintype Ω] : (∑ a : α, Fintype.card (fixedBy α β a)) = Fintype.card Ω * Fintype.card α := by
+theorem sum_card_fixedBy_eq_card_orbits_mul_card_group [Fintype α] [∀ a : α, Fintype <| fixedBy β a]
+    [Fintype Ω] : (∑ a : α, Fintype.card (fixedBy β a)) = Fintype.card Ω * Fintype.card α := by
   rw [← Fintype.card_prod, ← Fintype.card_sigma,
     Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]
 #align mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group
@@ -426,7 +426,7 @@ theorem card_comm_eq_card_conjClasses_mul_card (G : Type*) [Group G] :
   -- Porting note: Changed `calc` proof into a `rw` proof.
   rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype Commute), card_sigma,
     sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // Commute a b })
-      (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g))
+      (fun g ↦ card (MulAction.fixedBy G g))
       fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
     MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group]
   congr 1; apply card_congr'; congr; ext;

Mathlib/GroupTheory/GroupAction/SubMulAction.lean

@@ -331,9 +331,9 @@ lemma orbit_of_sub_mul {p : SubMulAction R M} (m : p) :
 -/
 /-- Stabilizers in monoid SubMulAction coincide with stabilizers in the ambient space -/
 theorem stabilizer_of_subMul.submonoid {p : SubMulAction R M} (m : p) :
-    MulAction.Stabilizer.submonoid R m = MulAction.Stabilizer.submonoid R (m : M) := by
+    MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R (m : M) := by
   ext
-  simp only [MulAction.mem_stabilizer_submonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]
+  simp only [MulAction.mem_stabilizerSubmonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]
 #align sub_mul_action.stabilizer_of_sub_mul.submonoid SubMulAction.stabilizer_of_subMul.submonoid
 
 end MulActionMonoid

Mathlib/GroupTheory/PGroup.lean

@@ -198,7 +198,7 @@ theorem card_modEq_card_fixedPoints [Fintype (fixedPoints G α)] :
       Eq.symm
         (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
           (fun a₁ a₂ _ _ _ _ h =>
-            Subtype.eq ((mem_fixedPoints' α).mp a₂.2 a₁.1 (Quotient.exact' h)))
+            Subtype.eq (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
           (fun b => Quotient.inductionOn' b fun b _ hb => _) fun a ha _ => by
           rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
     obtain ⟨k, hk⟩ := hG.card_orbit b

Mathlib/GroupTheory/Sylow.lean

@@ -503,7 +503,7 @@ namespace Sylow
 theorem mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {H : Subgroup G} [Finite (H : Set G)]
     {x : G} : (x : G ⧸ H) ∈ MulAction.fixedPoints H (G ⧸ H) ↔ x ∈ normalizer H :=
   ⟨fun hx =>
-    have ha : ∀ {y : G ⧸ H}, y ∈ orbit H (x : G ⧸ H) → y = x := (mem_fixedPoints' _).1 hx _
+    have ha : ∀ {y : G ⧸ H}, y ∈ orbit H (x : G ⧸ H) → y = x := mem_fixedPoints'.1 hx _
     (inv_mem_iff (G := G)).1
       (mem_normalizer_fintype fun n (hn : n ∈ H) =>
         have : (n⁻¹ * x)⁻¹ * x ∈ H := QuotientGroup.eq.1 (ha ⟨⟨n⁻¹, inv_mem hn⟩, rfl⟩)
@@ -512,7 +512,7 @@ theorem mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {H : Subgroup G} [Fin
           convert this
           rw [inv_inv]),
     fun hx : ∀ n : G, n ∈ H ↔ x * n * x⁻¹ ∈ H =>
-    (mem_fixedPoints' _).2 fun y =>
+    mem_fixedPoints'.2 fun y =>
       Quotient.inductionOn' y fun y hy =>
         QuotientGroup.eq.2
           (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy