The coproduct with trace markers

This file defines the coproduct Δ^c of Marcolli, Chomsky and Berwick on forests of trees whose vertices are labelled α ⊕ β. It sums over the admissible cuts of a tree, pairing the cut-off subtrees with the remaining trunk, in which each cut subtree S leaves a trace leaf inr (τ S) computed by a trace encoder τ. With the edge grading of TraceGrading.lean this gives their Lemma 1.2.10: disjoint union and Δ^c make a graded bialgebra.

Main definitions

• ConnesKreimer.comulCAlgHomN: Δ^c as an algebra homomorphism, for a trace encoder τ.
• ConnesKreimer.TraceCoherent: τ gives a cut trunk the same marker as the tree it was cut from.

Main results

• ConnesKreimer.comulCN_coassoc: Δ^c is coassociative for a coherent encoder.
• ConnesKreimer.instIsAdmissibleCutsCN: the counit laws and coassociativity, which give WithCuts R (cutSummandsCN τ) its Bialgebra instance.

Implementation notes

Coassociativity is proved directly: both composites enumerate pairs of nested admissible cuts, and the two enumerations agree under trace coherence (DoubleCut.coassT). The pairing duality that gives coassociativity of the pruning coproduct in Coproduct/PruningDuality.lean fails here, because grafting never removes trace markers.

References

• [MCB25]
• [Foi21]

Δ^c on trees and forests

These instantiate the admissible-cut coproduct of Coproduct/WithCuts.lean at the enumeration cutSummandsCN τ.

noncomputable def ConnesKreimer.comulCTreeN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) : UnorderedTree (α ⊕ β) → TensorProduct R (ConnesKreimer R (UnorderedTree (α ⊕ β))) (ConnesKreimer R (UnorderedTree (α ⊕ β)))

comulCTreeN τ is Δ^c on a single tree, comulTreeNG at the cuts cutSummandsCN τ.

Equations

• ConnesKreimer.comulCTreeN τ = ConnesKreimer.comulTreeNG (ConnesKreimer.cutSummandsCN τ)

noncomputable def ConnesKreimer.comulCForestN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) : UnorderedTree.Forest (UnorderedTree (α ⊕ β)) → TensorProduct R (ConnesKreimer R (UnorderedTree (α ⊕ β))) (ConnesKreimer R (UnorderedTree (α ⊕ β)))

comulCForestN τ is Δ^c on a forest, the product over its trees.

Equations

• ConnesKreimer.comulCForestN τ = ConnesKreimer.comulForestNG (ConnesKreimer.cutSummandsCN τ)

@[simp]

theorem ConnesKreimer.comulCForestN_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) : comulCForestN τ 0 = 1

@[simp]

theorem ConnesKreimer.comulCForestN_add {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) (F G : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : comulCForestN τ (F + G) = comulCForestN τ F * comulCForestN τ G

noncomputable def ConnesKreimer.comulCAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) : ConnesKreimer R (UnorderedTree (α ⊕ β)) →ₐ[R] TensorProduct R (ConnesKreimer R (UnorderedTree (α ⊕ β))) (ConnesKreimer R (UnorderedTree (α ⊕ β)))

comulCAlgHomN τ is the coproduct Δ^c on ConnesKreimer R (UnorderedTree (α ⊕ β)), an algebra homomorphism, for the trace encoder τ.

Equations

• ConnesKreimer.comulCAlgHomN τ = ConnesKreimer.comulAlgHomNG (ConnesKreimer.cutSummandsCN τ)

@[simp]

