The Munthe-Kaas-Wright Coproduct

This file defines the coproduct of the Munthe-Kaas-Wright Hopf algebra of ordered forests of planar rooted trees, following the recursion of Munthe-Kaas & Wright, On the Hopf algebraic structure of Lie group integrators (Found. Comput. Math. 8, 2008; arXiv:math/0603023), Definition 3:

Δ_N(𝟙) = 𝟙 ⊗ 𝟙, Δ_N(ω τ) = ω τ ⊗ 𝟙 + Δ_N(ω) ⊔·(I ⊗ B⁺)Δ_N(B⁻(τ)),

where τ is the last tree of the forest and ⊔· shuffles the left tensor factors and concatenates the right tensor factors. The terms of the coproduct enumerate the full admissible left cuts of the ordered forest.

Main definitions

• PlanarForest.mkwTerms - the list of coproduct terms, with multiplicity
• PlanarTensorAlgebra - tensor-coded ordered forest algebra
• PlanarForest.mkwCoproduct - the MKW coproduct
• PlanarForest.counitLeft_mkwCoproduct and PlanarForest.counitRight_mkwCoproduct - the counit laws
• PlanarForest.orderList_fst_add_snd_of_mem_mkwTerms - the order grading

The small-order values are verified against the coproduct table of the paper; in particular Δ_N(•χ) reproduces the illustrative example of Section 2 with its multiplicity 2 term, and the cherry shows the left-admissibility constraint (the right branch alone is never pruned, unlike in the Butcher-Connes-Kreimer coproduct).

@[irreducible]

def HopfAlgebras.PlanarForest.mkwTermsAux : List PTree → List (PlanarForest × PlanarForest)

MKW coproduct terms of the ordered forest whose reversed tree list is the input. The recursion peels the last tree τ = B⁺(τ.children) of the forest, following arXiv:math/0603023, Definition 3.

Equations

• One or more equations did not get rendered due to their size.
• HopfAlgebras.PlanarForest.mkwTermsAux [] = [([], [])]

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

The list of MKW coproduct terms of an ordered forest, with multiplicity. Each term is a pair (pruned, remaining) corresponding to one full admissible left cut of the forest.

Equations

• ω.mkwTerms = HopfAlgebras.PlanarForest.mkwTermsAux (List.reverse ω)

@[simp]

theorem HopfAlgebras.PlanarForest.mkwTerms_nil : mkwTerms [] = [([], [])]

theorem HopfAlgebras.PlanarForest.mkwTerms_concat (ω : PlanarForest) (t : PTree) : (ω ++ [t]).mkwTerms = (ω ++ [t], []) :: List.flatMap (fun (pr₁ : PlanarForest × PlanarForest) => List.flatMap (fun (pr₂ : PlanarForest × PlanarForest) => List.map (fun (s : PlanarForest) => (s, pr₁.2 ++ [PTree.node pr₂.2])) (Word.shuffle pr₁.1 pr₂.1)) (mkwTerms t.children)) ω.mkwTerms

The defining recursion of the MKW coproduct terms, peeling the last tree.

theorem HopfAlgebras.PlanarForest.concatChildrenInduction {motive : PlanarForest → Prop} (ω : PlanarForest) (nil : motive []) (concat : ∀ (ω : PlanarForest) (t : PTree), motive ω → motive t.children → motive (ω ++ [t])) : motive ω

Induction along the MKW recursion: the empty forest, and appending one tree whose children forest satisfies the motive.

theorem HopfAlgebras.PlanarForest.self_nil_mem_mkwTerms (ω : PlanarForest) : (ω, []) ∈ ω.mkwTerms

The full cut, pruning the whole forest, is always a coproduct term.

theorem HopfAlgebras.PlanarForest.nil_self_mem_mkwTerms (ω : PlanarForest) : ([], ω) ∈ ω.mkwTerms

The empty cut, pruning nothing, is always a coproduct term.

theorem HopfAlgebras.PlanarForest.mkwTerms_eq_self_nil_cons (ω : PlanarForest) : ω.mkwTerms = (ω, []) :: ω.mkwTerms.tail

The first MKW coproduct term is always the full cut ω ⊗ 𝟙.

theorem HopfAlgebras.PlanarForest.snd_ne_nil_of_mem_tail_mkwTerms {ω : PlanarForest} {pr : PlanarForest × PlanarForest} (hω : ω ≠ []) (hpr : pr ∈ ω.mkwTerms.tail) : pr.2 ≠ []

Every MKW coproduct term other than the full cut has a nonempty remaining part.

theorem HopfAlgebras.PlanarForest.orderList_fst_add_snd_of_mem_mkwTerms (ω : PlanarForest) (pr : PlanarForest × PlanarForest) : pr ∈ ω.mkwTerms → PTree.orderList pr.1 + PTree.orderList pr.2 = PTree.orderList ω

The MKW coproduct respects the grading by total order of forests.

theorem HopfAlgebras.PlanarForest.orderList_fst_lt_of_mem_tail_mkwTerms {ω : PlanarForest} {pr : PlanarForest × PlanarForest} (hω : ω ≠ []) (hpr : pr ∈ ω.mkwTerms.tail) : PTree.orderList pr.1 < PTree.orderList ω

