Word Combinatorics: Shuffles and Splits

This file defines the shuffle of two words and prefix-suffix splits of a word, counted with multiplicity, as lists. These are shared between the rough-path signature theory (shuffle identities) and the Munthe-Kaas-Wright Hopf algebra of ordered forests, whose product is a shuffle of forests.

Main definitions

• Word.shuffle - all shuffles of two words, counted with multiplicity
• Word.splits - all prefix-suffix decompositions of a word

@[irreducible]

def HopfAlgebras.Word.shuffle {α : Type u} : List α → List α → List (List α)

All shuffles of two words, with multiplicity.

Equations

• One or more equations did not get rendered due to their size.
• HopfAlgebras.Word.shuffle [] x✝ = [x✝]
• HopfAlgebras.Word.shuffle x✝ [] = [x✝]

@[simp]

theorem HopfAlgebras.Word.shuffle_nil_left {α : Type u} (v : List α) : shuffle [] v = [v]

@[simp]

theorem HopfAlgebras.Word.shuffle_nil_right {α : Type u} (u : List α) : shuffle u [] = [u]

@[simp]

theorem HopfAlgebras.Word.shuffle_cons_cons {α : Type u} (a b : α) (u v : List α) : shuffle (a :: u) (b :: v) = List.map (fun (w : List α) => a :: w) (shuffle u (b :: v)) ++ List.map (fun (w : List α) => b :: w) (shuffle (a :: u) v)

theorem HopfAlgebras.Word.length_shuffle {α : Type u} (u v : List α) : (shuffle u v).length = (u.length + v.length).choose u.length

The number of shuffles of two words is the binomial coefficient.

theorem HopfAlgebras.Word.shuffle_map {α : Type u} {β : Type v} (f : α → β) (u v : List α) : List.map (List.map f) (shuffle u v) = shuffle (List.map f u) (List.map f v)

theorem HopfAlgebras.Word.shuffle_ne_nil {α : Type u} (u v : List α) : shuffle u v ≠ []

theorem HopfAlgebras.Word.perm_append_of_mem_shuffle {α : Type u} {u v w : List α} : w ∈ shuffle u v → w.Perm (u ++ v)

Every shuffle of u and v is a permutation of u ++ v.

theorem HopfAlgebras.Word.length_of_mem_shuffle {α : Type u} {u v w : List α} (hw : w ∈ shuffle u v) : w.length = u.length + v.length

theorem HopfAlgebras.Word.eq_nil_of_mem_shuffle {α : Type u} {u v w : List α} (hw : w ∈ shuffle u v) (hnil : w = []) : u = [] ∧ v = []

theorem HopfAlgebras.Word.ne_nil_of_mem_shuffle_left {α : Type u} {u v w : List α} (hw : w ∈ shuffle u v) (hu : u ≠ []) : w ≠ []

theorem HopfAlgebras.Word.ne_nil_of_mem_shuffle_right {α : Type u} {u v w : List α} (hw : w ∈ shuffle u v) (hv : v ≠ []) : w ≠ []

theorem HopfAlgebras.Word.shuffle_singleton_concat_perm {α : Type u} (a b : α) (v : List α) : (shuffle [a] (v ++ [b])).Perm ((v ++ [b] ++ [a]) :: List.map (fun (w : List α) => w ++ [b]) (shuffle [a] v))

Shuffling a single letter into a word ending in b: either a lands at the very end, or it shuffles into the prefix.

theorem HopfAlgebras.Word.shuffle_concat_singleton_perm {α : Type u} (a b : α) (u : List α) : (shuffle (u ++ [a]) [b]).Perm ((u ++ [a] ++ [b]) :: List.map (fun (w : List α) => w ++ [a]) (shuffle u [b]))

Shuffling a word ending in a with a single letter b: either b lands at the very end, or it shuffles into the prefix.

