Documentation

Complexity.Foundations.GroupTheory.Perm.FiveCycle

Five-cycles #

A five-cycle is a permutation of cycle type {5} (Equiv.Perm.IsFiveCycle), defined like Mathlib's Equiv.Perm.IsThreeCycle. Five-cycles are even (Equiv.Perm.IsFiveCycle.sign), all five-cycles are conjugate (Equiv.Perm.IsFiveCycle.isConj), and in Fin 5 every five-cycle is a commutator of two five-cycles (Equiv.Perm.IsFiveCycle.exists_commutator), the fact behind Barrington's theorem [Bar89].

Main definitions #

Main results #

References #

source
def Equiv.Perm.IsFiveCycle {α : Type u_1} [DecidableEq α] [Fintype α] (σ : Perm α) :
Prop

A five-cycle is a cycle of length 5.

Instances For
    source
    theorem Equiv.Perm.IsFiveCycle.cycleType {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ.IsFiveCycle) :
    σ.cycleType = {5}

    A five-cycle has cycle type {5}.

    source
    theorem Equiv.Perm.IsFiveCycle.ne_one {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ.IsFiveCycle) :
    σ ≠ 1

    A five-cycle is not the identity.

    source
    theorem Equiv.Perm.IsFiveCycle.inv {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ.IsFiveCycle) :
    σ⁻¹.IsFiveCycle

    The inverse of a five-cycle is a five-cycle.

    source
    @[simp]
    theorem Equiv.Perm.IsFiveCycle.inv_iff {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} :
    σ⁻¹.IsFiveCycle ↔ σ.IsFiveCycle

    σ⁻¹ is a five-cycle exactly when σ is.

    source
    theorem Equiv.Perm.IsFiveCycle.sign {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ.IsFiveCycle) :
    Perm.sign σ = 1

    A five-cycle has sign 1.

    source
    theorem Equiv.Perm.IsFiveCycle.mem_alternatingGroup {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ.IsFiveCycle) :
    σ ∈ alternatingGroup α

    Five-cycles are even.

    source
    theorem Equiv.Perm.IsFiveCycle.conj {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} (h : σ.IsFiveCycle) (ρ : Perm α) :
    (ρ * σ * ρ⁻¹).IsFiveCycle

    A conjugate ρ * σ * ρ⁻¹ of a five-cycle is a five-cycle.

    source
    theorem Equiv.Perm.IsFiveCycle.isConj {α : Type u_1} [DecidableEq α] [Fintype α] {σ τ : Perm α} (hσ : σ.IsFiveCycle) (hτ : τ.IsFiveCycle) :
    IsConj σ τ

    All five-cycles are conjugate.

    source
    theorem Equiv.Perm.isFiveCycle_formPerm {α : Type u_1} [DecidableEq α] [Fintype α] {l : List α} (hl : l.Nodup) (hlen : l.length = 5) :
    l.formPerm.IsFiveCycle

    The cyclic permutation of a list of five distinct elements is a five-cycle.

    source
    theorem Equiv.Perm.IsFiveCycle.exists_commutator {σ : Perm (Fin 5)} (hσ : σ.IsFiveCycle) :
    ∃ (τ₁ : Perm (Fin 5)) (τ₂ : Perm (Fin 5)), τ₁.IsFiveCycle ∧ τ₂.IsFiveCycle ∧ ⁅τ₁, τ₂⁆ = σ

    Every five-cycle of Fin 5 is the commutator of two five-cycles [Bar89].