The Munthe-Kaas–Wright bialgebra as a combinatorial bialgebra

The MKW Hopf algebra of ordered (planar) rooted forests, packaged as a CombBialg: the product is the shuffle of forests, the coproduct the MKW expansion PlanarForest.mkwTerms from HopfAlgebras. Its characters — the shuffle-multiplicative functionals on ordered forests, i.e. the Lie–Butcher series and the coefficient systems of planarly branched rough paths — inherit the abstract convolution monoid of HopfAlgebra.Basic, which coincides with the Grossman–Larson convolution PlanarForest.mkwConvolution.

All axioms are discharged from the keystones in HopfAlgebras: shuffle_flatMap_mkwTerms_perm (bialgebra compatibility), mkwLeftTriples_perm_mkwRightTriples via mkwConvolution_assoc (coassociativity), and mkwConvolution_counit_left/_right.

theorem HopfAlgebras.MKW.counitCoeff_eq_boolIte {R : Type v} [CommSemiring R] (ts : PlanarForest) : PlanarForestAlgebra.counitCoeff ts = if List.isEmpty ts = true then 1 else 0

The planar counit coefficient as a Boolean if-then-else.

noncomputable def HopfAlgebras.mkwBialg : CombBialg PlanarForest

The MKW bialgebra of ordered forests as a combinatorial bialgebra: shuffle product and MKW (Grossman–Larson-dual) coproduct.

Equations

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

theorem HopfAlgebras.isShuffleCharacter_iff_isCharacter {R : Type v} [CommSemiring R] (f : PlanarForest → R) : PlanarForest.IsShuffleCharacter f ↔ mkwBialg.IsCharacter f

Shuffle characters on ordered forests are exactly the characters of the MKW combinatorial bialgebra.

theorem HopfAlgebras.mkwConvolution_eq_conv {R : Type v} [CommSemiring R] (f g : PlanarForest → R) : PlanarForest.mkwConvolution f g = CombBialg.Character.conv f g

The Grossman–Larson convolution is the abstract MKW convolution — definitionally.