Permutation A_4

Stream: new members

[Nick_adfor]

How to prove that e, (a b c), (a b)(c d) generate A_4
a, b, c, d = 0 or 1 or 2 or 3.

I think that this trivial proof must be already a theorem in lean. But I do not find it. Even a swap product need to be defined by myself! Is there any easier way?

[Nick_adfor]

def IsDoubleTransposition (σ : Perm (Fin 4)) : Prop :=

  ∃ (a b c d : Fin 4), a ≠ b ∧ c ≠ d ∧

  Disjoint ({a, b} : Finset (Fin 4)) ({c, d} : Finset (Fin 4)) ∧

  σ = swap a b * swap c d

[Kevin Buzzard]

Can you formalize your question in Lean? Or are you asking a maths question?

[Nick_adfor]

Kevin Buzzard said:

Can you formalize your question in Lean? Or are you asking a maths question?

Yes, and I'm trying. Now the first step is to prove all the generators are in A_4.

[Kevin Buzzard]

Can you edit your code to make it a #mwe , so that people can run your code with just one click? I can't get this compiling as it stands. Was it written by a language model by the way? Does it compile for you?

[Nick_adfor]

Kevin Buzzard said:

Can you edit your code to make it a #mwe , so that people can run your code with just one click? I can't get this compiling as it stands. Was it written by a language model by the way? Does it compile for you?

I was trying to prove it by:

Lemma 1: Prove that all elements of the generating set are in A₄
Lemma 2: Prove that every element of A₄ can be generated by the generating set
Main Theorem: A₄ is generated by three types of permutations

And I am on lemma 1 now. "simp only" is totally wrong. I'm trying to fix it.

[Nick_adfor]

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 sorry

mwe is here now.

[Nick_adfor]

The discussion is here now.

#new members > I want to write a lemma eq_empty_iff_forall_not_mem