The labelled Butcher–Connes–Kreimer bialgebra as a combinatorial bialgebra

The labelled BCK Hopf algebra of decorated non-planar rooted forests, packaged as a CombBialg, mirroring HopfAlgebras.Combinatorial.BCK: monomial forest-union product, admissible-cut coproduct LRootedForest.coproductTerms. Characters of the labelled forest algebra correspond to combinatorial characters via the AddMonoidAlgebra.lift bridge lbckCharacter / evalForest_lbckIsCharacter.

theorem HopfAlgebras.LBCK.counitCoeff_eq_boolIte {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : LForestAlgebra.counitCoeff φ = if decide (Multiset.card φ = 0) = true then 1 else 0

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

noncomputable def HopfAlgebras.lbckBialg (α : Type u) : CombBialg (LRootedForest α)

The labelled BCK bialgebra of decorated 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 labelled forest algebra vs combinatorial

characters

theorem HopfAlgebras.evalForest_lbckIsCharacter {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) : (lbckBialg α).IsCharacter χ.evalForest

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

theorem HopfAlgebras.convolution_evalForest_lconv {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (φ : LRootedForest α) : (χ.convolution ψ).evalForest φ = CombBialg.Character.conv χ.evalForest ψ.evalForest φ

Labelled character convolution is the abstract convolution.

noncomputable def HopfAlgebras.lbckCharacter {α : Type u} {R : Type v} [CommSemiring R] (f : LRootedForest α → R) (hf : (lbckBialg α).IsCharacter f) : LForestAlgebra.Character α R

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

Equations

• HopfAlgebras.lbckCharacter f hf = (AddMonoidAlgebra.lift R R (HopfAlgebras.LRootedForest α)) (HopfAlgebras.lbckMonoidHom✝ f hf)

@[simp]

theorem HopfAlgebras.evalForest_lbckCharacter {α : Type u} {R : Type v} [CommSemiring R] (f : LRootedForest α → R) (hf : (lbckBialg α).IsCharacter f) (φ : LRootedForest α) : (lbckCharacter f hf).evalForest φ = f φ