theorem ConnesKreimer.comulCAlgHomN_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) (F : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : (comulCAlgHomN τ) (of' F) = comulCForestN τ F

@[simp]

theorem ConnesKreimer.comulCAlgHomN_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) (T : UnorderedTree (α ⊕ β)) : (comulCAlgHomN τ) (ofTree T) = comulCTreeN τ T

Trace coherence

Coassociativity of Δ^c depends on the trace encoder. Iterating Δ^c encodes a subtree that already carries markers, while the other cut order encodes the original subtree; for τ the number of inl vertices the two disagree on a three-vertex chain of inl vertices. Marcolli, Chomsky and Berwick's proof of Lemma 1.2.10 (pp. 37–38) uses that "the accessible terms of accessible terms … are themselves accessible terms", and TraceCoherent states the hypothesis this needs.

def ConnesKreimer.TraceCoherent {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) : Prop

A trace encoder τ is coherent when it gives a cut trunk, with its trace markers, the same marker as the tree it was cut from. Constant encoders are coherent (traceCoherent_const).

Equations

• ConnesKreimer.TraceCoherent τ = ∀ (T : UnorderedTree (α ⊕ β)), ∀ p ∈ ConnesKreimer.cutSummandsCN τ T, τ p.2 = τ T

theorem ConnesKreimer.traceCoherent_const {α : Type u_2} {β : Type u_3} (b : β) : TraceCoherent fun (x : UnorderedTree (α ⊕ β)) => b

Constant trace encoders are coherent.

Enumerating pairs of nested cuts

Both (Δ^c ⊗ id) ∘ Δ^c and (id ⊗ Δ^c) ∘ Δ^c sum over pairs of nested admissible cuts of a tree. This section writes Δ^c as a sum over cut enumerators (treeCutsN, forestCutsN) and each composite as a sum over a double-cut enumerator (dcLHS, dcRHS).

Descent of the double-cut enumerators

The enumerators dcLHS and dcRHS are the images under UnorderedTree.mk of the planar DoubleCut.dcLHSP and DoubleCut.dcRHSP, which DoubleCut.coassT identifies.

Coassociativity

The statements are over a commutative ring for the Bialgebra consumers; the proof itself works over a commutative semiring.

theorem ConnesKreimer.comulCN_coassoc_tree {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : UnorderedTree (α' ⊕ β') → β') (hτ : TraceCoherent τ) (T : UnorderedTree (α' ⊕ β')) : (TensorProduct.assoc R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (ConnesKreimer R' (UnorderedTree (α' ⊕ β')))) ((LinearMap.rTensor (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (comulCAlgHomN τ).toLinearMap) (comulCTreeN τ T)) = (LinearMap.lTensor (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (comulCAlgHomN τ).toLinearMap) (comulCTreeN τ T)

On a tree, both composites enumerate the pairs of nested admissible cuts of T, and TraceCoherent τ makes the markers written by the two cut orders agree.

theorem ConnesKreimer.comulCN_coassoc {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : UnorderedTree (α' ⊕ β') → β') (hτ : TraceCoherent τ) : ↑(TensorProduct.assoc R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (ConnesKreimer R' (UnorderedTree (α' ⊕ β')))) ∘ₗ LinearMap.rTensor (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (comulCAlgHomN τ).toLinearMap ∘ₗ (comulCAlgHomN τ).toLinearMap = LinearMap.lTensor (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (comulCAlgHomN τ).toLinearMap ∘ₗ (comulCAlgHomN τ).toLinearMap

Δ^c is coassociative for a coherent trace encoder. On each tree both composites enumerate the pairs of nested cuts; the forest case follows since both are algebra homomorphisms.

Counit laws and the bialgebra

The counit laws follow from the uniqueness of the empty cut (cutSummandsCN_filter_empty).

theorem ConnesKreimer.comulCAlgHomN_coassoc_algHom {R' : Type u_4} [CommRing R'] {α' : Type u_5} {β' : Type u_6} (τ : UnorderedTree (α' ⊕ β') → β') (hτ : TraceCoherent τ) : (↑(Algebra.TensorProduct.assoc R' R' R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))) (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))))).comp ((Algebra.TensorProduct.map (comulCAlgHomN τ) (AlgHom.id R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))))).comp (comulCAlgHomN τ)) = (Algebra.TensorProduct.map (AlgHom.id R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β')))) (comulCAlgHomN τ)).comp (comulCAlgHomN τ)

The AlgHom form of Δ^c coassociativity under trace coherence.

Counit laws on trees and forests

As for the pruning coproduct, the laws are proved on trees and extended to forests multiplicatively, over a commutative semiring.

theorem ConnesKreimer.counit_rTensor_comulCAlgHomN {R' : Type u_4} [CommSemiring R'] {α' : Type u_5} {β' : Type u_6} (τ : UnorderedTree (α' ⊕ β') → β') : (Algebra.TensorProduct.map counit (AlgHom.id R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β'))))).comp (comulCAlgHomN τ) = ↑(Algebra.TensorProduct.lid R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β')))).symm

The right counit law for Δ^c.

theorem ConnesKreimer.counit_lTensor_comulCAlgHomN {R' : Type u_4} [CommSemiring R'] {α' : Type u_5} {β' : Type u_6} (τ : UnorderedTree (α' ⊕ β') → β') : (Algebra.TensorProduct.map (AlgHom.id R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β')))) counit).comp (comulCAlgHomN τ) = ↑(Algebra.TensorProduct.rid R' R' (ConnesKreimer R' (UnorderedTree (α' ⊕ β')))).symm

The left counit law for Δ^c.

theorem ConnesKreimer.comulCAlgHomN_eq_G {α' : Type u_5} {β' : Type u_6} {R : Type u_7} [CommSemiring R] (τ : UnorderedTree (α' ⊕ β') → β') : comulCAlgHomN τ = comulAlgHomNG (cutSummandsCN τ)

Δ^c is the admissible-cut coproduct at the cuts cutSummandsCN τ.

instance ConnesKreimer.instIsAdmissibleCutsCN {α' : Type u_5} {β' : Type u_6} (τ : UnorderedTree (α' ⊕ β') → β') [Fact (TraceCoherent τ)] : IsAdmissibleCuts (cutSummandsCN τ)

For a coherent trace encoder, cutSummandsCN τ is an admissible cut policy, so WithCuts R (cutSummandsCN τ) is a bialgebra, as in Marcolli, Chomsky and Berwick's Lemma 1.2.10. Coherence enters through Fact, since instance search cannot find the hypothesis otherwise.