feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. (leanprover-community#33082)

This is  preparatory material for the conclusion of the story of the proof of simplicity of the alternating group using the Iwasawa criterion which is leanprover-community#36524.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: AntoineChambert-Loir

Mathlib/GroupTheory/GroupAction/ConjAct.lean

@@ -168,6 +168,13 @@ end Units
 
 variable [Group G]
 
+theorem coe_smul {G : Type*} [Group G] {H : Subgroup G} (g h : H) :
+    (ConjAct.toConjAct g • h).1 = ConjAct.toConjAct g.1 • h.1 := by
+  rfl
+
+theorem toConjAct_inv_smul (g h : G) : toConjAct g⁻¹ • h = g⁻¹ * h * g := by
+  rw [toConjAct_smul, inv_inv]
+
 -- todo: this file is not in good order; I will refactor this after the PR
 
 instance : MulDistribMulAction (ConjAct G) G where
@@ -188,6 +195,9 @@ instance smulCommClass' [SMul α G] [SMulCommClass G α G] [IsScalarTower α G G
 theorem smul_eq_mulAut_conj (g : ConjAct G) (h : G) : g • h = MulAut.conj (ofConjAct g) h :=
   rfl
 
+theorem toConjAct_smul_eq_mulAut_conj (g h : G) : ConjAct.toConjAct g • h = MulAut.conj g h :=
+  rfl
+
 /-- The set of fixed points of the conjugation action of `G` on itself is the center of `G`. -/
 theorem fixedPoints_eq_center : fixedPoints (ConjAct G) G = center G := by
   ext x

Mathlib/GroupTheory/Perm/ConjAct.lean

@@ -39,6 +39,11 @@ theorem mem_conj_support (k : ConjAct (Perm α)) (g : Perm α) (a : α) :
     Function.comp_apply, ConjAct.ofConjAct_inv]
   apply Equiv.apply_eq_iff_eq_symm_apply
 
+theorem support_conj_eq_smul_support (k : ConjAct (Perm α)) (g : Equiv.Perm α) :
+    (k • g).support = k.ofConjAct • g.support := by
+  ext
+  rw [mem_conj_support, ← Perm.smul_def, ConjAct.ofConjAct_inv, Finset.inv_smul_mem_iff]
+
 theorem cycleFactorsFinset_conj (g k : Perm α) :
     (ConjAct.toConjAct k • g).cycleFactorsFinset =
       Finset.map (MulAut.conj k).toEquiv.toEmbedding g.cycleFactorsFinset := by
@@ -65,4 +70,13 @@ theorem cycleFactorsFinset_conj_eq
   simp only [inv_smul_smul]
   exact Finset.inv_smul_mem_iff
 
+omit [Fintype α] in
+theorem conj_smul_range_ofSubtype [Finite α] (g : Perm α) (s : Finset α) :
+    ConjAct.toConjAct g • (ofSubtype (p := (· ∈ s))).range =
+      (ofSubtype (p := (· ∈ g • s))).range := by
+  have : Fintype α := Fintype.ofFinite α
+  ext k
+  simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, mem_range_ofSubtype_iff]
+  simp [support_conj_eq_smul_support, Set.subset_smul_set_iff]
+
 end Equiv.Perm

Mathlib/GroupTheory/Perm/Finite.lean

@@ -290,6 +290,18 @@ lemma disjoint_closure_of_disjoint_support {S T : Set (Perm α)}
   apply disjoint_support_closure_of_disjoint_support
   exact h
 
+theorem mem_range_ofSubtype_iff {p : α → Prop} [DecidablePred p] {g : Perm α} :
+    g ∈ (ofSubtype : Perm (Subtype p) →* Perm α).range ↔ (g.support : Set α) ⊆ setOf p := by
+  constructor
+  · rintro ⟨k, rfl⟩ x
+    simp only [Finset.mem_coe, mem_support_ofSubtype, Set.mem_setOf_eq]
+    exact fun ⟨hx, _⟩ ↦ hx
+  · intro hg
+    refine ⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩
+    by_cases hx : g x = x
+    · rw [hx]
+    · refine iff_of_true (hg ?_) (hg ?_) <;> simpa
+
 end Fintype
 
 end Equiv.Perm

Mathlib/GroupTheory/Perm/Sign.lean

