klein

Stream: mathlib4

[BANGJI HU]

The Klein group is a regular subgroup of A4, how to formalize the question stem·here are my try

import Mathlib.Tactic
import Mathlib.Algebra.Group.Basic


variable(G : Type) [Group G] [IsKleinFour G]
lemma V4_normal : (G : Type) [Group G] [IsKleinFour G] Normal (G : Subgroup (AlternatingGroup (Fin 4))) := by

[Yury G. Kudryashov]

• Why are you interested in this particular question?
• Please provide an unformal math statement & proof.
• Please try to fix the syntax errors or explain what you don't understand about the error messages.

[Antoine Chambert-Loir]

I had to study this for my work on the alternating group. My method, to be found in the Jordan4/V4.lean, is more sophisticated than the non-proof that is usually suggested.

• I consider the set $V$ of elements of A4 with cycle type (2,2) to which I add the identity; this is a four-element set (because one knows the number of permutations of given cycle type).
• In that set, each element $g$ satisfies $g^2=1$.
• Let $S$ be a 2-Sylow subgroup of A4. It has order 4. Any element of $S$ satisfies $g^4=1$; using the possible cycle types, one sees that they belong to $V$.
• Since $S$ and $V$ have both cardinality 4, one has $S=V$.
• This proves that $V$ is a subgroup, and that it is equal to any 2-Sylow subgroup of A4.
• Since all 2-Sylow subgroups are conjugate, $V$ is normal.

[Antoine Chambert-Loir]

A more elementary proof would probably be possible by proving directly that the elements of the set $V$ is stable under products.

[Miyahara Kō]

My formalization in #23555:

• Consider $K_4 := \{0, (0 1)(2 3), (0 2)(1 3), (0 3)(1 2)\}$ as the subgroup of $S_4$, not $A_4$.
• Prove that $\sigma \in K_4$ iff the type of $\sigma$ is none or $(2, 2)$.
• The fact that $K_4$ is normal in $S_4$ follows immediately from this.
• This is normal in $A_4$ too.

[vxctyxeha]

@Miyahara Kō have a look tactic 'decide' failed for proposition
(∀ (x : ↑{1, swap 0 1 * swap 2 3,

import Mathlib
open Equiv Equiv.Perm Subgroup Fintype


abbrev A4 : Subgroup (Perm (Fin 4)) := alternatingGroup (Fin 4)

def kleinFour : Subgroup (Perm (Fin 4)) where
  carrier := {1, swap 0 1 * swap 2 3, swap 0 2 * swap 1 3, swap 0 3 * swap 1 2}
  mul_mem' := by decide
  one_mem' := by decide
  inv_mem' := by decide
lemma kleinFour_le_alternatingGroup : kleinFour ≤ alternatingGroup (Fin 4) := by
  intro p hp
  rw [Equiv.Perm.mem_alternatingGroup]

  simp only [kleinFour, Subgroup.mem_mk, Set.mem_insert_iff, Set.mem_singleton_iff] at hp
  rcases hp with rfl | rfl | rfl | rfl <;>
  decide
lemma mem_kleinFour {p : Perm (Fin 4)} :
    p ∈ kleinFour ↔ p.cycleType ∈ ({0, {2, 2}} : Set (Multiset ℕ)) := by
  revert p; simp_rw [kleinFour, mem_mk, iff_def, forall_and, SetCoe.forall']; decide



instance : kleinFour.Normal where
  conj_mem := by simp [mem_kleinFour]

lemma card_kleinFour : Nat.card kleinFour = 4 := by
simp [kleinFour]
decide
theorem A4_has_normal_subgroup_of_order_4 :
    ∃ (H : Subgroup (Perm (Fin 4))), H ≤ A4 ∧ Nat.card H = 4 ∧ Subgroup.Normal H := by
   use kleinFour

   refine' ⟨_, _, _⟩
   exact kleinFour_le_alternatingGroup
   exact card_kleinFour
   exact instNormalPermFinOfNatNatKleinFour

[Michael Rothgang]

(deleted)