Gradings of the concrete combinatorial bialgebras

The word shuffle Hopf algebra is graded by word length, and the BCK, labelled BCK and MKW forest bialgebras by forest order. Via CombBialg.Grading.characterGroup the characters of all four form groups under convolution — in particular the tree bialgebras, which have no terms-level antipode, acquire their character groups here.

The only new combinatorial input is mkwTermsAux_order: MKW coproduct terms split the forest order, proved by the same well-founded recursion as mkwTermsAux itself.

The word shuffle Hopf algebra, graded by word length

def HopfAlgebras.wordGrading (α : Type u) : (wordHopf α).Grading

Word length grades the word shuffle Hopf algebra.

Equations

• HopfAlgebras.wordGrading α = { deg := List.length, deg_eq_zero_iff := ⋯, deg_coprod := ⋯, deg_mul := ⋯ }

The BCK bialgebras, graded by forest order

def HopfAlgebras.bckGrading : bckBialg.Grading

Forest order grades the BCK bialgebra.

Equations

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

def HopfAlgebras.lbckGrading (α : Type u) : (lbckBialg α).Grading

Forest order grades the labelled BCK bialgebra.

Equations

• HopfAlgebras.lbckGrading α = { deg := HopfAlgebras.LRootedForest.order, deg_eq_zero_iff := ⋯, deg_coprod := ⋯, deg_mul := ⋯ }

The MKW bialgebra, graded by planar forest order

theorem HopfAlgebras.mkwTermsAux_order (l : List PTree) (pr : PlanarForest × PlanarForest) : pr ∈ PlanarForest.mkwTermsAux l → pr.1.order + pr.2.order = PTree.orderList l

MKW coproduct terms split the planar forest order — by the same well-founded recursion as mkwTermsAux.

theorem HopfAlgebras.mkwTerms_order {ω : PlanarForest} {pr : PlanarForest × PlanarForest} (hpr : pr ∈ ω.mkwTerms) : pr.1.order + pr.2.order = ω.order

MKW coproduct terms split the forest order.

def HopfAlgebras.mkwGrading : mkwBialg.Grading

Planar forest order grades the MKW bialgebra.

Equations

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

Character groups of the tree bialgebras

The word shuffle Hopf algebra already carries the antipode group (CombBialg.Character.instGroup); the graded construction now supplies groups for the tree bialgebras, which have no terms-level antipode.

@[reducible]

noncomputable def HopfAlgebras.bckCharacterGroup (R : Type v) [CommRing R] : Group (bckBialg.Character R)

The BCK character group: branched rough path increments are invertible under character convolution.

Equations

• HopfAlgebras.bckCharacterGroup R = HopfAlgebras.bckGrading.characterGroup

@[reducible]

noncomputable def HopfAlgebras.lbckCharacterGroup (R : Type v) [CommRing R] (α : Type u) : Group ((lbckBialg α).Character R)

The labelled BCK character group.

Equations

• HopfAlgebras.lbckCharacterGroup R α = (HopfAlgebras.lbckGrading α).characterGroup

@[reducible]

noncomputable def HopfAlgebras.mkwCharacterGroup (R : Type v) [CommRing R] : Group (mkwBialg.Character R)

The MKW character group: planarly branched rough path increments are invertible under Grossman–Larson convolution.

Equations

• HopfAlgebras.mkwCharacterGroup R = HopfAlgebras.mkwGrading.characterGroup