closure_three_cycles_eq_alternating

English

Let α be a finite type. The subgroup generated by all 3-cycles in Perm(α) is exactly the alternating group on α.

Русский

Пусть α—конечный тип. Подгруппа, порождаемая всеми трёхциклами в Perm(α), равна чередующей группе на α.

LaTeX

$$$$\\operatorname{closure} \\{ \\sigma \\in \\operatorname{Perm}(\\alpha) \\mid \\operatorname{IsThreeCycle}(\\sigma) \\} = \\operatorname{alternatingGroup}(\\alpha).$$$$

Lean4

@[simp]
theorem closure_three_cycles_eq_alternating : closure {σ : Perm α | IsThreeCycle σ} = alternatingGroup α :=
  closure_eq_of_le _ (fun _ hσ => mem_alternatingGroup.2 hσ.sign) fun σ hσ =>
    by
    suffices hind :
      ∀ (n : ℕ) (l : List (Perm α)) (_ : ∀ g, g ∈ l → IsSwap g) (_ : l.length = 2 * n),
        l.prod ∈ closure {σ : Perm α | IsThreeCycle σ}
      by
      obtain ⟨l, rfl, hl⟩ := truncSwapFactors σ
      obtain ⟨n, hn⟩ := (prod_list_swap_mem_alternatingGroup_iff_even_length hl).1 hσ
      rw [← two_mul] at hn
      exact hind n l hl hn
    intro n
    induction n with intro l hl hn
    | zero => simp [List.length_eq_zero_iff.1 hn, one_mem]
    | succ n ih =>
      rw [Nat.mul_succ] at hn
      obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn
      rw [List.length_cons, Nat.succ_inj] at hn
      obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn
      rw [List.prod_cons, List.prod_cons, ← mul_assoc]
      rw [List.length_cons, Nat.succ_inj] at hn
      exact
        mul_mem
          (IsSwap.mul_mem_closure_three_cycles (hl a List.mem_cons_self)
            (hl b (List.mem_cons_of_mem a List.mem_cons_self)))
          (ih _ (fun g hg => hl g (List.mem_cons_of_mem _ (List.mem_cons_of_mem _ hg))) hn)

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