The Butcher–Connes–Kreimer bialgebra as a combinatorial bialgebra

The BCK Hopf algebra of non-planar rooted forests, packaged as a CombBialg: the product is the (monomial) forest union, the coproduct the admissible-cut expansion RootedForest.coproductTerms from HopfAlgebras. Its characters — the multiplicative functionals on forests, i.e. the coefficient systems of branched rough paths and B-series — thereby inherit the abstract convolution monoid of HopfAlgebra.Basic.

All axioms are discharged from the cut-combinatorics keystones already in HopfAlgebras: coproductTerms_add_perm (bialgebra compatibility), nestedCoproductTerms_left_right_perm (coassociativity) and the series-level counit laws counitLeft_coproduct/counitRight_coproduct, paired against arbitrary coefficient functions via Finsupp.linearCombination.

theorem HopfAlgebras.BCK.counitCoeff_eq_boolIte {R : Type v} [CommSemiring R] (φ : RootedForest) : ForestAlgebra.counitCoeff φ = if decide (Multiset.card φ = 0) = true then 1 else 0

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

noncomputable def HopfAlgebras.bckBialg : CombBialg RootedForest

The BCK bialgebra of rooted forests as a combinatorial bialgebra: monomial forest-union product and admissible-cut coproduct.

Equations

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

Characters of the forest algebra vs combinatorial characters

theorem HopfAlgebras.evalForest_isCharacter {R : Type v} [CommSemiring R] (χ : ForestAlgebra.Character R) : bckBialg.IsCharacter χ.evalForest

The coefficient system of a forest-algebra character is a character of the BCK combinatorial bialgebra.

theorem HopfAlgebras.convolution_evalForest_conv {R : Type v} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (φ : RootedForest) : (χ.convolution ψ).evalForest φ = CombBialg.Character.conv χ.evalForest ψ.evalForest φ

Character convolution is the abstract BCK convolution.

noncomputable def HopfAlgebras.bckCharacter {R : Type v} [CommSemiring R] (f : RootedForest → R) (hf : bckBialg.IsCharacter f) : ForestAlgebra.Character R

Lift a character of the combinatorial BCK bialgebra to an algebra character of the forest algebra.

Equations

• HopfAlgebras.bckCharacter f hf = (AddMonoidAlgebra.lift R R HopfAlgebras.RootedForest) (HopfAlgebras.bckMonoidHom✝ f hf)

@[simp]

theorem HopfAlgebras.evalForest_bckCharacter {R : Type v} [CommSemiring R] (f : RootedForest → R) (hf : bckBialg.IsCharacter f) (φ : RootedForest) : (bckCharacter f hf).evalForest φ = f φ