theorem HopfAlgebras.Word.shuffle_concat_concat_perm {α : Type u} (a b : α) (u v : List α) : (shuffle (u ++ [a]) (v ++ [b])).Perm (List.map (fun (w : List α) => w ++ [a]) (shuffle u (v ++ [b])) ++ List.map (fun (w : List α) => w ++ [b]) (shuffle (u ++ [a]) v))

The right-end recursion for shuffles: every shuffle of u ++ [a] and v ++ [b] ends in either a or b.

theorem HopfAlgebras.Word.shuffle_comm_perm {α : Type u} (u v : List α) : (shuffle u v).Perm (shuffle v u)

Shuffling is commutative up to permutation.

theorem HopfAlgebras.Word.shuffle_flatMap_shuffle_perm {α : Type u} (x y z : List α) : (List.flatMap (fun (w : List α) => shuffle w z) (shuffle x y)).Perm (List.flatMap (fun (w : List α) => shuffle x w) (shuffle y z))

Shuffle associativity at the level of multisets of words: shuffling x ⧢ y against z produces the same words, with multiplicity, as shuffling x against y ⧢ z.

theorem HopfAlgebras.Word.shuffle_exchange_perm {α : Type u} (x y z : List α) : (List.flatMap (fun (w : List α) => shuffle w z) (shuffle x y)).Perm (List.flatMap (fun (w : List α) => shuffle w y) (shuffle x z))

Exchange of the shuffle arguments: shuffling x ⧢ y against z gives the same multiset of words as shuffling x ⧢ z against y.

theorem HopfAlgebras.Word.flatMap_comm_perm {α β γ : Type u} (l : List α) (m : List β) (f : α → β → List γ) : (List.flatMap (fun (a : α) => List.flatMap (fun (b : β) => f a b) m) l).Perm (List.flatMap (fun (b : β) => List.flatMap (fun (a : α) => f a b) l) m)

Independent flatMaps commute up to permutation.

def HopfAlgebras.Word.splits {α : Type u} : List α → List (List α × List α)

All prefix-suffix decompositions of a word.

Equations

• HopfAlgebras.Word.splits [] = [([], [])]
• HopfAlgebras.Word.splits (x_1 :: w) = ([], x_1 :: w) :: List.map (fun (p : List α × List α) => (x_1 :: p.1, p.2)) (HopfAlgebras.Word.splits w)

@[simp]

theorem HopfAlgebras.Word.splits_nil {α : Type u} : splits [] = [([], [])]

@[simp]

theorem HopfAlgebras.Word.splits_cons {α : Type u} (x : α) (w : List α) : splits (x :: w) = ([], x :: w) :: List.map (fun (p : List α × List α) => (x :: p.1, p.2)) (splits w)

theorem HopfAlgebras.Word.splits_map {α : Type u} {β : Type v} (f : α → β) (w : List α) : List.map (fun (p : List α × List α) => (List.map f p.1, List.map f p.2)) (splits w) = splits (List.map f w)

theorem HopfAlgebras.Word.mem_splits_append {α : Type u} {w : List α} {p : List α × List α} : p ∈ splits w → p.1 ++ p.2 = w

theorem HopfAlgebras.Word.flatMap_cons_perm_map_flatMap {α : Type u} {β : Type v} (xs : List α) (head : α → β) (tail : α → List β) : (List.flatMap (fun (x : α) => head x :: tail x) xs).Perm (List.map head xs ++ List.flatMap tail xs)

@[reducible, inline]

abbrev HopfAlgebras.Word.TripleSplits (α : Type u) : Type u

Equations

• HopfAlgebras.Word.TripleSplits α = (List α × List α × List α)

def HopfAlgebras.Word.leftSplits3 {α : Type u} (w : List α) : List (TripleSplits α)

Equations

• One or more equations did not get rendered due to their size.

def HopfAlgebras.Word.rightSplits3 {α : Type u} (w : List α) : List (TripleSplits α)

Equations

• One or more equations did not get rendered due to their size.

theorem HopfAlgebras.Word.leftSplits3_perm_rightSplits3 {α : Type u} (w : List α) : (leftSplits3 w).Perm (rightSplits3 w)