Docs / Syntax / Minimalist / Workspace / Coproduct / TraceGrading
import Linglib.Syntax.Minimalist.Workspace.Coproduct.TraceGrading · namespace ConnesKreimer
The graded subspaces of ConnesKreimer R (UnorderedTree (α ⊕ β)) under the
edge-count grading (the summed UnorderedTree.numEdges of a forest),
with the coproduct half of the grading compatibility
(comulCAlgHomN_of'_mem_gradedSpan) — the graded content of Lemma 1.2.10.
TODO: once mathlib's graded coalgebra/bialgebra API lands
(leanprover-community/mathlib4#39849), restate gradedPiece as a
DirectSum.Decomposition and this file's content as a GradedBialgebra
instance (with connectedness feeding the graded Hopf upgrade).
Per Marcolli et al. 2025 p. 37, Lemma 1.2.10:
Let V^c(𝔉_{SO_0}) denote the vector space (over ℚ) spanned by the workspaces F ∈ 𝔉_{SO_0}, endowed with the product given by the disjoint union ⊔ and the coproduct Δ^c of (1.2.8). The space V(𝔉_{SO_0}) is graded by the number of edges. Then (V^c(𝔉_{SO_0}), ⊔, Δ^c) is a graded bialgebra.
This file defines the graded subspaces and proves the coproduct half of
the grading compatibility (comulCAlgHomN_of'_mem_gradedSpan); the
product half is edge-count additivity over disjoint union
(Multiset.map_add, Multiset.sum_add), and edge conservation through the trace cuts is
cutSummandsCN_numEdges (Coproduct/TraceConservation.lean).
The graded piece V_n is the subspace of ConnesKreimer R (UnorderedTree X)
spanned by forests with exactly n edges.
The definition is too large to print here; read it in the source.
Used by comulCAlgHomN_of'_mem_gradedSpan
Δ^c preserves the edge-count grading (Marcolli et al. 2025 Lemma 1.2.10, p. 37).
Built from