Docs / Syntax / Minimalist / Workspace / Coproduct / Trace
import Linglib.Syntax.Minimalist.Workspace.Coproduct.Trace · namespace ConnesKreimer
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.
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.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.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.
These instantiate the admissible-cut coproduct of Coproduct/WithCuts.lean at the enumeration
cutSummandsCN τ.
comulCTreeN τ is Δ^c on a single tree, comulTreeNG at the cuts cutSummandsCN τ.
comulCForestN τ is Δ^c on a forest, the product over its trees.
Used by comulCForestN_zero, comulCForestN_add, comulCAlgHomN_apply_of'
Built from
Built from
comulCAlgHomN τ is the coproduct Δ^c on ConnesKreimer R (UnorderedTree (α ⊕ β)), an
algebra homomorphism, for the trace encoder τ.
Used by comulCAlgHomN_apply_of', comulCAlgHomN_apply_ofTree, comulCN_coassoc_tree, comulCN_coassoc, comulCAlgHomN_coassoc_algHom, counit_rTensor_comulCAlgHomN, counit_lTensor_comulCAlgHomN, comulCAlgHomN_eq_G
Used in Syntax/Minimalist/Workspace/Coproduct/Deletion, Syntax/Minimalist/Workspace/Coproduct/TraceGrading
Built from ,
Built from ,
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.
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).
Used by traceCoherent_const, comulCN_coassoc_tree, comulCN_coassoc, comulCAlgHomN_coassoc_algHom, instIsAdmissibleCutsCN
Constant trace encoders are coherent.
Built from
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).
The enumerators dcLHS and dcRHS are the images under UnorderedTree.mk of the planar
DoubleCut.dcLHSP and DoubleCut.dcRHSP, which DoubleCut.coassT identifies.
The statements are over a commutative ring for the Bialgebra consumers; the proof itself works
over a commutative semiring.
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.
Built from , ,
Δ^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.
Built from ,
The counit laws follow from the uniqueness of the empty cut (cutSummandsCN_filter_empty).
The AlgHom form of Δ^c coassociativity under trace coherence.
Built from ,
As for the pruning coproduct, the laws are proved on trees and extended to forests multiplicatively, over a commutative semiring.
The right counit law for Δ^c.
Built from
The left counit law for Δ^c.
Built from
Δ^c is the admissible-cut coproduct at the cuts cutSummandsCN τ.
Built from
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.
Built from