(alternatingGroup (Fin 4))=⊤

Stream: maths

[Move fast]

import Mathlib
open Equiv Equiv.Perm Subgroup Fintype
/-I want to show $A_{4}$ is not simple.-/

/-- Find a normal subgroup in $A_{4}$ of order 4.
 define the subgroup in the problem. -/
def alt_nsubgrp_four : Subgroup (alternatingGroup (Fin 4)) where
  -- the carrier of the subgroup
  carrier := {1, ⟨swap 0 1 * swap 2 3, rfl⟩, ⟨swap 0 2 * swap 1 3, rfl⟩, ⟨swap 0 3 * swap 1 2, rfl⟩}
  -- the set is closed under multiplication
  mul_mem' := by
    intro a b ha hb; simp only [Fin.isValue, Set.mem_insert_iff, Set.mem_singleton_iff] at *
    -- check all cases
    rcases ha with ha | ha | ha | ha; all_goals rcases hb with hb | hb | hb | hb
    all_goals rw [ha, hb]; decide
  -- one is in the set
  one_mem' := by decide
  -- the set is closed under inverses
  inv_mem' := by decide
/-- prove the subgroup has such properties mentioned in the problem. -/
theorem exists_alt_nsubgrp_four :  Nat.card alt_nsubgrp_four = 4 ∧
  Subgroup.Normal alt_nsubgrp_four := by
  constructor; all_goals unfold alt_nsubgrp_four
    -- verify the cardinality
  · simp only [Fin.isValue, Subgroup.mem_mk, Set.mem_insert_iff, Set.mem_singleton_iff,
    Nat.card_eq_fintype_card]; rfl
  -- verify the subgroup is normal by testing its normaliser
  refine Subgroup.normalizer_eq_top_iff.mp ?_
  -- prove the normaliser is the entire group
  ext x; simp only [Fin.isValue, Subgroup.mem_top, iff_true]
  -- use the definition of normalisers
  refine Subgroup.mem_normalizer_iff'.mpr ?_
  simp only [Fin.isValue, Subgroup.mem_mk, Set.mem_insert_iff, Set.mem_singleton_iff,
    Subtype.forall, mem_alternatingGroup]
  -- plug in all cases to get the result
  -- **Note:** here we can use `decide` as well (and the conclusion will follow in a few seconds),
  -- but compared to `native_decide` it seems to take forever. should `native_decide` be avoided?
  native_decide +revert

set_option synthInstance.maxHeartbeats 400000
/--$A{4}$ is not simple.-/
theorem alternatingGroup_simple_for_4  :
    ¬IsSimpleGroup (alternatingGroup (Fin 4)) := by
  --  -- **Goal.** Construct a *proper* normal subgroup of $A_{4}$$.
  by_contra simple
  --|alt_nsubgrp_four|=4 and alt_nsubgrp_four is normal in $A_4$
  have h1:Nat.card alt_nsubgrp_four = 4 ∧ Subgroup.Normal alt_nsubgrp_four := by
    exact exists_alt_nsubgrp_four
  -- In a simple group, any normal subgroup is either ⊥ or ⊤.
  rcases (simple.2 alt_nsubgrp_four h1.2) with h|h
  have h2: alt_nsubgrp_four ≠ ⊥:=by
    intro h
    rw [h] at h1
    simp at h1
  contradiction
    --alt_nsubgrp_four = ⊤
  have h3: alt_nsubgrp_four ≠  ⊤:=by
    intro h
    rw [h] at h1
    have card_4:Nat.card alt_nsubgrp_four=4:=by
      apply exists_alt_nsubgrp_four.1
    have card_A4 : Nat.card (alternatingGroup (Fin 4))= 12 := by
      simp [@Nat.card_perm (Fin 4), Nat.card_eq_fintype_card, Fintype.card_fin]
      rfl
    have :(alternatingGroup (Fin 4))=⊤:= by
      sorry --I can't get (alternatingGroup (Fin 4))=⊤, and so I can't get the contradiction.
    rw [h] at card_4
    rw [this] at card_A4
    simp_all
  contradiction

In the sorry line, I can't get (alternatingGroup (Fin 4))=⊤, and so I can't get the contradiction. Does anyone know how to solve it? I want to use rfl to prove it, but it failed.

[张守信(Shouxin Zhang)]

Consider using Subgroup.card_top rather than attempting to directly prove that the group is equal to its top subgroup in the type universe—I suspect that equality might not hold, or perhaps it's not provable.

[Move fast]

Yeah, in the latest Lean, I can get it by simp_all. But I can get the result as you say. Thank you very much.

[Antoine Chambert-Loir]

docs#alternatingGroup is a subgroup of docs#Equiv.Perm. Except for a subsingleton type, it is not equal to ⊤, it has index two, as expressed by docs#alternatingGroup.index_eq_two