Shuffle–deconcatenation compatibility

The keystone bialgebra theorem of the word shuffle Hopf algebra: the prefix–suffix splittings of all shuffles of u and v are, with multiplicity, the pairs of shuffles of splittings of u and of v (Word.shuffle_splits_perm). This drives both Chen's theorem for piecewise-linear signatures and the bialgebra axiom of HopfAlgebras.wordHopf.

def HopfAlgebras.Word.splitShufflePairs {α : Type u} (u v : List α) : List (List α × List α)

The shuffles of splittings of u and v, as prefix–suffix pairs.

Equations

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

theorem HopfAlgebras.Word.splitShufflePairs_def {α : Type u} (u v : List α) : splitShufflePairs u v = List.flatMap (fun (p : List α × List α) => List.flatMap (fun (q : List α × List α) => List.flatMap (fun (x : List α) => List.map (fun (y : List α) => (x, y)) (shuffle p.2 q.2)) (shuffle p.1 q.1)) (splits v)) (splits u)

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

Prefix a letter to the first component of a splitting.

Equations

• HopfAlgebras.Word.consFst a p = (a :: p.1, p.2)

@[simp]

theorem HopfAlgebras.Word.consFst_apply {α : Type u} (a : α) (p : List α × List α) : consFst a p = (a :: p.1, p.2)

Small loop lemmas

Degenerate cases

theorem HopfAlgebras.Word.splitShufflePairs_nil_left {α : Type u} (v : List α) : splitShufflePairs [] v = splits v

theorem HopfAlgebras.Word.splitShufflePairs_nil_right {α : Type u} (u : List α) : splitShufflePairs u [] = splits u

The cons–cons decompositions

theorem HopfAlgebras.Word.shuffle_splits_perm {α : Type u} (u v : List α) : (List.flatMap splits (shuffle u v)).Perm (splitShufflePairs u v)

Shuffle–deconcatenation bialgebra compatibility.