feat(GroupTheory/SpecificGroups/Alternating/Simple): simplicity of the alternating groups

Mathlib.lean

@@ -4683,6 +4683,7 @@ public import Mathlib.GroupTheory.SpecificGroups.Alternating
 public import Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
 public import Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
 public import Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
+public import Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
 public import Mathlib.GroupTheory.SpecificGroups.Cyclic
 public import Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
 public import Mathlib.GroupTheory.SpecificGroups.Dihedral

Mathlib/Algebra/Group/Subgroup/Map.lean

@@ -372,6 +372,10 @@ theorem subgroupOf_eq_top {H K : Subgroup G} : H.subgroupOf K = ⊤ ↔ K ≤ H
 
 variable (H : Subgroup G)
 
+@[to_additive]
+instance [IsMulCommutative G] : IsMulCommutative H :=
+  IsMulCommutative.of_setLike_mul_comm fun a _ b _ ↦ mul_comm' a b
+
 @[to_additive]
 instance map_isMulCommutative (f : G →* G') [IsMulCommutative H] : IsMulCommutative (H.map f) := by
   refine .of_setLike_mul_comm ?_

Mathlib/FieldTheory/Galois/Profinite.lean

@@ -304,7 +304,7 @@ lemma isOpen_mulEquivToLimit_image_fixingSubgroup [IsGalois k K]
     exact (isOpen_induced <| (continuous_apply (op L)).isOpen_preimage {1} trivial)
   ext x
   obtain ⟨σ, rfl⟩ := (mulEquivToLimit k K).surjective x
-  simpa using FiniteGaloisIntermediateField.mem_fixingSubgroup_iff _ _
+  simpa using FiniteGaloisIntermediateField.mem_fixingSubgroup_iff σ L
 
 set_option backward.isDefEq.respectTransparency false in
 lemma mulEquivToLimit_symm_continuous [IsGalois k K] : Continuous (mulEquivToLimit k K).symm := by

Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

@@ -532,7 +532,7 @@ variable (α) in
 theorem isMultiplyPretransitive (n : ℕ) :
     IsMultiplyPretransitive (Perm α) α n := by
   rw [isMultiplyPretransitive_iff]
-  exact fun x y => exists_smul_eq_embedding x y
+  exact exists_smul_eq_embedding
 
 /-- The action of the permutation group of `α` on `α` is preprimitive -/
 instance : IsPreprimitive (Perm α) α :=

Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean

@@ -208,6 +208,24 @@ theorem mulActionHom_compl_bijective :
 
 end compl
 
+variable {G} in
+set_option backward.isDefEq.respectTransparency false in
+theorem fixedPoints_ne_univ_of_faithfulSMul
+    [Nontrivial G] [FaithfulSMul G α]
+    (n : ℕ) (hn : 0 < n) (hn' : n < Nat.card α) :
+    fixedPoints G (Set.powersetCard α n) ≠ _root_.Set.univ := by
+  have : Finite α := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt hn')
+  obtain ⟨g, h⟩ := exists_ne (1 : G)
+  contrapose! h
+  replace h : (toPerm g : Perm (Set.powersetCard α n)) = 1 := by
+    ext1 s
+    exact Set.eq_univ_iff_forall.mp h s g
+  rwa [← toPermHom_apply, map_eq_one_iff] at h
+  have := Set.powersetCard.faithfulSMul (G := G) (α := α) (n := n) ?_ ?_
+  · exact MulAction.toPerm_injective
+  · exact hn
+  · rwa [ENat.card_eq_coe_natCard, Nat.cast_lt]
+
 variable (α)
 
 /-- The obvious map from a type to its 1-combinations, as an equivariant map. -/

Mathlib/GroupTheory/SpecificGroups/Alternating.lean

@@ -9,6 +9,7 @@ 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.SpecificGroups.Cyclic
 public import Mathlib.GroupTheory.Subgroup.Simple
 public import Mathlib.Tactic.IntervalCases
 
@@ -143,6 +144,47 @@ theorem nat_card_alternatingGroup [Nontrivial α] :
 
 namespace alternatingGroup
 
+theorem isCyclic_of_card_le_three (hα : Nat.card α ≤ 3) :
+    IsCyclic (alternatingGroup α) := by
+  cases subsingleton_or_nontrivial α
+  · infer_instance
+  have : 1 < Nat.card α := Finite.one_lt_card
+  apply isCyclic_of_card_dvd_prime (p := 3)
+  rw [nat_card_alternatingGroup]
+  interval_cases (Nat.card α) <;> simp [Nat.factorial_succ]
+
+theorem isMulCommutative_of_card_le_three (hα : Nat.card α ≤ 3) :
+    IsMulCommutative (alternatingGroup α) :=
+  (isCyclic_of_card_le_three hα).isMulCommutative
+
+theorem isMulCommutative_iff_card_le_three :
+    IsMulCommutative (alternatingGroup α) ↔ Nat.card α ≤ 3 := by
+  refine ⟨fun ⟨⟨H⟩⟩ ↦ ?_, fun h ↦ (isCyclic_of_card_le_three h).isMulCommutative⟩
+  rw [← not_lt, ← Set.ncard_univ, Set.three_lt_ncard_iff]
+  push Not
+  intro a b c d _ _ _ _ hab hac had hbc hbd
+  by_contra hcd
+  apply Ne.symm hcd
+  let g : alternatingGroup α := ⟨swap a b * swap a c, by
+    rw [mem_alternatingGroup]
+    exact (isThreeCycle_swap_mul_swap_same hab hac hbc).sign⟩
+  let h : alternatingGroup α := ⟨swap a b * swap a d, by
+    rw [mem_alternatingGroup]
+    exact (isThreeCycle_swap_mul_swap_same hab had hbd).sign⟩
+  specialize H g h
+  simp only [MulMemClass.mk_mul_mk, Subtype.mk.injEq, Perm.ext_iff, Perm.coe_mul,
+    Function.comp_apply, EmbeddingLike.apply_eq_iff_eq, g, h] at H
+  simpa only [swap_apply_left,
+    swap_apply_of_ne_of_ne (Ne.symm had) (Ne.symm hbd),
+    swap_apply_of_ne_of_ne (Ne.symm hac) (Ne.symm hbc),
+    swap_apply_of_ne_of_ne (Ne.symm hac) hcd,
+    swap_apply_of_ne_of_ne (Ne.symm had) (Ne.symm hcd)] using H a
+
+theorem isCyclic_iff_card_le_three :
+    IsCyclic (alternatingGroup α) ↔ Nat.card α ≤ 3 :=
+  ⟨fun _ ↦ by rw [← isMulCommutative_iff_card_le_three]; exact IsCyclic.isMulCommutative,
+   isCyclic_of_card_le_three⟩
+
 open Equiv.Perm
 
 instance normal : (alternatingGroup α).Normal :=
@@ -171,9 +213,10 @@ theorem isConj_of {σ τ : alternatingGroup α} (hc : IsConj (σ : Perm α) (τ
         exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
       simp [mul_assoc, hd.commute.eq]
 
-theorem isThreeCycle_isConj (h5 : 5 ≤ Fintype.card α) {σ τ : alternatingGroup α}
-    (hσ : IsThreeCycle (σ : Perm α)) (hτ : IsThreeCycle (τ : Perm α)) : IsConj σ τ :=
-  alternatingGroup.isConj_of (isConj_iff_cycleType_eq.2 (hσ.trans hτ.symm))
+theorem isThreeCycle_isConj (h5 : 5 ≤ Nat.card α) {σ τ : alternatingGroup α}
+    (hσ : IsThreeCycle (σ : Perm α)) (hτ : IsThreeCycle (τ : Perm α)) : IsConj σ τ := by
+  simp only [Nat.card_eq_fintype_card] at h5
+  exact alternatingGroup.isConj_of (isConj_iff_cycleType_eq.2 (hσ.trans hτ.symm))
     (by rwa [hσ.card_support])
 
 end alternatingGroup
@@ -257,7 +300,7 @@ theorem _root_.alternatingGroup.closure_cycleType_eq_two_two_eq_top (h5 : 5 ≤
 
 /-- 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 α}
+theorem IsThreeCycle.alternating_normalClosure (h5 : 5 ≤ Nat.card α) {f : Perm α}
     (hf : IsThreeCycle f) :
     normalClosure ({⟨f, hf.mem_alternatingGroup⟩} : Set (alternatingGroup α)) = ⊤ := by
   rw [eq_top_iff, ← map_subtype_le_map_subtype, ← MonoidHom.range_eq_map, range_subtype,
@@ -319,7 +362,7 @@ theorem normalClosure_finRotate_five : normalClosure ({⟨finRotate 5,
       have h3 :
         IsThreeCycle (Fin.cycleRange 2 * finRotate 5 * (Fin.cycleRange 2)⁻¹ * (finRotate 5)⁻¹) :=
         card_support_eq_three_iff.1 (by decide)
-      rw [← h3.alternating_normalClosure (by rw [card_fin])]
+      rw [← h3.alternating_normalClosure (by rw [Nat.card_eq_fintype_card, card_fin])]
       refine normalClosure_le_normal ?_
       rw [Set.singleton_subset_iff, SetLike.mem_coe]
       have h :
@@ -415,7 +458,7 @@ instance isSimpleGroup_five : IsSimpleGroup (alternatingGroup (Fin 5)) :=
     -- If `n = 3`, then `g` has a 3-cycle in its decomposition, so `g^2` is a 3-cycle.
     -- `g^2` is in the normal closure of `g`, so that normal closure must be $A_5$.
     · rw [eq_top_iff, ← (isThreeCycle_sq_of_three_mem_cycleType_five ng).alternating_normalClosure
-        (by rw [card_fin])]
+        (by rw [Nat.card_eq_fintype_card, card_fin])]
       refine normalClosure_le_normal ?_
       rw [Set.singleton_subset_iff, SetLike.mem_coe]
       have h := SetLike.mem_coe.1 (subset_normalClosure
@@ -473,6 +516,18 @@ def ofSubtype (s : Finset α) : alternatingGroup s →* alternatingGroup α wher
   map_mul' := by simp
   map_one' := by simp
 
+theorem ofSubtype_injective {s : Finset α} : Function.Injective (ofSubtype s) := by
+  rw [← Function.Injective.of_comp_iff (alternatingGroup α).subtype_injective]
+  exact Perm.ofSubtype_injective.comp (alternatingGroup s).subtype_injective
+
+theorem ofSubtype_inj {s : Finset α} {g h : alternatingGroup s} :
+    ofSubtype s g = ofSubtype s h ↔ g = h :=
+  ofSubtype_injective.eq_iff
+
+theorem coe_ofSubtype (s : Finset α) (k : alternatingGroup s) :
+    (ofSubtype s k : Equiv.Perm α) = Equiv.Perm.ofSubtype k.1 := by
+  rfl
+
 theorem map_ofSubtype (s : Finset α) :
     (alternatingGroup s).map (Perm.ofSubtype : Perm s →* Perm α) =
       (Perm.ofSubtype : Perm s →* Perm α).range ⊓ (alternatingGroup α) := by

Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

@@ -246,7 +246,7 @@ theorem centralizer_le_alternating_iff :
 
 namespace IsThreeCycle
 
-variable (h5 : 5 ≤ Fintype.card α) {g : alternatingGroup α} (hg : IsThreeCycle (g : Perm α))
+variable (h5 : 5 ≤ Nat.card α) {g : alternatingGroup α} (hg : IsThreeCycle (g : Perm α))
 
 include h5 hg
 
@@ -276,7 +276,7 @@ theorem alternatingGroup.commutator_perm_le :
   simp [map_commutatorElement, commutatorElement_eq_one_iff_commute, Commute.all]
 
 /-- If `n ≥ 5`, then the alternating group on `n` letters is perfect -/
-theorem commutator_alternatingGroup_eq_top (h5 : 5 ≤ Fintype.card α) :
+theorem commutator_alternatingGroup_eq_top (h5 : 5 ≤ Nat.card α) :
     commutator (alternatingGroup α) = ⊤ := by
   suffices closure {b : alternatingGroup α | (b : Perm α).IsThreeCycle} = ⊤ by
     rw [eq_top_iff, ← this, Subgroup.closure_le]
@@ -286,13 +286,13 @@ theorem commutator_alternatingGroup_eq_top (h5 : 5 ≤ Fintype.card α) :
   exact Subgroup.closure_closure_coe_preimage
 
 /-- If `n ≥ 5`, then the alternating group on `n` letters is perfect (subgroup version) -/
-theorem commutator_alternatingGroup_eq_self (h5 : 5 ≤ Fintype.card α) :
+theorem commutator_alternatingGroup_eq_self (h5 : 5 ≤ Nat.card α) :
     ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α := by
   rw [← Subgroup.map_subtype_commutator, commutator_alternatingGroup_eq_top h5,
     ← MonoidHom.range_eq_map, Subgroup.range_subtype]
 
 /-- The commutator subgroup of the permutation group is the alternating group -/
-theorem alternatingGroup.commutator_perm_eq (h5 : 5 ≤ Fintype.card α) :
+theorem alternatingGroup.commutator_perm_eq (h5 : 5 ≤ Nat.card α) :
     commutator (Perm α) = alternatingGroup α := by
   apply le_antisymm alternatingGroup.commutator_perm_le
   rw [← commutator_alternatingGroup_eq_self h5]