Trying to construct A_4 using permutation.

Stream: new members

[Nick_adfor]

I was trying to construct A_4 using permutation. It need (1)(2)(3)(4)=e, (a b c), and (a b)(c d), the first is to prove they are elements of A_4, the second is to count them up and get 12. With |A_4|=12, the proof is finished.

import Mathlib

open Equiv Perm

def IsDoubleTransposition (σ : Perm (Fin 4)) : Prop :=
  ∃ (a b c d : Fin 4), a ≠ b ∧ c ≠ d ∧
  Disjoint (support (swap a b)) (support (swap c d)) ∧
  σ = swap a b * swap c d

def doubleTranspositions : List (Perm (Fin 4)) :=
  [swap 0 1 * swap 2 3,
   swap 0 2 * swap 1 3,
   swap 0 3 * swap 1 2]

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
  σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  revert σ
  simp only [doubleTranspositions, IsDoubleTransposition]
  decide

lemma doubleTranspositions_mem_A4 :
    ∀ σ ∈ doubleTranspositions, σ ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_mul, Equiv.Perm.IsSwap.sign_eq]
  decide

def ThreeCycles : List (Perm (Fin 4)) :=
  [swap 0 1 * swap 0 2,  -- (0 1 2)
   swap 0 2 * swap 0 1,  -- (0 2 1)
   swap 0 1 * swap 0 3,  -- (0 1 3)
   swap 0 3 * swap 0 1,  -- (0 3 1)
   swap 0 2 * swap 0 3,  -- (0 2 3)
   swap 0 3 * swap 0 2,  -- (0 3 2)
   swap 1 2 * swap 1 3,  -- (1 2 3)
   swap 1 3 * swap 1 2]  -- (1 3 2)
--lean does not have a good way to deFine a list of all 3-cycles, so I use swap products.

lemma mem_allThreeCycles_iff {σ : Perm (Fin 4)} :
    σ ∈ ThreeCycles ↔ σ.IsThreeCycle := by
  revert σ
  simp only [ThreeCycles, ← card_support_eq_three_iff]
  decide

lemma ThreeCycles_mem_A4 :
    ∀ σ ∈ ThreeCycles, σ ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_mul, Equiv.Perm.IsSwap.sign_eq]
  decide

lemma one_mem_A4 : (1 : Perm (Fin 4)) ∈ alternatingGroup (Fin 4) := by
  simp only [Equiv.Perm.mem_alternatingGroup, Perm.sign_one]

lemma card_A4_Fin4 : Fintype.card (alternatingGroup (Fin 4)) = 12 := by
  have h1 := @Fintype.card_perm (Fin 4) _ _
  have h2 := @two_mul_card_alternatingGroup (Fin 4) _ _ _
  rw [h1] at h2
  norm_num at h2
  exact (Nat.eq_of_mul_eq_mul_left zero_lt_two h2).symm

def generators : List (Perm (Fin 4)) :=
  (1 : Perm (Fin 4)) :: (ThreeCycles ++ doubleTranspositions)

lemma generators_subset_A4 : ∀ σ ∈ generators, σ ∈ alternatingGroup (Fin 4) := by
  intros σ hσ
  simp only [generators] at hσ
  cases hσ
  · -- σ = 1
    exact one_mem_A4
  · -- σ ∈ ThreeCycles ++ doubleTranspositions
    rename_i h
    change σ ∈ ThreeCycles ++ doubleTranspositions at h
    simp only [List.mem_append] at h
    cases h
    · rename_i h'
      exact ThreeCycles_mem_A4 σ h'
    · rename_i h'
      exact doubleTranspositions_mem_A4 σ h'

lemma generators_card : generators.length = 1 + ThreeCycles.length + doubleTranspositions.length := by
  simp [generators]
  linarith

def G : Subgroup (Perm (Fin 4)) := Subgroup.closure generators.toFinset

lemma G_subset_A4 : G ≤ alternatingGroup (Fin 4) := by
  dsimp [G]
  rw [Subgroup.closure_le]
  intros σ hσ
  have h_mem := List.mem_toFinset.mp hσ
  exact generators_subset_A4 σ h_mem

open scoped Classical

lemma G_eq_A4 : G = alternatingGroup (Fin 4) := by
  let A4 := alternatingGroup (Fin 4)
  have hG_le : G ≤ A4 := G_subset_A4
  haveI : Finite G := inferInstance
  haveI : Finite A4 := inferInstance
  apply le_antisymm hG_le
  letI := Fintype.ofFinite G
  suffices Nat.card ↥G = Nat.card ↥A4 by
    sorry
  have hG_card : Fintype.card G = 12 := by
    sorry
  have hA4_card : Fintype.card A4 = 12 := card_A4_Fin4
  rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card, hG_card, hA4_card]

But I cannot find a good method to fill the two sorry. It seems that I'm too tired and my mind get stuck. That's terrible.