Graded combinatorial bialgebras: the character group

A connected grading on a combinatorial bialgebra H (as in Definition 2.1 of Rahm, Planar Regularity Structures): a degree function on the basis for which the unit is the unique degree-zero element, degrees add along the product expansion, and every coproduct term splits the degree.

The main theorem is the classical one: over a connected graded bialgebra the characters form a group under convolution (CombBialg.Grading.characterGroup) — no antipode is needed. The inverse is the geometric series φ⁻¹ = ∑ₖ (ε − φ)^{*k}, a finite sum in each degree because (ε − φ)^{*k} vanishes below degree k (convPow_vanish); the convolution-inverse identities follow by telescoping (conv_gradedInv, gradedInv_conv), and multiplicativity of the inverse (gradedInv_isCharacter) by strong induction on total degree, splitting the counit as ε = φ + (ε − φ) and extracting the diagonal with the counit laws.

This equips the characters of the BCK, labelled BCK and MKW forest bialgebras with group structure (see HopfAlgebras.Combinatorial.GradedInstances).

structure HopfAlgebras.CombBialg.Grading {B : Type u} (H : CombBialg B) : Type u

A connected grading of a combinatorial bialgebra: the unit is the unique basis element of degree zero, degrees are additive along the product expansion, and each coproduct term splits the degree.

• deg : B → ℕ

  The degree of a basis element.

• deg_eq_zero_iff (x : B) : self.deg x = 0 ↔ x = H.one

  Connectedness: the unit is the only degree-zero element.

• deg_coprod (x : B) (p : B × B) : p ∈ H.coprod x → self.deg p.1 + self.deg p.2 = self.deg x

  Coproduct terms split the degree.

• deg_mul (x y z : B) : z ∈ H.mul x y → self.deg z = self.deg x + self.deg y

  Degrees are additive along the product expansion.

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

Convolution powers of a functional, with the counit as the zeroth power.

Equations

• H.convPow φ 0 = HopfAlgebras.CombBialg.Character.counit
• H.convPow φ k.succ = HopfAlgebras.CombBialg.Character.conv φ (H.convPow φ k)

def HopfAlgebras.CombBialg.counitSub {B : Type u} {R : Type v} (H : CombBialg B) [CommRing R] (φ : B → R) : B → R

The counit defect ε − φ of a functional.

Equations

• H.counitSub φ x = HopfAlgebras.CombBialg.Character.counit x - φ x

Sum plumbing

Degree bookkeeping

theorem HopfAlgebras.CombBialg.Grading.deg_one {B : Type u} {H : CombBialg B} (G : H.Grading) : G.deg H.one = 0

theorem HopfAlgebras.CombBialg.Grading.deg_pos_of_ne_one {B : Type u} {H : CombBialg B} (G : H.Grading) {x : B} (hx : x ≠ H.one) : 0 < G.deg x

Vanishing of convolution powers

theorem HopfAlgebras.CombBialg.Grading.convPow_vanish {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommSemiring R] {φ : B → R} (hφ0 : φ H.one = 0) (k : ℕ) (x : B) : G.deg x < k → H.convPow φ k x = 0

If φ kills the unit, its k-th convolution power vanishes below degree k.

The geometric-series inverse

noncomputable def HopfAlgebras.CombBialg.Grading.gradedInv {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommRing R] (φ : B → R) : B → R

The convolution inverse of a character over a connected graded bialgebra: the geometric series ∑ₖ (ε − φ)^{*k}, truncated at the degree of the argument.

Equations

• G.gradedInv φ x = ∑ k ∈ Finset.range (G.deg x + 1), H.convPow (H.counitSub φ) k x

theorem HopfAlgebras.CombBialg.Grading.counitSub_one {B : Type u} {R : Type v} {H : CombBialg B} [CommRing R] {φ : B → R} (hφ1 : φ H.one = 1) : H.counitSub φ H.one = 0

theorem HopfAlgebras.CombBialg.Grading.gradedInv_eq_sum {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommRing R] {φ : B → R} (hφ1 : φ H.one = 1) {x : B} {n : ℕ} (hn : G.deg x ≤ n) : G.gradedInv φ x = ∑ k ∈ Finset.range (n + 1), H.convPow (H.counitSub φ) k x

The truncation in gradedInv can be extended to any bound on the degree.

theorem HopfAlgebras.CombBialg.Grading.conv_counit_left {B : Type u} {R : Type v} {H : CombBialg B} [CommRing R] (F : B → R) : Character.conv Character.counit F = F

Convolution with the counit on the left is the identity.

theorem HopfAlgebras.CombBialg.Grading.conv_counit_right {B : Type u} {R : Type v} {H : CombBialg B} [CommRing R] (F : B → R) : Character.conv F Character.counit = F

Convolution with the counit on the right is the identity.

theorem HopfAlgebras.CombBialg.Grading.conv_assoc {B : Type u} {R : Type v} {H : CombBialg B} [CommRing R] (f g h : B → R) : Character.conv (Character.conv f g) h = Character.conv f (Character.conv g h)

Convolution is associative on arbitrary functionals.

theorem HopfAlgebras.CombBialg.Grading.conv_convPow_comm {B : Type u} {R : Type v} {H : CombBialg B} [CommRing R] (φ : B → R) (k : ℕ) : Character.conv φ (H.convPow φ k) = Character.conv (H.convPow φ k) φ

φ commutes with its own convolution powers.

theorem HopfAlgebras.CombBialg.Grading.conv_gradedInv {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommRing R] {φ : B → R} (hφ : H.IsCharacter φ) : Character.conv φ (G.gradedInv φ) = Character.counit

Left inverse identity: φ * φ⁻¹ = ε for a character φ.

theorem HopfAlgebras.CombBialg.Grading.gradedInv_conv {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommRing R] {φ : B → R} (hφ : H.IsCharacter φ) : Character.conv (G.gradedInv φ) φ = Character.counit

Right inverse identity: φ⁻¹ * φ = ε for a character φ.

theorem HopfAlgebras.CombBialg.Grading.gradedInv_one {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommRing R] {φ : B → R} : G.gradedInv φ H.one = 1

The inverse takes the value 1 on the unit.

Multiplicativity of the inverse

theorem HopfAlgebras.CombBialg.Grading.gradedInv_isCharacter {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommRing R] {φ : B → R} (hφ : H.IsCharacter φ) : H.IsCharacter (G.gradedInv φ)

The inverse of a character is a character. Proved by strong induction on total degree: the counit splits as ε = φ + (ε − φ), the φφ-part collapses by the bialgebra axiom and the inverse identities, every term containing an ε − φ factor dies by the inductive hypothesis, and the εε-part extracts the claim via the counit laws.

The character group

@[reducible]

noncomputable def HopfAlgebras.CombBialg.Grading.characterGroup {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommRing R] : Group (H.Character R)

The character group of a connected graded combinatorial bialgebra: characters form a group under convolution, with the geometric-series inverse.

Equations

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

theorem HopfAlgebras.CombBialg.Grading.isUnit_character {B : Type u} {R : Type v} {H : CombBialg B} (G : H.Grading) [CommRing R] (φ : H.Character R) : IsUnit φ

Every character of a connected graded combinatorial bialgebra is a unit of the convolution monoid.