The deletion coproduct and the erasure of traces

Marcolli, Chomsky and Berwick extract accessible terms from a syntactic object with three coproducts, which differ in the remainder an extraction leaves. Δ^c contracts each extracted term to a trace leaf, Δ^ρ leaves the remainder of the admissible cut, and Δ^d deletes the term and contracts the vertices left with a single child. They relate the three by projections of the right channel: Π_{ρ,c} deletes the trace leaves, Π_{d,ρ} contracts the non-branching vertices, and Δ^d = (id ⊗ Π_{d,ρ}) ∘ Δ^ρ = (id ⊗ Π_{d,ρ} ∘ Π_{ρ,c}) ∘ Δ^c, displayed before their (1.3.10). Here Δ^d is defined by the first expression, and the second is proved for trees without traces.

Main definitions

• ConnesKreimer.eraseTraces: the projection that deletes every trace vertex.
• ConnesKreimer.cutSummandsDN: the deletion cuts, the pruning cuts with the unary vertices of each trunk contracted.
• ConnesKreimer.comulDAlgHomN: the deletion coproduct, which sums them (comulDAlgHomN_apply_ofTree).

Main results

• ConnesKreimer.eraseTraces_comp_rename_inl: erasure is a retraction of the embedding of the trees without traces.
• ConnesKreimer.eraseTraces_comulCAlgHomN: on trees without traces, erasing the traces that the trace coproduct leaves gives the pruning coproduct.
• ConnesKreimer.contractUnary_eraseTraces_comulCAlgHomN: erasing them and contracting the unary vertices gives the deletion coproduct.
• ConnesKreimer.cutSummandsDN_numEdges: in a full binary tree, deleting one accessible term costs two accessible terms besides its own, the book's (1.6.7).

Implementation notes

• Trees without traces are UnorderedTree α and trees with traces are UnorderedTree (α ⊕ β), so the relations hold along the embedding rename (UnorderedTree.map Sum.inl). The left channel of Δ^c on an embedded tree is embedded and the right channel is not, which is why the projections act on the right channel alone.
• The book's Π_{d,ρ} takes a tree whose vertices have at most two children to the maximal binary tree obtained by contracting edges. Here it is UnorderedTree.contractUnary, on trees of any arity.
• Δ^d carries no Bialgebra structure: its coassociativity holds only up to the multiplicity of some terms (the book's Lemma 1.2.12).
• (1.6.7) extends to a cut extracting several terms only when no two of them are sisters. A cut extracting both children of a vertex leaves it a leaf, with nothing to contract, so the two cost one accessible term each (cutSummandsN_numUnary).

References

• [MCB25]

Erasing traces

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

eraseTraces is the projection Π_{ρ,c}. It sends a tree whose root is a trace to 1 and removes from any other tree the subtrees rooted at a trace.

Equations

• ConnesKreimer.eraseTraces = ConnesKreimer.aeval fun (T : UnorderedTree (α ⊕ β)) => (UnorderedTree.filterMap Sum.getLeft? T).elim 1 ConnesKreimer.ofTree

@[simp]

theorem ConnesKreimer.eraseTraces_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (T : UnorderedTree (α ⊕ β)) : eraseTraces (ofTree T) = (UnorderedTree.filterMap Sum.getLeft? T).elim 1 ofTree

theorem ConnesKreimer.eraseTraces_comp_rename_inl {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} : eraseTraces.comp (rename (UnorderedTree.map Sum.inl)) = AlgHom.id R (ConnesKreimer R (UnorderedTree α))

Erasure is a retraction of the embedding of the trees without traces.

theorem ConnesKreimer.eraseTraces_comulCAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) : ((Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (UnorderedTree (α ⊕ β)))) eraseTraces).comp (comulCAlgHomN τ)).comp (rename (UnorderedTree.map Sum.inl)) = (Algebra.TensorProduct.map (rename (UnorderedTree.map Sum.inl)) (AlgHom.id R (ConnesKreimer R (UnorderedTree α)))).comp comulAlgHomN

On trees without traces, erasing the traces that Δ^c leaves in the right channel gives the pruning coproduct Δ^ρ.

The deletion coproduct

noncomputable def ConnesKreimer.comulDAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (UnorderedTree α) →ₐ[R] TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The deletion coproduct Δ^d is the pruning coproduct Δ^ρ followed, on the right channel, by the contraction Π_{d,ρ} of unary vertices.

Equations

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

def ConnesKreimer.cutSummandsDN {α : Type u_2} (T : UnorderedTree α) : Multiset (Multiset (UnorderedTree α) × UnorderedTree α)

The deletion cuts of a tree are its pruning cuts with the unary vertices of each trunk contracted.

Equations

• ConnesKreimer.cutSummandsDN T = Multiset.map (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => (p.1, p.2.contractUnary)) (ConnesKreimer.cutSummandsN T)

theorem ConnesKreimer.comulDAlgHomN_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : UnorderedTree α) : comulDAlgHomN (ofTree T) = ofTree T ⊗ₜ[R] 1 + (Multiset.map (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => of' p.1 ⊗ₜ[R] ofTree p.2) (cutSummandsDN T)).sum

On a tree, Δ^d sums the deletion cuts.

The cost of a deletion

theorem ConnesKreimer.cutSummandsDN_numEdges_of_card_le_one {α : Type u_2} {T : UnorderedTree α} {p : Multiset (UnorderedTree α) × UnorderedTree α} (hT : T.IsFullBinary) (hp : p ∈ cutSummandsDN T) (h : p.1.card ≤ 1) : T.numEdges = (Multiset.map UnorderedTree.numEdges p.1).sum + p.2.numEdges + 2 * p.1.card

A deletion cut of a full binary tree extracting at most one tree costs two edges for it besides the tree's own.

theorem ConnesKreimer.cutSummandsDN_numEdges {α : Type u_2} {T : UnorderedTree α} {p : Multiset (UnorderedTree α) × UnorderedTree α} (hT : T.IsFullBinary) (hp : p ∈ cutSummandsDN T) {v : UnorderedTree α} (hv : p.1 = {v}) : T.numEdges = v.numEdges + p.2.numEdges + 2

Deleting one accessible term costs two accessible terms besides its own ([MCB25] (1.6.7)).

theorem ConnesKreimer.hasExtractionCost_numEdges_cutSummandsDN {α : Type u_2} {F : Multiset (UnorderedTree α)} {s : CutChoice α} (hF : ∀ T ∈ F, T.IsFullBinary) (hs : s ∈ forestCutChoicesG cutSummandsDN F) (h : ∀ x ∈ s, x.2.2 ≠ 0 → x.2.1.card ≤ 1) : CutChoice.HasExtractionCost UnorderedTree.numEdges 2 s

A choice of deletion cuts of full binary trees, extracting at most one tree from each tree it cuts, costs two edges for each tree it extracts.

theorem ConnesKreimer.contractUnary_eraseTraces_comulCAlgHomN {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) : ((Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (UnorderedTree (α ⊕ β)))) ((rename UnorderedTree.contractUnary).comp eraseTraces)).comp (comulCAlgHomN τ)).comp (rename (UnorderedTree.map Sum.inl)) = (Algebra.TensorProduct.map (rename (UnorderedTree.map Sum.inl)) (AlgHom.id R (ConnesKreimer R (UnorderedTree α)))).comp comulDAlgHomN

On trees without traces, erasing the traces that Δ^c leaves and contracting the unary vertices gives the deletion coproduct Δ^d.