Towards the MKW Bialgebra Law

This file defines the pairwise-shuffle product of MKW coproduct term lists (the operation ⊔⊔ of arXiv:math/0603023) and the grafting tail of the coproduct recursion, together with their unit laws. These are the operations in which the MKW bialgebra compatibility Δ_N(ω₁ ⧢ ω₂) = Δ_N(ω₁) ⊔⊔ Δ_N(ω₂) is stated.

Main definitions

• PlanarForest.pairShuffle - shuffle both tensor factors of two term lists
• PlanarForest.graftTail - the tail operation of the coproduct recursion

def HopfAlgebras.PlanarForest.pairShuffle (xs ys : List (PlanarForest × PlanarForest)) : List (PlanarForest × PlanarForest)

The pairwise-shuffle product of two coproduct term lists: shuffle the pruned factors and the remaining factors of every pair of terms (the operation ⊔⊔ of arXiv:math/0603023).

Equations

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

def HopfAlgebras.PlanarForest.graftTail (xs : List (PlanarForest × PlanarForest)) (t : PTree) : List (PlanarForest × PlanarForest)

The tail operation of the MKW coproduct recursion: ⊔·(I ⊗ B⁺)Δ_N(B⁻ τ) applied to a term list.

Equations

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

theorem HopfAlgebras.PlanarForest.mkwTerms_concat_graftTail (ω : PlanarForest) (t : PTree) : (ω ++ [t]).mkwTerms = (ω ++ [t], []) :: graftTail ω.mkwTerms t

The MKW coproduct recursion in terms of the grafting tail.

@[simp]

theorem HopfAlgebras.PlanarForest.pairShuffle_nil_left (ys : List (PlanarForest × PlanarForest)) : pairShuffle [] ys = []

@[simp]

theorem HopfAlgebras.PlanarForest.pairShuffle_nil_right (xs : List (PlanarForest × PlanarForest)) : pairShuffle xs [] = []

@[simp]

theorem HopfAlgebras.PlanarForest.pairShuffle_unit_left (ys : List (PlanarForest × PlanarForest)) : pairShuffle [([], [])] ys = ys

The empty-cut singleton is a left unit for the pairwise shuffle.

@[simp]

theorem HopfAlgebras.PlanarForest.pairShuffle_unit_right (xs : List (PlanarForest × PlanarForest)) : pairShuffle xs [([], [])] = xs

The empty-cut singleton is a right unit for the pairwise shuffle.

@[simp]

theorem HopfAlgebras.PlanarForest.graftTail_nil (t : PTree) : graftTail [] t = []

theorem HopfAlgebras.PlanarForest.graftTail_append (xs ys : List (PlanarForest × PlanarForest)) (t : PTree) : graftTail (xs ++ ys) t = graftTail xs t ++ graftTail ys t

theorem HopfAlgebras.PlanarForest.graftTail_perm {xs ys : List (PlanarForest × PlanarForest)} (h : xs.Perm ys) (t : PTree) : (graftTail xs t).Perm (graftTail ys t)

theorem HopfAlgebras.PlanarForest.pairShuffle_cons_left (x : PlanarForest × PlanarForest) (xs ys : List (PlanarForest × PlanarForest)) : pairShuffle (x :: xs) ys = List.flatMap (fun (t₂ : PlanarForest × PlanarForest) => List.flatMap (fun (p : List PlanarTree) => List.map (fun (r : List PlanarTree) => (p, r)) (Word.shuffle x.2 t₂.2)) (Word.shuffle x.1 t₂.1)) ys ++ pairShuffle xs ys

theorem HopfAlgebras.PlanarForest.pairShuffle_append_left (xs xs' ys : List (PlanarForest × PlanarForest)) : pairShuffle (xs ++ xs') ys = pairShuffle xs ys ++ pairShuffle xs' ys

theorem HopfAlgebras.PlanarForest.pairShuffle_cons_right_perm (xs : List (PlanarForest × PlanarForest)) (y : PlanarForest × PlanarForest) (ys : List (PlanarForest × PlanarForest)) : (pairShuffle xs (y :: ys)).Perm (List.flatMap (fun (t₁ : PlanarForest × PlanarForest) => List.flatMap (fun (p : List PlanarTree) => List.map (fun (r : List PlanarTree) => (p, r)) (Word.shuffle t₁.2 y.2)) (Word.shuffle t₁.1 y.1)) xs ++ pairShuffle xs ys)

Splitting the second argument of the pairwise shuffle, up to permutation.

theorem HopfAlgebras.PlanarForest.shuffle_flatMap_mkwTerms_perm (ω₁ ω₂ : PlanarForest) : (List.flatMap mkwTerms (Word.shuffle ω₁ ω₂)).Perm (pairShuffle ω₁.mkwTerms ω₂.mkwTerms)

The MKW bialgebra compatibility at the level of coproduct terms: Δ_N(ω₁ ⧢ ω₂) = Δ_N(ω₁) ⊔⊔ Δ_N(ω₂) — the coproduct terms of all shuffles of two ordered forests are, with multiplicity, the pairwise shuffles of the coproduct terms of the factors (arXiv:math/0603023, Theorem 2).

Coassociativity of the MKW coproduct

def HopfAlgebras.PlanarForest.mkwLeftTriples (ω : PlanarForest) : List (PlanarForest × PlanarForest × PlanarForest)

The terms of the left iterated coproduct (Δ_N ⊗ I)Δ_N.

Equations

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

def HopfAlgebras.PlanarForest.mkwRightTriples (ω : PlanarForest) : List (PlanarForest × PlanarForest × PlanarForest)

The terms of the right iterated coproduct (I ⊗ Δ_N)Δ_N.

Equations

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

def HopfAlgebras.PlanarForest.tripleGraft (xs ys : List (PlanarForest × PlanarForest × PlanarForest)) : List (PlanarForest × PlanarForest × PlanarForest)

The triple analogue of the grafting product appearing in both iterated coproducts of a forest υ ++ [τ].

Equations

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

theorem HopfAlgebras.PlanarForest.mkwLeftTriples_perm_mkwRightTriples (ω : PlanarForest) : ω.mkwLeftTriples.Perm ω.mkwRightTriples

Coassociativity of the MKW coproduct at the level of coproduct terms: (Δ_N ⊗ I)Δ_N and (I ⊗ Δ_N)Δ_N produce the same triples of forests, with multiplicity (arXiv:math/0603023, Theorem 2).