isSimpleGroup_five — Mathlib

English

The alternating group on five elements is a simple group.

Русский

Чередующаяся группа на пяти элементах простая.

LaTeX

$$$$\\text{IsSimpleGroup}(\\operatorname{alternatingGroup}(\\operatorname{Fin}(5))).$$$$

Lean4

/-- Shows that $A_5$ is simple by taking an arbitrary non-identity element and showing by casework
  on its cycle type that its normal closure is all of $A_5$. -/
instance isSimpleGroup_five : IsSimpleGroup (alternatingGroup (Fin 5)) :=
  ⟨fun H => by
    intro Hn
    refine or_not.imp id fun Hb => ?_
    rw [eq_bot_iff_forall] at Hb
    push_neg at Hb
    obtain ⟨⟨g, gA⟩, gH, g1⟩ : ∃ x : ↥(alternatingGroup (Fin 5)), x ∈ H ∧ x ≠ 1 := Hb
    rw [← SetLike.mem_coe, ← Set.singleton_subset_iff] at gH
    refine
      eq_top_iff.2
        (le_trans (ge_of_eq ?_) (normalClosure_le_normal gH))
          -- It suffices to show that the normal closure of `g` in $A_5$ is $A_5$.

    by_cases h2 :
      ∀ n ∈ g.cycleType,
        n =
          2
            -- If the cycle decomposition of `g` consists entirely of swaps, then the cycle type is $(2,2)$.
                -- This means that it is conjugate to $(04)(13)$, whose normal closure is $A_5$.

    · rw [Ne, Subtype.ext_iff] at g1
      exact (isConj_swap_mul_swap_of_cycleType_two gA g1 h2).normalClosure_eq_top_of normalClosure_swap_mul_swap_five
    push_neg at h2
    obtain ⟨n, ng, n2⟩ : ∃ n : ℕ, n ∈ g.cycleType ∧ n ≠ 2 := h2
    have n2' : 2 < n := lt_of_le_of_ne (two_le_of_mem_cycleType ng) n2.symm
    have n5 : n ≤ 5 := le_trans ?_ g.support.card_le_univ
    swap
    · obtain ⟨m, hm⟩ := Multiset.exists_cons_of_mem ng
      rw [← sum_cycleType, hm, Multiset.sum_cons]
      exact le_add_right le_rfl
    interval_cases n
    · rw [eq_top_iff, ← (isThreeCycle_sq_of_three_mem_cycleType_five ng).alternating_normalClosure (by rw [card_fin])]
      refine normalClosure_le_normal ?_
      rw [Set.singleton_subset_iff, SetLike.mem_coe]
      have h := SetLike.mem_coe.1 (subset_normalClosure (G := alternatingGroup (Fin 5)) (Set.mem_singleton ⟨g, gA⟩))
      exact mul_mem h h
    · -- The case `n = 4` leads to contradiction, as no element of $A_5$ includes a 4-cycle.

      have con := mem_alternatingGroup.1 gA
      rw [sign_of_cycleType, cycleType_of_card_le_mem_cycleType_add_two (by decide) ng] at con
      have : Odd 5 := by decide
      simp [this] at con
    · -- If `n = 5`, then `g` is itself a 5-cycle, conjugate to `finRotate 5`.

      refine (isConj_iff_cycleType_eq.2 ?_).normalClosure_eq_top_of normalClosure_finRotate_five
      rw [cycleType_of_card_le_mem_cycleType_add_two (by decide) ng, cycleType_finRotate]⟩

Похожие утверждения