Word-level antipode combinatorics

The combinatorial content of the shuffle antipode S(w) = (-1)^{|w|}wʳ: shuffles of reversed words (shuffle_reverse_perm) and the telescoping antipode identity (antipode_convolution) — the signed sum of the shuffles of reversed prefixes with suffixes over all deconcatenation splits of a nonempty word vanishes, i.e. m ∘ (S ⊗ id) ∘ Δ = η ∘ ε paired against arbitrary coefficients. These feed both the abstract word Hopf algebra (HopfAlgebras.Combinatorial.Shuffle) and the signature antipode in RoughPaths.

theorem HopfAlgebras.Word.shuffle_reverse_perm {α : Type u} (u v : List α) : (List.map List.reverse (shuffle u v)).Perm (shuffle u.reverse v.reverse)

Reversal is a shuffle morphism: the reversals of the shuffles of u and v are the shuffles of uʳ and vʳ, up to permutation.

theorem HopfAlgebras.Word.antipode_convolution {α : Type u} {R : Type v} [CommRing R] (f : List α → R) (c : α) (t : List α) : (List.map (fun (pq : List α × List α) => (-1) ^ pq.1.length * (List.map f (shuffle pq.1.reverse pq.2)).sum) (splits (c :: t))).sum = 0

The antipode identity: the signed sum of the shuffles of the reversed prefixes with the suffixes, over all deconcatenation splits of a nonempty word, vanishes — m ∘ (S ⊗ id) ∘ Δ = η ∘ ε for the shuffle Hopf algebra, paired against arbitrary coefficients.