Combinatorial Hopf algebras and their character groups

A combinatorial Hopf algebra (CombHopf) is a Hopf algebra given by a distinguished basis B with finitary structure constants: the product and coproduct of basis elements expand as finite lists of basis elements (resp. pairs), and the antipode as a finite signed list. This is the common shape of the Hopf algebras of rough path theory — the word shuffle algebra, the Butcher–Connes–Kreimer algebra of rooted forests, and the Munthe-Kaas–Wright algebra of planar forests — and it avoids topological tensor products entirely: every axiom is a coefficientwise finite-sum identity.

The payoff is proved once, abstractly: the R-valued characters (CombHopf.Character) — multiplicative functionals on the basis — form a monoid under the convolution product dual to the coproduct (Character.instMonoid), and over a commutative ring a group, with inverse given by precomposition with the antipode (Character.instGroup). Signatures of paths, branched signatures, and Lie–Butcher series are characters of the three instances above.

structure HopfAlgebras.CombBialg (B : Type u) : Type (max u (v + 1))

A combinatorial bialgebra on a basis B: finitary expansions of the product and coproduct of basis elements, with the bialgebra axioms stated as coefficientwise finite-sum identities against arbitrary coefficient functions. Its characters form a monoid under convolution (Character.instMonoid).

• mul : B → B → List B

  Product expansion of two basis elements.

• one : B

  The unit basis element (empty word / empty forest).

• coprod : B → List (B × B)

  Coproduct expansion of a basis element.

