Documentation

HopfAlgebras.Hopf.MKWAntipode

The Munthe-Kaas-Wright Antipode #

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

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

where μ_N is the shuffle product of ordered forests. The argument of S_N ⊗ I consists of all MKW coproduct terms except the full cut ωτ ⊗ 𝟙, and every such term prunes strictly fewer vertices, so the recursion is well-founded by forest order.

Main definitions #

The antipode is verified on forests of order at most two.

source
noncomputable def HopfAlgebras.PlanarForestAlgebra.shuffleOf {R : Type u} [Semiring R] (ts us : PlanarForest) :
PlanarForestAlgebra R

The shuffle product of two ordered forests in the ordered forest algebra. This is the product μ_N of the MKW Hopf algebra.

Equations
Instances For
    source
    @[simp]
    theorem HopfAlgebras.PlanarForestAlgebra.shuffleOf_nil_left {R : Type u} [Semiring R] (us : PlanarForest) :
    shuffleOf [] us = ofForest us
    source
    @[simp]
    theorem HopfAlgebras.PlanarForestAlgebra.shuffleOf_nil_right {R : Type u} [Semiring R] (ts : PlanarForest) :
    shuffleOf ts [] = ofForest ts
    source
    theorem HopfAlgebras.PlanarForestAlgebra.shuffleOf_singleton_singleton {R : Type u} [Semiring R] (t u : PTree) :
    shuffleOf [t] [u] = ofForest [t, u] + ofForest [u, t]
    source
    noncomputable def HopfAlgebras.PlanarForestAlgebra.shuffleRight {R : Type u} [Semiring R] (x : PlanarForestAlgebra R) (us : PlanarForest) :
    PlanarForestAlgebra R

    Shuffle a general element of the ordered forest algebra with a fixed ordered forest on the right.

    Equations
    Instances For
      source
      @[simp]
      theorem HopfAlgebras.PlanarForestAlgebra.shuffleRight_zero_left {R : Type u} [Semiring R] (us : PlanarForest) :
      shuffleRight 0 us = 0
      source
      theorem HopfAlgebras.PlanarForestAlgebra.shuffleRight_single_left {R : Type u} [Semiring R] (ts : PlanarForest) (a : R) (us : PlanarForest) :
      shuffleRight (MonoidAlgebra.single ts a) us = a • shuffleOf ts us
      source
      @[simp]
      theorem HopfAlgebras.PlanarForestAlgebra.shuffleRight_ofForest_left {R : Type u} [Semiring R] (ts us : PlanarForest) :
      (ofForest ts).shuffleRight us = shuffleOf ts us
      source
      @[simp]
      theorem HopfAlgebras.PlanarForestAlgebra.shuffleRight_one_left {R : Type u} [Semiring R] (us : PlanarForest) :
      shuffleRight 1 us = ofForest us
      source
      theorem HopfAlgebras.PlanarForestAlgebra.shuffleRight_add_left {R : Type u} [Semiring R] (x y : PlanarForestAlgebra R) (us : PlanarForest) :
      (x + y).shuffleRight us = x.shuffleRight us + y.shuffleRight us
      source
      theorem HopfAlgebras.PlanarForestAlgebra.shuffleRight_neg_left {R : Type u} [Ring R] (x : PlanarForestAlgebra R) (us : PlanarForest) :
      (-x).shuffleRight us = -x.shuffleRight us
      source
      @[simp]
      theorem HopfAlgebras.PlanarForestAlgebra.shuffleRight_nil_right {R : Type u} [Semiring R] (x : PlanarForestAlgebra R) :
      x.shuffleRight [] = x

      Shuffling with the empty forest on the right is the identity.

      source
      @[irreducible]
      def HopfAlgebras.PlanarForest.mkwAntipode {R : Type u} [Ring R] (ω : PlanarForest) :
      PlanarForestAlgebra R

      The MKW antipode of an ordered forest, by the recursion of arXiv:math/0603023, Theorem 2: minus the shuffle products S_N(p) ⧢ r over all MKW coproduct terms (p, r) except the full cut.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem HopfAlgebras.PlanarForest.mkwAntipode_nil {R : Type u} [Ring R] :
        mkwAntipode [] = 1
        source
        theorem HopfAlgebras.PlanarForest.mkwAntipode_of_ne_nil {R : Type u} [Ring R] {ω : PlanarForest} (hω : ω ≠ []) :
        ω.mkwAntipode = -(List.map (fun (pr : PlanarForest × PlanarForest) => pr.1.mkwAntipode.shuffleRight pr.2) ω.mkwTerms.tail).sum

        The defining recursion of the MKW antipode on a nonempty forest.

        source
        theorem HopfAlgebras.PlanarForest.sum_shuffleRight_mkwAntipode_mkwTerms {R : Type u} [Ring R] (ω : PlanarForest) :
        (List.map (fun (pr : PlanarForest × PlanarForest) => pr.1.mkwAntipode.shuffleRight pr.2) ω.mkwTerms).sum = PlanarForestAlgebra.counitCoeff ω • 1

        The left antipode identity μ_N(S_N ⊗ I)Δ_N = u_N ∘ e_N of the MKW Hopf algebra (arXiv:math/0603023, Theorem 2), evaluated on an ordered forest.

        Small-order verification against arXiv:math/0603023 #

        S_N(•) = -• and S_N(χ) = • ⧢ • - χ = 2(••) - χ for the two-vertex chain χ.

        source
        theorem HopfAlgebras.PlanarForest.mkwAntipode_bullet_forest {R : Type u} [Ring R] :
        mkwAntipode [PTree.bullet] = -PlanarForestAlgebra.ofForest [PTree.bullet]
        source
        theorem HopfAlgebras.PlanarForest.mkwAntipode_chain2_forest {R : Type u} [Ring R] :
        mkwAntipode [PTree.chain2] = PlanarForestAlgebra.ofForest [PTree.bullet, PTree.bullet] + PlanarForestAlgebra.ofForest [PTree.bullet, PTree.bullet] - PlanarForestAlgebra.ofForest [PTree.chain2]