The shuffle antipode and the group of signatures

The words over α form the shuffle Hopf algebra: shuffle product, deconcatenation coproduct, and antipode S(w) = (-1)^{|w|}·wʳ. A group-like signature series (IsGroupLike) is precisely a character of this Hopf algebra, and the characters of a Hopf algebra form a group under convolution — here, the tensor (concatenation) product — with inverse given by precomposition with the antipode:

a⁻¹(w) = (-1)^{|w|} · a(w.reverse) (Word.antipode).

This file proves the two facts that make this work and upgrades the bundled Signature α R from a monoid to a group:

• Word.shuffle_reverse_perm — reversal is a shuffle-algebra morphism ((u ⧢ v)ʳ ∼ uʳ ⧢ vʳ), whence characters are closed under the antipode (IsGroupLike.antipode);
• antipode_convolution — the defining identity of the antipode, Σ_{uv=w} (-1)^{|u|}·(uʳ ⧢ v) = 0 for w ≠ [], by a telescoping induction along the deconcatenation splits;
• Signature.instGroup — the group instance, over a commutative ring;
• Signature.inv_ofPiecewiseLinear — the group inverse of a piecewise-linear signature is the signature of the reversed path.

References

• C. Reutenauer, Free Lie Algebras, §1.5
• P. Friz, M. Hairer, A Course on Rough Paths, Ch. 2

The antipode of a signature series

def RoughPaths.Word.antipode {α : Type u} {R : Type v} [Ring R] (a : List α → R) : List α → R

The shuffle antipode of a signature series: a ↦ (w ↦ (-1)^{|w|}·a(wʳ)). For a character (group-like series) this is the convolution inverse — for the signature of a path, the signature of the time-reversed path.

Equations

• RoughPaths.Word.antipode a w = (-1) ^ w.length * a w.reverse

@[simp]

theorem RoughPaths.Word.antipode_coeff {α : Type u} {R : Type v} [Ring R] (a : List α → R) (w : List α) : coeff (antipode a) w = (-1) ^ w.length * coeff a w.reverse

theorem RoughPaths.Word.IsGroupLike.antipode {α : Type u} {R : Type v} [CommRing R] {a : List α → R} (ha : IsGroupLike a) : IsGroupLike (Word.antipode a)

Characters are closed under the antipode: the antipode of a group-like series is group-like. The content is that reversal is a morphism of the (commutative) shuffle algebra.

theorem RoughPaths.Word.IsGroupLike.antipode_tensorProduct {α : Type u} {R : Type v} [CommRing R] {a : List α → R} (ha : IsGroupLike a) : Word.tensorProduct (Word.antipode a) a = unit α R

The antipode is a left convolution inverse on characters: S(a) ⊗ a = 1 for group-like a.

theorem RoughPaths.Signature.inv_val {α : Type u} {R : Type v} [CommRing R] (σ : Signature α R) : ↑σ⁻¹ = Word.antipode ↑σ

The underlying series of the group inverse is the shuffle antipode σ⁻¹(w) = (-1)^{|w|}·σ(wʳ).

@[simp]

theorem RoughPaths.Signature.inv_coeff {α : Type u} {R : Type v} [CommRing R] (σ : Signature α R) (w : List α) : σ⁻¹.coeff w = (-1) ^ w.length * σ.coeff w.reverse

theorem RoughPaths.Word.IsGroupLike.tensorProduct_antipode {α : Type u} {R : Type v} [CommRing R] {a : List α → R} (ha : IsGroupLike a) : Word.tensorProduct a (Word.antipode a) = unit α R

The antipode is a two-sided inverse on characters: a ⊗ S(a) = 1 for group-like a (from the group structure).

theorem RoughPaths.Signature.inv_ofPiecewiseLinear {α : Type u} {R : Type v} [Field R] [CharZero R] (segs : List (α → R)) : (ofPiecewiseLinear segs)⁻¹ = ofPiecewiseLinear (List.map (fun (s : α → R) => -s) segs.reverse)

The group inverse of a piecewise-linear signature is the signature of the reversed path: the antipode and time reversal agree, by uniqueness of inverses.