The primitive coproduct on the Connes–Kreimer algebra

The primitive coproduct Δ_P(t) = t ⊗ 1 + 1 ⊗ t on ConnesKreimer R T, extended multiplicatively, sums A ⊗ B over the splittings F = A + B of a forest. It is the coproduct of the symmetric algebra on the trees (Grinberg and Reiner, Example 1.3.14), unlike the admissible-cut coproducts of the sibling files.

Main declarations

• ConnesKreimer.comulPrim: the primitive coproduct, as an algebra homomorphism.
• ConnesKreimer.comulPrim_of': Δ_P(F) = ∑_{A + B = F} A ⊗ B.
• ConnesKreimer.comulAlgHomNG_emptyCuts: Δ_P is the admissible-cut coproduct whose only cut is the empty one.
• ConnesKreimer.rTensor_homogeneousComponent_comulPrim_of': the terms whose left factor has k trees are indexed by the k-tree subforests.
• ConnesKreimer.comulPrim_coassoc, ConnesKreimer.rTensor_counit_comp_comulPrim, ConnesKreimer.lTensor_counit_comp_comulPrim, ConnesKreimer.comm_comp_comulPrim: the coalgebra laws and cocommutativity, in the shape of Bialgebra.ofAlgHom.
• ConnesKreimer.comulPrim_comp_equiv: along IsSymmetricAlgebra.connesKreimer, Δ_P is the comultiplication of SymmetricAlgebra.instBialgebra.

Implementation notes

Δ_P is not a Bialgebra instance: the carrier already carries the admissible-cut Bialgebra (HopfAlgebra.lean), so Δ_P is an algebra homomorphism with its laws stated separately.

References

• [GR20]

noncomputable def ConnesKreimer.comulPrim {R : Type u_1} [CommSemiring R] {T : Type u_2} : ConnesKreimer R T →ₐ[R] TensorProduct R (ConnesKreimer R T) (ConnesKreimer R T)

The primitive coproduct Δ_P is the algebra homomorphism under which every tree is primitive, Δ_P(t) = t ⊗ 1 + 1 ⊗ t.

Equations

• ConnesKreimer.comulPrim = ConnesKreimer.aeval fun (t : T) => ConnesKreimer.ofTree t ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ConnesKreimer.ofTree t

@[simp]

theorem ConnesKreimer.comulPrim_ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} (t : T) : comulPrim (ofTree t) = ofTree t ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ofTree t

theorem ConnesKreimer.comulPrim_unique {R : Type u_1} [CommSemiring R] {T : Type u_2} (φ : ConnesKreimer R T →ₐ[R] TensorProduct R (ConnesKreimer R T) (ConnesKreimer R T)) (h : ∀ (t : T), φ (ofTree t) = ofTree t ⊗ₜ[R] 1 + 1 ⊗ₜ[R] ofTree t) : φ = comulPrim

Δ_P is the only algebra homomorphism under which every tree is primitive.

theorem ConnesKreimer.comulAlgHomNG_emptyCuts {R : Type u_1} [CommSemiring R] {α : Type u_3} : comulAlgHomNG emptyCuts = comulPrim

The admissible-cut coproduct at the empty-cut enumeration is primitive.

theorem ConnesKreimer.comulPrim_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : UnorderedTree.Forest T) : comulPrim (of' F) = (Multiset.map (fun (p : Multiset T × Multiset T) => of' p.1 ⊗ₜ[R] of' p.2) (Multiset.antidiagonal F)).sum

Δ_P sums A ⊗ B over the splittings F = A + B, counted with multiplicity.

theorem ConnesKreimer.rTensor_homogeneousComponent_comulPrim_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] (k : ℕ) (F : UnorderedTree.Forest T) : (LinearMap.rTensor (ConnesKreimer R T) (homogeneousComponent k)) (comulPrim (of' F)) = (Multiset.map (fun (A : UnorderedTree.Forest T) => of' A ⊗ₜ[R] of' (F - A)) (Multiset.powersetCard k F)).sum

The terms of Δ_P(F) whose left factor has k trees sum A ⊗ (F - A) over the k-tree subforests A of F.

theorem ConnesKreimer.comulPrim_coassoc {R : Type u_1} [CommSemiring R] {T : Type u_2} : (↑(Algebra.TensorProduct.assoc R R R (ConnesKreimer R T) (ConnesKreimer R T) (ConnesKreimer R T))).comp ((Algebra.TensorProduct.map comulPrim (AlgHom.id R (ConnesKreimer R T))).comp comulPrim) = (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R T)) comulPrim).comp comulPrim

theorem ConnesKreimer.rTensor_counit_comp_comulPrim {R : Type u_1} [CommSemiring R] {T : Type u_2} : (Algebra.TensorProduct.map counit (AlgHom.id R (ConnesKreimer R T))).comp comulPrim = ↑(Algebra.TensorProduct.lid R (ConnesKreimer R T)).symm

theorem ConnesKreimer.lTensor_counit_comp_comulPrim {R : Type u_1} [CommSemiring R] {T : Type u_2} : (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R T)) counit).comp comulPrim = ↑(Algebra.TensorProduct.rid R R (ConnesKreimer R T)).symm

theorem ConnesKreimer.comm_comp_comulPrim {R : Type u_1} [CommSemiring R] {T : Type u_2} : (↑(Algebra.TensorProduct.comm R (ConnesKreimer R T) (ConnesKreimer R T))).comp comulPrim = comulPrim

theorem ConnesKreimer.comulPrim_comp_equiv {R : Type u_1} [CommSemiring R] {T : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module R M] (b : Module.Basis T R M) : comulPrim.comp ↑⋯.equiv = (Algebra.TensorProduct.map ↑⋯.equiv ↑⋯.equiv).comp (Bialgebra.comulAlgHom R (SymmetricAlgebra R M))

Along the identification of ConnesKreimer R T with the symmetric algebra on a module with basis T, Δ_P is the comultiplication of the symmetric algebra.