@@ -579,8 +579,8 @@ theorem sign_extendDomain (e : Perm α) {p : β → Prop} [DecidablePred p] (f :
   simp only [Equiv.Perm.extendDomain, sign_subtypeCongr, sign_permCongr, sign_refl, mul_one]
 
 @[simp]
-theorem sign_ofSubtype {p : α → Prop} [DecidablePred p] (f : Equiv.Perm (Subtype p)) :
-    sign (ofSubtype f) = sign f :=
+theorem sign_ofSubtype {p : α → Prop} [DecidablePred p] [Fintype (Subtype p)]
+    (f : Equiv.Perm (Subtype p)) : sign (ofSubtype f) = sign f :=
   sign_extendDomain f (Equiv.refl (Subtype p))
 
 end congr

Mathlib/GroupTheory/Perm/Support.lean

@@ -365,6 +365,10 @@ theorem support_ofSubtype {p : α → Prop} [DecidablePred p] (u : Perm (Subtype
   · simp only [forall_prop_of_true hx, ofSubtype_apply_of_mem u hx, ← Subtype.coe_inj]
   · simp only [forall_prop_of_false hx, ofSubtype_apply_of_not_mem u hx]
 
+theorem mem_support_ofSubtype {p : α → Prop} [DecidablePred p] (x : α) (u : Perm (Subtype p)) :
+    x ∈ (ofSubtype u).support ↔ ∃ (hx : p x), ⟨x, hx⟩ ∈ u.support := by
+  simp [support_ofSubtype]
+
 theorem mem_support_of_mem_noncommProd_support {α β : Type*} [DecidableEq β] [Fintype β]
     {s : Finset α} {f : α → Perm β}
     {comm : (s : Set α).Pairwise (Commute on f)} {x : β} (hx : x ∈ (s.noncommProd f comm).support) :

Mathlib/GroupTheory/SpecificGroups/Alternating.lean

@@ -5,12 +5,11 @@ Authors: Aaron Anderson, Antoine Chambert-Loir
 -/
 module
 
-public import Mathlib.Algebra.Ring.CharZero
 public import Mathlib.Data.Fintype.Units
 public import Mathlib.GroupTheory.IndexNormal
+public import Mathlib.GroupTheory.Perm.ConjAct
 public import Mathlib.GroupTheory.Perm.Fin
 public import Mathlib.GroupTheory.Subgroup.Simple
-public import Mathlib.Logic.Equiv.Fin.Rotate
 public import Mathlib.Tactic.IntervalCases
 
 /-!
@@ -205,8 +204,19 @@ theorem closure_three_cycles_eq_alternating :
     rw [List.prod_cons, List.prod_cons, ← mul_assoc]
     apply mul_mem <;> grind [IsSwap.mul_mem_closure_three_cycles]
 
+theorem isThreeCycle_subset_alternatingGroup :
+    {g : Perm α | g.IsThreeCycle} ⊆ alternatingGroup α :=
+  fun _ ↦ IsThreeCycle.mem_alternatingGroup
+
+theorem _root_.alternatingGroup.closure_isThreeCycles_eq_top :
+    Subgroup.closure {g : alternatingGroup α | Equiv.Perm.IsThreeCycle (g : Equiv.Perm α)} = ⊤ := by
+  rw [← map_subtype_inj, MonoidHom.map_closure]
+  have : (alternatingGroup α).subtype '' _ = {g : Perm α | IsThreeCycle g} :=
+    Subtype.coe_image_of_subset isThreeCycle_subset_alternatingGroup
+  aesop
+
 /-- The alternating group is the closure of the set of permutations with cycle type (2, 2). -/
-theorem closure_cycleType_eq_2_2_eq_alternatingGroup (h5 : 5 ≤ Nat.card α) :
+theorem closure_cycleType_eq_two_two_eq_alternatingGroup (h5 : 5 ≤ Nat.card α) :
     Subgroup.closure {g : Perm α | g.cycleType = {2, 2}} = alternatingGroup α := by
   apply le_antisymm
   · rw [Subgroup.closure_le]
@@ -227,6 +237,24 @@ theorem closure_cycleType_eq_2_2_eq_alternatingGroup (h5 : 5 ≤ Nat.card α) :
     · apply Subgroup.subset_closure
       exact cycleType_swap_mul_swap_of_nodup (by grind [Finset.mem_compl])
 
+@[deprecated (since := "2026-03-10")]
+alias closure_cycleType_eq_2_2_eq_alternatingGroup :=
+  closure_cycleType_eq_two_two_eq_alternatingGroup
+
+theorem cycleType_eq_two_two_subset_alternatingGroup :
+    {g : Perm α | g.cycleType = {2, 2}} ⊆ alternatingGroup α := by
+  intro g hg
+  rw [Set.mem_setOf_eq] at hg
+  simp [sign_of_cycleType, hg, ← Units.val_inj]
+
+theorem _root_.alternatingGroup.closure_cycleType_eq_two_two_eq_top (h5 : 5 ≤ Nat.card α) :
+    Subgroup.closure {g : alternatingGroup α | (g : Perm α).cycleType = {2, 2}} = ⊤ := by
+  rw [← map_subtype_inj, MonoidHom.map_closure]
+  have : (alternatingGroup α).subtype '' _ = {g : Perm α | g.cycleType = {2, 2}} :=
+    Subtype.coe_image_of_subset cycleType_eq_two_two_subset_alternatingGroup
+  have := closure_cycleType_eq_two_two_eq_alternatingGroup h5
+  aesop
+
 /-- A key lemma to prove $A_5$ is simple. Shows that any normal subgroup of an alternating group on
   at least 5 elements is the entire alternating group if it contains a 3-cycle. -/
 theorem IsThreeCycle.alternating_normalClosure (h5 : 5 ≤ Fintype.card α) {f : Perm α}
@@ -437,6 +465,43 @@ theorem center_eq_bot (hα4 : 4 ≤ Nat.card α) :
     simp only [← Subgroup.mk_smul k this, ← mul_smul, hg']
   simp [k, hc.2.symm, hd.2.symm]
 
+/-- The element of `alternatingGroup α` induced by an element
+of `alternatingGroup s`, when `s : Finset α`. -/
+def ofSubtype (s : Finset α) : alternatingGroup s →* alternatingGroup α where
+  toFun x := ⟨Perm.ofSubtype (x : Perm s), by
+    rw [mem_alternatingGroup, sign_ofSubtype, mem_alternatingGroup.mp x.prop]⟩
+  map_mul' := by simp
+  map_one' := by simp
+
+theorem map_ofSubtype (s : Finset α) :
+    (alternatingGroup s).map (Perm.ofSubtype : Perm s →* Perm α) =
+      (Perm.ofSubtype : Perm s →* Perm α).range ⊓ (alternatingGroup α) := by
+  ext k
+  rw [Subgroup.mem_map, Subgroup.mem_inf, MonoidHom.mem_range]
+  grind [sign_ofSubtype, mem_alternatingGroup]
+
+theorem ofSubtype_comp_subtype (s : Finset α) : (alternatingGroup α).subtype.comp (ofSubtype s) =
+    Perm.ofSubtype.comp (alternatingGroup s).subtype := by
+  rfl
+
+theorem range_ofSubtype (s : Finset α) : (ofSubtype s).range =
+    (Perm.ofSubtype (p := (· ∈ s))).range.subgroupOf (alternatingGroup α) := by
+  rw [← map_subtype_inj, ← MonoidHom.range_comp, ofSubtype_comp_subtype, MonoidHom.range_comp,
+    range_subtype, subgroupOf_map_subtype, map_ofSubtype]
+
+theorem mem_range_ofSubtype_iff (s : Finset α) (k : alternatingGroup α) :
+    k ∈ (ofSubtype s).range ↔ (k : Perm α).support ⊆ s := by
+  rw [range_ofSubtype, mem_subgroupOf, Perm.mem_range_ofSubtype_iff]
+  simp
+
+open Pointwise in
+theorem conj_smul_range_ofSubtype (s : Finset α) (g : alternatingGroup α) :
+    MulAut.conj g • (ofSubtype s).range = (ofSubtype (g • s)).range := by
+  ext k
+  simp_rw [mem_pointwise_smul_iff_inv_smul_mem, mem_range_ofSubtype_iff, ← map_inv,
+    MulAut.smul_def, ← ConjAct.toConjAct_smul_eq_mulAut_conj, ConjAct.coe_smul]
+  simp [support_conj_eq_smul_support, Finset.subset_smul_finset_iff, Subgroup.smul_def]
+
 end alternatingGroup
 
 namespace Equiv.Perm

Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean

@@ -97,12 +97,12 @@ theorem stabilizer.surjective_toPerm {s : Set α} (hs : sᶜ.Nontrivial) :
     exact (Set.disjoint_left.mp hk_support) hx
   intro g
   rcases Int.units_eq_one_or (sign g) with hsg | hsg
-  · use! ofSubtype g
+  · use! Equiv.Perm.ofSubtype g
     · simp [mem_alternatingGroup, hsg]
     · rw [mem_stabilizer_iff, Submonoid.mk_smul]
       exact ofSubtype_mem_stabilizer g
     · aesop
-  · use! ofSubtype g * k
+  · use! Equiv.Perm.ofSubtype g * k
     · simp [mem_alternatingGroup, hk_swap.sign_eq, hsg]
     · rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
     · ext x

Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

@@ -73,6 +73,11 @@ instance {G : Type*} [AddGroup G] [IsAddKleinFour G] : IsKleinFour (Multiplicati
 
 namespace IsKleinFour
 
+@[to_additive]
+theorem isMulCommutative {G : Type*} [Group G] [IsKleinFour G] :
+    IsMulCommutative G where
+  is_comm.comm := mul_comm_of_exponent_two exponent_two
+
 /-- This instance is scoped, because it always applies (which makes linting and typeclass inference
 potentially *a lot* slower). -/
 @[to_additive]