• isOne : B → Bool

  Boolean test for the unit basis element (keeps the counit's case split free of Decidable instance mismatches).

• isOne_iff (x : B) : self.isOne x = true ↔ x = self.one
• mul_one_expand (x : B) : self.mul x self.one = [x]
• one_mul_expand (x : B) : self.mul self.one x = [x]
• coprod_one : self.coprod self.one = [(self.one, self.one)]
• coassoc {R : Type v} [CommSemiring R] (f g h : B → R) (x : B) : (List.map (fun (p : B × B) => (List.map (fun (q : B × B) => f q.1 * g q.2) (self.coprod p.1)).sum * h p.2) (self.coprod x)).sum = (List.map (fun (p : B × B) => f p.1 * (List.map (fun (q : B × B) => g q.1 * h q.2) (self.coprod p.2)).sum) (self.coprod x)).sum

  Coassociativity, paired against coefficients.

• counit_left {R : Type v} [CommSemiring R] (f : B → R) (x : B) : (List.map (fun (p : B × B) => (if self.isOne p.1 = true then 1 else 0) * f p.2) (self.coprod x)).sum = f x

  Left counit law, paired against coefficients.

• counit_right {R : Type v} [CommSemiring R] (f : B → R) (x : B) : (List.map (fun (p : B × B) => f p.1 * if self.isOne p.2 = true then 1 else 0) (self.coprod x)).sum = f x

  Right counit law, paired against coefficients.

• mul_count_one {R : Type v} [CommSemiring R] (x y : B) : (List.map (fun (z : B) => if self.isOne z = true then 1 else 0) (self.mul x y)).sum = (if self.isOne x = true then 1 else 0) * if self.isOne y = true then 1 else 0

  The counit is multiplicative: the unit occurs in a product expansion exactly when both factors are the unit.

• bialg {R : Type v} [CommSemiring R] (φ ψ : B → R) (x y : B) : (List.map (fun (z : B) => (List.map (fun (p : B × B) => φ p.1 * ψ p.2) (self.coprod z)).sum) (self.mul x y)).sum = (List.map (fun (p : B × B) => (List.map (fun (q : B × B) => (List.map φ (self.mul p.1 q.1)).sum * (List.map ψ (self.mul p.2 q.2)).sum) (self.coprod y)).sum) (self.coprod x)).sum

  Product–coproduct (bialgebra) compatibility, paired against a pair of coefficient functions.

structure HopfAlgebras.CombHopf (B : Type u) extends HopfAlgebras.CombBialg B : Type (max u (v + 1))

A combinatorial Hopf algebra: a combinatorial bialgebra together with a finitary signed antipode expansion and its defining identities. Its characters form a group under convolution (Character.instGroup).

• mul : B → B → List B
• one : B
• coprod : B → List (B × B)
• isOne : B → Bool
• isOne_iff (x : B) : self.isOne x = true ↔ x = self.one
• mul_one_expand (x : B) : self.mul x self.one = [x]
• one_mul_expand (x : B) : self.mul self.one x = [x]
• coprod_one : self.coprod self.one = [(self.one, self.one)]
• coassoc {R : Type v} [CommSemiring R] (f g h : B → R) (x : B) : (List.map (fun (p : B × B) => (List.map (fun (q : B × B) => f q.1 * g q.2) (self.coprod p.1)).sum * h p.2) (self.coprod x)).sum = (List.map (fun (p : B × B) => f p.1 * (List.map (fun (q : B × B) => g q.1 * h q.2) (self.coprod p.2)).sum) (self.coprod x)).sum
• counit_left {R : Type v} [CommSemiring R] (f : B → R) (x : B) : (List.map (fun (p : B × B) => (if self.isOne p.1 = true then 1 else 0) * f p.2) (self.coprod x)).sum = f x
• counit_right {R : Type v} [CommSemiring R] (f : B → R) (x : B) : (List.map (fun (p : B × B) => f p.1 * if self.isOne p.2 = true then 1 else 0) (self.coprod x)).sum = f x
• mul_count_one {R : Type v} [CommSemiring R] (x y : B) : (List.map (fun (z : B) => if self.isOne z = true then 1 else 0) (self.mul x y)).sum = (if self.isOne x = true then 1 else 0) * if self.isOne y = true then 1 else 0
• bialg {R : Type v} [CommSemiring R] (φ ψ : B → R) (x y : B) : (List.map (fun (z : B) => (List.map (fun (p : B × B) => φ p.1 * ψ p.2) (self.coprod z)).sum) (self.mul x y)).sum = (List.map (fun (p : B × B) => (List.map (fun (q : B × B) => (List.map φ (self.mul p.1 q.1)).sum * (List.map ψ (self.mul p.2 q.2)).sum) (self.coprod y)).sum) (self.coprod x)).sum
• antipode : B → List (Bool × B)

  Signed antipode expansion (true = +1, false = -1).

• antipode_one : self.antipode self.one = [(true, self.one)]
• antipode_conv {R : Type v} [CommRing R] (f : B → R) (x : B) : x ≠ self.one → (List.map (fun (p : B × B) => (List.map (fun (sa : Bool × B) => (if sa.1 = true then 1 else -1) * (List.map f (self.mul sa.2 p.2)).sum) (self.antipode p.1)).sum) (self.coprod x)).sum = 0

  The antipode identity m ∘ (S ⊗ id) ∘ Δ = η ∘ ε, paired against coefficients.

• antipode_char {R : Type v} [CommRing R] (φ : B → R) : (∀ (x y : B), φ x * φ y = (List.map φ (self.mul x y)).sum) → ∀ (x y : B), (List.map (fun (sa : Bool × B) => (if sa.1 = true then 1 else -1) * φ sa.2) (self.antipode x)).sum * (List.map (fun (sa : Bool × B) => (if sa.1 = true then 1 else -1) * φ sa.2) (self.antipode y)).sum = (List.map (fun (z : B) => (List.map (fun (sa : Bool × B) => (if sa.1 = true then 1 else -1) * φ sa.2) (self.antipode z)).sum) (self.mul x y)).sum

  Precomposition with the antipode preserves multiplicativity (the antipode is an algebra morphism for a commutative product).

def HopfAlgebras.CombBialg.IsCharacter {B : Type u} (H : CombBialg B) {R : Type v} [CommSemiring R] (φ : B → R) : Prop

A character of a combinatorial Hopf algebra: a multiplicative R-valued functional on the basis, sending the unit to 1.

Equations

• H.IsCharacter φ = (φ H.one = 1 ∧ ∀ (x y : B), φ x * φ y = (List.map φ (H.mul x y)).sum)

def HopfAlgebras.CombBialg.Character {B : Type u} (H : CombBialg B) (R : Type v) [CommSemiring R] : Type (max u v)

The characters of a combinatorial Hopf algebra with values in R.

Equations

• H.Character R = { φ : B → R // H.IsCharacter φ }

@[implicit_reducible]

instance HopfAlgebras.CombBialg.Character.instCoeFunForall {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] : CoeFun (H.Character R) fun (x : H.Character R) => B → R

Equations

• HopfAlgebras.CombBialg.Character.instCoeFunForall = { coe := fun (φ : H.Character R) => ↑φ }

theorem HopfAlgebras.CombBialg.Character.map_one {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] (φ : H.Character R) : ↑φ H.one = 1

theorem HopfAlgebras.CombBialg.Character.map_mul {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] (φ : H.Character R) (x y : B) : ↑φ x * ↑φ y = (List.map (↑φ) (H.mul x y)).sum

theorem HopfAlgebras.CombBialg.Character.ext {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] {φ ψ : H.Character R} (h : ∀ (x : B), ↑φ x = ↑ψ x) : φ = ψ

theorem HopfAlgebras.CombBialg.Character.ext_iff {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] {φ ψ : H.Character R} : φ = ψ ↔ ∀ (x : B), ↑φ x = ↑ψ x

def HopfAlgebras.CombBialg.Character.conv {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] (φ ψ : B → R) : B → R

The convolution product of functionals, dual to the coproduct.

Equations

• HopfAlgebras.CombBialg.Character.conv φ ψ x = (List.map (fun (p : B × B) => φ p.1 * ψ p.2) (H.coprod x)).sum

def HopfAlgebras.CombBialg.Character.counit {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] : B → R

The counit character ε(x) = δ_{x,1}, the convolution unit.

Equations

• HopfAlgebras.CombBialg.Character.counit x = if H.isOne x = true then 1 else 0

theorem HopfAlgebras.CombBialg.Character.counit_isCharacter {B : Type u} (H : CombBialg B) {R : Type v} [CommSemiring R] : H.IsCharacter counit

theorem HopfAlgebras.CombBialg.Character.conv_isCharacter {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] (φ ψ : H.Character R) : H.IsCharacter (conv ↑φ ↑ψ)

Convolution of characters is a character (the bialgebra axiom).

@[implicit_reducible]

noncomputable instance HopfAlgebras.CombBialg.Character.instMonoid {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] : Monoid (H.Character R)

The character monoid: characters under convolution.

Equations

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

@[simp]

theorem HopfAlgebras.CombBialg.Character.mul_apply {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] (φ ψ : H.Character R) (x : B) : ↑(φ * ψ) x = (List.map (fun (p : B × B) => ↑φ p.1 * ↑ψ p.2) (H.coprod x)).sum

@[simp]

theorem HopfAlgebras.CombBialg.Character.one_apply {B : Type u} {H : CombBialg B} {R : Type v} [CommSemiring R] (x : B) : ↑1 x = if H.isOne x = true then 1 else 0

@[reducible, inline]

abbrev HopfAlgebras.CombHopf.Character {B : Type u} (H : CombHopf B) (R : Type v) [CommSemiring R] : Type (max u v)

Characters of the underlying bialgebra.

Equations

• H.Character R = H.Character R

def HopfAlgebras.CombHopf.Character.antipodeComp {B : Type u} {H : CombHopf B} {R : Type v} [CommRing R] (φ : B → R) : B → R

Precomposition with the (signed) antipode.

Equations

• HopfAlgebras.CombHopf.Character.antipodeComp φ x = (List.map (fun (sa : Bool × B) => (if sa.1 = true then 1 else -1) * φ sa.2) (H.antipode x)).sum

theorem HopfAlgebras.CombHopf.Character.antipodeComp_isCharacter {B : Type u} {H : CombHopf B} {R : Type v} [CommRing R] (φ : H.Character R) : H.IsCharacter (antipodeComp ↑φ)

theorem HopfAlgebras.CombHopf.Character.antipodeComp_conv {B : Type u} {H : CombHopf B} {R : Type v} [CommRing R] (φ : H.Character R) : ⟨antipodeComp ↑φ, ⋯⟩ * φ = 1

The antipode inverts characters on the left.

@[implicit_reducible]

noncomputable instance HopfAlgebras.CombHopf.Character.instGroup {B : Type u} {H : CombHopf B} {R : Type v} [CommRing R] : Group (H.Character R)

The character group: over a commutative ring, the characters of a combinatorial Hopf algebra form a group under convolution, with inverse given by precomposition with the antipode.

Equations

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

@[simp]

theorem HopfAlgebras.CombHopf.Character.inv_apply {B : Type u} {H : CombHopf B} {R : Type v} [CommRing R] (φ : H.Character R) (x : B) : ↑φ⁻¹ x = (List.map (fun (sa : Bool × B) => (if sa.1 = true then 1 else -1) * ↑φ sa.2) (H.antipode x)).sum