The Dual of the MKW Hopf Algebra: the Grossman-Larson Convolution

This file defines the convolution product on linear functionals of ordered forests induced by the MKW coproduct,

(α ∘ β)(ω) = ⟨α ⊗ β, Δ_N(ω)⟩ = Σ_{cuts} α(P^c(ω)) β(R^c(ω)),

which by arXiv:math/0603023 (Section 3) is the Grossman-Larson product on the graded dual of H_N. Associativity follows from coassociativity of Δ_N, the unit laws from the counit laws, and the shuffle-multiplicative functionals (the exponential Lie-Butcher series) are closed under the product by the bialgebra law — the character group of Lie group integrators.

Main definitions

• PlanarForest.mkwConvolution - the Grossman-Larson convolution
• PlanarForest.mkwConvolution_assoc - associativity, from coassociativity
• PlanarForest.IsShuffleCharacter - shuffle-multiplicative functionals
• PlanarForest.IsShuffleCharacter.mkwConvolution - the character group is closed under the Grossman-Larson convolution

def HopfAlgebras.PlanarForest.mkwConvolution {R : Type u} [Semiring R] (f g : PlanarForest → R) (ω : PlanarForest) : R

The Grossman-Larson convolution of two functionals on ordered forests, dual to the MKW coproduct (arXiv:math/0603023, Section 3).

Equations

• HopfAlgebras.PlanarForest.mkwConvolution f g ω = (List.map (fun (pr : HopfAlgebras.PlanarForest × HopfAlgebras.PlanarForest) => f pr.1 * g pr.2) ω.mkwTerms).sum

@[simp]

theorem HopfAlgebras.PlanarForest.mkwConvolution_nil {R : Type u} [Semiring R] (f g : PlanarForest → R) : mkwConvolution f g [] = f [] * g []

theorem HopfAlgebras.PlanarForest.mkwConvolution_counit_left {R : Type u} [CommSemiring R] (g : PlanarForest → R) (ω : PlanarForest) : mkwConvolution PlanarForestAlgebra.counitCoeff g ω = g ω

The counit is a left unit for the Grossman-Larson convolution.

theorem HopfAlgebras.PlanarForest.mkwConvolution_counit_right {R : Type u} [CommSemiring R] (f : PlanarForest → R) (ω : PlanarForest) : mkwConvolution f PlanarForestAlgebra.counitCoeff ω = f ω

The counit is a right unit for the Grossman-Larson convolution.

theorem HopfAlgebras.PlanarForest.mkwConvolution_assoc {R : Type u} [CommSemiring R] (f g h : PlanarForest → R) (ω : PlanarForest) : mkwConvolution (mkwConvolution f g) h ω = mkwConvolution f (mkwConvolution g h) ω

Associativity of the Grossman-Larson convolution, dual to coassociativity of the MKW coproduct.

def HopfAlgebras.PlanarForest.IsShuffleCharacter {R : Type u} [Semiring R] (f : PlanarForest → R) : Prop

A functional on ordered forests is a shuffle character if it is normalized and multiplicative for the shuffle product: these are the exponential Lie-Butcher series of arXiv:math/0603023, Lemma 2.

Equations

• HopfAlgebras.PlanarForest.IsShuffleCharacter f = (f [] = 1 ∧ ∀ (ω₁ ω₂ : HopfAlgebras.PlanarForest), (List.map f (HopfAlgebras.Word.shuffle ω₁ ω₂)).sum = f ω₁ * f ω₂)

theorem HopfAlgebras.PlanarForest.IsShuffleCharacter.mkwConvolution {R : Type u} [CommSemiring R] {f g : PlanarForest → R} (hf : IsShuffleCharacter f) (hg : IsShuffleCharacter g) : IsShuffleCharacter (PlanarForest.mkwConvolution f g)

The Grossman-Larson convolution of shuffle characters is a shuffle character: Lie group integrators form a group under composition (arXiv:math/0603023, Section 3).