Bialgebra structure on ConnesKreimer R T via shuffle Δ

Registers Coalgebra R (ConnesKreimer R T) and Bialgebra R (ConnesKreimer R T) instances using comulShuffle (the shuffle/polynomial coproduct, where each tree is primitive: Δ(of' {t}) = of' {t} ⊗ 1 + 1 ⊗ of' {t}) and the existing counit (empty-forest coefficient extractor).

This is distinct from mathlib's default AddMonoidAlgebra.instBialgebra (which uses the group-like coproduct single g r ↦ single g r ⊗ single g r). The def-vs-abbrev discipline on ConnesKreimer R T keeps the two unambiguous: typeclass synthesis on ConnesKreimer R T finds the shuffle Bialgebra instance, while AddMonoidAlgebra R (Forest T) retains the group-like one.

Status

Phase A2 of Path A-honest (convolution route to GL associativity). [UPSTREAM] candidate (the parametric construction is mathlib-generic).

§1: Counit laws

(ε ⊗ id) ∘ Δ = mk R 1 and (id ⊗ ε) ∘ Δ = (mk R).flip 1. Proved by LinearMap-extensionality reduction to basis of' F₀, then induction on the multiset F₀ via multiplicativity (comulShuffle_mul + Algebra.TensorProduct algebra-hom structure on the targets).

theorem RootedTree.ConnesKreimer.rTensor_counit_comulShuffle {R : Type u} [CommSemiring R] {T : Type v} [DecidableEq T] : LinearMap.rTensor (ConnesKreimer R T) counit.toLinearMap ∘ₗ comulShuffle = (TensorProduct.mk R R (ConnesKreimer R T)) 1

LinearMap form of the left counit law: (ε ⊗ id) ∘ Δ = mk R 1.

theorem RootedTree.ConnesKreimer.lTensor_counit_comulShuffle {R : Type u} [CommSemiring R] {T : Type v} [DecidableEq T] : LinearMap.lTensor (ConnesKreimer R T) counit.toLinearMap ∘ₗ comulShuffle = (TensorProduct.mk R (ConnesKreimer R T) R).flip 1

LinearMap form of the right counit law: (id ⊗ ε) ∘ Δ = (mk R).flip 1.

§2: Coalgebra and Bialgebra instances

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instCoalgebraStruct {R : Type u} [CommSemiring R] {T : Type v} [DecidableEq T] : CoalgebraStruct R (ConnesKreimer R T)

Underlying CoalgebraStruct data.

Equations

• RootedTree.ConnesKreimer.instCoalgebraStruct = { comul := RootedTree.ConnesKreimer.comulShuffle, counit := RootedTree.ConnesKreimer.counit.toLinearMap }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instCoalgebra {R : Type u} [CommSemiring R] {T : Type v} [DecidableEq T] : Coalgebra R (ConnesKreimer R T)

The Coalgebra structure on ConnesKreimer R T with shuffle Δ.

Equations

• RootedTree.ConnesKreimer.instCoalgebra = { toCoalgebraStruct := RootedTree.ConnesKreimer.instCoalgebraStruct, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instBialgebra {R : Type u} [CommSemiring R] {T : Type v} [DecidableEq T] : Bialgebra R (ConnesKreimer R T)

The Bialgebra structure on ConnesKreimer R T with shuffle Δ.

Equations

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