Permutations

Results named in Tau Ceti's TauCeti.GroupTheory.Perm modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Euler bound for a pair of permutations#

For permutations σ and τ of a finite type, the orbits of σ, of τ and of τ * σ together number at most the number of points plus twice the number of orbits of the group generated by σ and τ. For the rotation and edge involution of a ribbon graph these count vertices, edges and faces, and this is the bound χ ≤ 2 on each connected component; equality holds exactly when every component is a sphere.

Equiv.Perm.orbitCount_add_orbitCount_add_orbitCount_mul_le.{u_1} {α : Type u_1} [Finite α]
  (σ τ : Equiv.Perm α) :
  TauCeti.orbitCount σ + TauCeti.orbitCount τ + TauCeti.orbitCount (τ * σ) ≤
    Nat.card α + 2 * Nat.card (MulAction.orbitRel.Quotient (↥(Subgroup.closure {σ, τ})) α)
Lean

Formalized in Tau Ceti as Equiv.Perm.orbitCount_add_orbitCount_add_orbitCount_mul_le.

Sources
LeanEquiv.Perm.orbitCount_add_orbitCount_add_orbitCount_mul_le
Uses 1 · Used by 1
Proof usesHurwitz's transposition bound
Used byThe Riemann–Hurwitz formula for a filled cover

TheoremHurwitz's transposition bound#

If a list of transpositions generates a group acting transitively on a finite type, its length is at least the number of points plus the number of cycles of its product, minus two. Equivalently, Nat.card α + orbitCount L.prod ≤ L.length + 2.

TauCeti.card_add_orbitCount_le_length_add_two.{u_1} {α : Type u_1} [DecidableEq α] [Finite α]
  {L : List (Equiv.Perm α)} (hL : ∀ g ∈ L, g.IsSwap)
  (htrans : MulAction.IsPretransitive (↥(Subgroup.closure {g | g ∈ L})) α) :
  Nat.card α + TauCeti.orbitCount L.prod ≤ L.length + 2
Lean

Formalized in Tau Ceti as TauCeti.card_add_orbitCount_le_length_add_two.

Other forms

Hurwitz's transposition bound with a defect. Formalized in Tau Ceti as TauCeti.card_add_orbitCount_add_two_le_length_add_two_mul_card_orbits.

TauCeti.card_add_orbitCount_add_two_le_length_add_two_mul_card_orbits.{u_1} {α : Type u_1}
  [DecidableEq α] {a b : α} [Finite α] {L M : List (Equiv.Perm α)} (hL : ∀ g ∈ L, g.IsSwap)
  (hM : ∀ g ∈ M, g.IsSwap) (hab : b ∈ MulAction.orbit (↥(Subgroup.closure {g | g ∈ M})) a)
  (h : ¬M.prod.SameCycle a b) :
  Nat.card α + TauCeti.orbitCount (L ++ Equiv.swap a b :: M).prod + 2 ≤
    (L ++ Equiv.swap a b :: M).length +
      2 *
        Nat.card
          (MulAction.orbitRel.Quotient (↥(Subgroup.closure {g | g ∈ L ++ Equiv.swap a b :: M})) α)

Hurwitz's transposition bound, componentwise. Formalized in Tau Ceti as TauCeti.card_add_orbitCount_le_length_add_two_mul_card_orbits.

TauCeti.card_add_orbitCount_le_length_add_two_mul_card_orbits.{u_1} {α : Type u_1} [DecidableEq α]
  [Finite α] {L : List (Equiv.Perm α)} (hL : ∀ g ∈ L, g.IsSwap) :
  Nat.card α + TauCeti.orbitCount L.prod ≤
    L.length + 2 * Nat.card (MulAction.orbitRel.Quotient (↥(Subgroup.closure {g | g ∈ L})) α)
Sources
LeanTauCeti.card_add_orbitCount_le_length_add_two · TauCeti.card_add_orbitCount_add_two_le_length_add_two_mul_card_orbits · TauCeti.card_add_orbitCount_le_length_add_two_mul_card_orbits
Used by 3
Used byThe Euler bound for a pair of permutations · Euler–Poincaré for Khovanov homology · Khovanov's theorem

TheoremJordan's theorem fails in degree p + 1#

A primitive permutation group of degree n containing a cycle of prime length p need not contain the alternating group when p + 1 = n: the affine group AGL(1, 8) of the field with eight elements is primitive on eight points and contains a 7-cycle. This shows that the bound p + 3 ≤ n of TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem cannot be weakened to p + 1 ≤ n.

TauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_add_one_eq :
  ¬∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] (G : Subgroup (Equiv.Perm α)),
      MulAction.IsPreprimitive (↥G) α →
        ∀ g ∈ G,
          g.IsCycle →
            Nat.Prime g.support.card → g.support.card + 1 = Nat.card α → alternatingGroup α ≤ G
Lean

Formalized in Tau Ceti as TauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_add_one_eq.

Sources
LeanTauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_add_one_eq

TheoremJordan's theorem fails in degree p#

A primitive permutation group of degree n containing a cycle of prime length p need not contain the alternating group when p = n: the affine group AGL(1, 5) is primitive on five points and contains a 5-cycle. This shows that the bound p + 3 ≤ n of TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem cannot be weakened to p ≤ n.

TauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_eq :
  ¬∀ (α : Type) [inst : Fintype α] [inst_1 : DecidableEq α] (G : Subgroup (Equiv.Perm α)),
      MulAction.IsPreprimitive (↥G) α →
        ∀ g ∈ G,
          g.IsCycle →
            Nat.Prime g.support.card → g.support.card = Nat.card α → alternatingGroup α ≤ G
Lean

Formalized in Tau Ceti as TauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_eq.

Sources
LeanTauCeti.not_forall_alternatingGroup_le_of_isPreprimitive_of_isCycle_mem_of_card_support_eq

TheoremJordan's theorem for a cycle of prime length (Wielandt, Theorem 13.9)#

A primitive permutation group of degree at least p + 3 that contains a cycle of prime length p contains the alternating group.

TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem.{u_1} {α : Type u_1} [Fintype α]
  [DecidableEq α] {G : Subgroup (Equiv.Perm α)} (hG : MulAction.IsPreprimitive (↥G) α) {p : ℕ}
  (hp : Nat.Prime p) (hp' : p + 3 ≤ Nat.card α) {g : Equiv.Perm α} (hgc : g.IsCycle)
  (hgp : g.support.card = p) (hg : g ∈ G) : alternatingGroup α ≤ G
Lean

Formalized in Tau Ceti as TauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem.

Sources
LeanTauCeti.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.