Every MKW coproduct term other than the full cut prunes strictly fewer vertices than the whole forest. This justifies the recursive definition of the antipode.

theorem HopfAlgebras.PlanarForest.sum_map_counitCoeff_fst_smul_mkwTerms {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (ω : PlanarForest) (g : PlanarForest → M) : (List.map (fun (pr : PlanarForest × PlanarForest) => PlanarForestAlgebra.counitCoeff pr.1 • g pr.2) ω.mkwTerms).sum = g ω

Applying the counit to the pruned factor of every MKW coproduct term recovers the forest: the only term with empty pruned part is the empty cut 𝟙 ⊗ ω. The statement is generalized over an arbitrary module-valued weight g of the remaining factor so that it can serve as its own induction hypothesis.

theorem HopfAlgebras.PlanarForest.sum_map_counitCoeff_snd_smul_mkwTerms {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] (ω : PlanarForest) (g : PlanarForest → M) : (List.map (fun (pr : PlanarForest × PlanarForest) => PlanarForestAlgebra.counitCoeff pr.2 • g pr.1) ω.mkwTerms).sum = g ω

Applying the counit to the remaining factor of every MKW coproduct term recovers the forest: the only term with empty remaining part is the full cut ω ⊗ 𝟙.

@[reducible, inline]

abbrev HopfAlgebras.PlanarTensorAlgebra (R : Type u) [Semiring R] : Type u

Tensor-coded ordered forest algebra: (φ, ψ) represents φ ⊗ ψ.

Equations

• HopfAlgebras.PlanarTensorAlgebra R = MonoidAlgebra R (HopfAlgebras.PlanarForest × HopfAlgebras.PlanarForest)

noncomputable def HopfAlgebras.PlanarTensorAlgebra.ofPair {R : Type u} [Semiring R] (term : PlanarForest × PlanarForest) : PlanarTensorAlgebra R

The basis tensor φ ⊗ ψ represented by a pair of ordered forests.

Equations

• HopfAlgebras.PlanarTensorAlgebra.ofPair term = MonoidAlgebra.single term 1

@[simp]

theorem HopfAlgebras.PlanarTensorAlgebra.ofPair_nil_nil {R : Type u} [Semiring R] : ofPair ([], []) = 1

@[simp]

theorem HopfAlgebras.PlanarTensorAlgebra.ofPair_mul {R : Type u} [Semiring R] (x y : PlanarForest × PlanarForest) : ofPair (x.1 ++ y.1, x.2 ++ y.2) = ofPair x * ofPair y

noncomputable def HopfAlgebras.PlanarTensorAlgebra.sumTerms {R : Type u} [Semiring R] (terms : List (PlanarForest × PlanarForest)) : PlanarTensorAlgebra R

Sum a finite list of basis tensors. Duplicates contribute multiplicity.

Equations

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

@[simp]

theorem HopfAlgebras.PlanarTensorAlgebra.sumTerms_nil {R : Type u} [Semiring R] : sumTerms [] = 0

@[simp]

theorem HopfAlgebras.PlanarTensorAlgebra.sumTerms_cons {R : Type u} [Semiring R] (term : PlanarForest × PlanarForest) (terms : List (PlanarForest × PlanarForest)) : sumTerms (term :: terms) = ofPair term + sumTerms terms

@[simp]

theorem HopfAlgebras.PlanarTensorAlgebra.sumTerms_singleton {R : Type u} [Semiring R] (term : PlanarForest × PlanarForest) : sumTerms [term] = ofPair term

theorem HopfAlgebras.PlanarTensorAlgebra.sumTerms_append {R : Type u} [Semiring R] (xs ys : List (PlanarForest × PlanarForest)) : sumTerms (xs ++ ys) = sumTerms xs + sumTerms ys

noncomputable def HopfAlgebras.PlanarTensorAlgebra.counitLeft {R : Type u} [CommSemiring R] : PlanarTensorAlgebra R →ₐ[R] PlanarForestAlgebra R

Apply the counit to the left tensor factor.

Equations

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

@[simp]

theorem HopfAlgebras.PlanarTensorAlgebra.counitLeft_ofPair {R : Type u} [CommSemiring R] (term : PlanarForest × PlanarForest) : counitLeft (ofPair term) = PlanarForestAlgebra.counitCoeff term.1 • PlanarForestAlgebra.ofForest term.2

theorem HopfAlgebras.PlanarTensorAlgebra.counitLeft_sumTerms {R : Type u} [CommSemiring R] (terms : List (PlanarForest × PlanarForest)) : counitLeft (sumTerms terms) = (List.map (fun (term : PlanarForest × PlanarForest) => PlanarForestAlgebra.counitCoeff term.1 • PlanarForestAlgebra.ofForest term.2) terms).sum

noncomputable def HopfAlgebras.PlanarTensorAlgebra.counitRight {R : Type u} [CommSemiring R] : PlanarTensorAlgebra R →ₐ[R] PlanarForestAlgebra R

Apply the counit to the right tensor factor.

Equations

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

@[simp]

theorem HopfAlgebras.PlanarTensorAlgebra.counitRight_ofPair {R : Type u} [CommSemiring R] (term : PlanarForest × PlanarForest) : counitRight (ofPair term) = PlanarForestAlgebra.counitCoeff term.2 • PlanarForestAlgebra.ofForest term.1

theorem HopfAlgebras.PlanarTensorAlgebra.counitRight_sumTerms {R : Type u} [CommSemiring R] (terms : List (PlanarForest × PlanarForest)) : counitRight (sumTerms terms) = (List.map (fun (term : PlanarForest × PlanarForest) => PlanarForestAlgebra.counitCoeff term.2 • PlanarForestAlgebra.ofForest term.1) terms).sum

noncomputable def HopfAlgebras.PlanarForest.mkwCoproduct {R : Type u} [Semiring R] (ω : PlanarForest) : PlanarTensorAlgebra R

The MKW coproduct of an ordered forest, in the tensor-coded algebra. Munthe-Kaas & Wright, arXiv:math/0603023, Definition 3.

Equations

• ω.mkwCoproduct = HopfAlgebras.PlanarTensorAlgebra.sumTerms ω.mkwTerms

@[simp]

theorem HopfAlgebras.PlanarForest.mkwCoproduct_nil {R : Type u} [Semiring R] : mkwCoproduct [] = 1

theorem HopfAlgebras.PlanarForest.counitLeft_mkwCoproduct {R : Type u} [CommSemiring R] (ω : PlanarForest) : PlanarTensorAlgebra.counitLeft ω.mkwCoproduct = PlanarForestAlgebra.ofForest ω

The left counit law of the MKW coproduct: (e ⊗ I)Δ_N = I.

theorem HopfAlgebras.PlanarForest.counitRight_mkwCoproduct {R : Type u} [CommSemiring R] (ω : PlanarForest) : PlanarTensorAlgebra.counitRight ω.mkwCoproduct = PlanarForestAlgebra.ofForest ω

The right counit law of the MKW coproduct: (I ⊗ e)Δ_N = I.

Small-order verification against arXiv:math/0603023

The coproduct terms for all ordered forests of order at most three, and the paper's illustrative example Δ_N(•χ) with its multiplicity 2 term. The cherry demonstrates left-admissibility: only the left branch may be pruned on its own, so • ⊗ χ appears with coefficient 1 rather than 2 as it would in the Butcher-Connes-Kreimer coproduct.

theorem HopfAlgebras.PlanarForest.mkwTerms_bullet_forest : mkwTerms [PTree.bullet] = [([PTree.bullet], []), ([], [PTree.bullet])]

theorem HopfAlgebras.PlanarForest.mkwTerms_chain2_forest : mkwTerms [PTree.chain2] = [([PTree.chain2], []), ([PTree.bullet], [PTree.bullet]), ([], [PTree.chain2])]

theorem HopfAlgebras.PlanarForest.mkwTerms_bullet_bullet_forest : mkwTerms [PTree.bullet, PTree.bullet] = [([PTree.bullet, PTree.bullet], []), ([PTree.bullet], [PTree.bullet]), ([], [PTree.bullet, PTree.bullet])]

theorem HopfAlgebras.PlanarForest.mkwTerms_chain3_forest : mkwTerms [PTree.chain3] = [([PTree.chain3], []), ([PTree.chain2], [PTree.bullet]), ([PTree.bullet], [PTree.chain2]), ([], [PTree.chain3])]

theorem HopfAlgebras.PlanarForest.mkwTerms_cherry_forest : mkwTerms [PTree.cherry] = [([PTree.cherry], []), ([PTree.bullet, PTree.bullet], [PTree.bullet]), ([PTree.bullet], [PTree.chain2]), ([], [PTree.cherry])]

Only the left branch of the cherry may be pruned on its own.

theorem HopfAlgebras.PlanarForest.mkwTerms_bullet_chain2_forest : mkwTerms [PTree.bullet, PTree.chain2] = [([PTree.bullet, PTree.chain2], []), ([PTree.bullet, PTree.bullet], [PTree.bullet]), ([PTree.bullet, PTree.bullet], [PTree.bullet]), ([PTree.bullet], [PTree.chain2]), ([PTree.bullet], [PTree.bullet, PTree.bullet]), ([], [PTree.bullet, PTree.chain2])]

The illustrative example of arXiv:math/0603023, Section 2: Δ_N(•χ) = •χ ⊗ 𝟙 + 2 (•• ⊗ •) + • ⊗ χ + • ⊗ •• + 𝟙 ⊗ •χ, where χ is the two-vertex chain.

theorem HopfAlgebras.PlanarForest.mkwCoproduct_bullet_forest {R : Type u} [Semiring R] : mkwCoproduct [PTree.bullet] = PlanarTensorAlgebra.ofPair ([PTree.bullet], []) + PlanarTensorAlgebra.ofPair ([], [PTree.bullet])

The one-vertex forest is primitive for the MKW coproduct.