The word shuffle Hopf algebra

The combinatorial Hopf algebra of words over an alphabet α: shuffle product, deconcatenation coproduct, and the signed-reversal antipode S(w) = (-1)^{|w|}·wʳ. Its characters with values in R are exactly the group-like signature series — the signatures of rough path theory (see RoughPaths.Signature.Character for the identification) — and the abstract character-group theory of HopfAlgebras.Combinatorial.Basic yields their monoid and group structure.

All axioms are discharged from the word-combinatorics keystones already in the library: shuffle_splits_perm (bialgebra compatibility), leftSplits3_perm_rightSplits3 (coassociativity), antipode_convolution and shuffle_reverse_perm (the antipode identities).

theorem HopfAlgebras.Word.sign_eq (n : ℕ) {R : Type v} [CommRing R] : (if decide (n % 2 = 0) = true then 1 else -1) = (-1) ^ n

The sign of the shuffle antipode as a Boolean.

noncomputable def HopfAlgebras.wordHopf (α : Type u) : CombHopf (List α)

The word shuffle Hopf algebra: shuffle product, deconcatenation coproduct, signed-reversal antipode. Its characters are the signatures.

Equations

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