Edge-count grading of the Δ^c bialgebra

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).

References

• [MCB25]

Edge-count grading

Per [MCB25] 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 cut machinery is cutSummandsCN_numEdges (Core/Combinatorics/RootedTree/Cut.lean).

noncomputable def ConnesKreimer.gradedPiece {R : Type u_1} [CommRing R] (X : Type u_4) (n : ℕ) : Submodule R (ConnesKreimer R (UnorderedTree X))

The graded piece V_n is the subspace of ConnesKreimer R (UnorderedTree X) spanned by forests with exactly n edges.

Equations

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

Homogeneous tensor span at fixed total edge degree

theorem ConnesKreimer.comulCAlgHomN_of'_mem_gradedSpan {R : Type u_1} [CommRing R] {α : Type u_2} {β : Type u_3} (τ : UnorderedTree (α ⊕ β) → β) (F : UnorderedTree.Forest (UnorderedTree (α ⊕ β))) : (comulCAlgHomN τ) (of' F) ∈ Submodule.span R {y : TensorProduct R (ConnesKreimer R (UnorderedTree (α ⊕ β))) (ConnesKreimer R (UnorderedTree (α ⊕ β))) | ∃ (i : ℕ) (j : ℕ) (_ : i + j = (Multiset.map UnorderedTree.numEdges F).sum) (xi : ConnesKreimer R (UnorderedTree (α ⊕ β))) (yi : ConnesKreimer R (UnorderedTree (α ⊕ β))), xi ∈ gradedPiece (α ⊕ β) i ∧ yi ∈ gradedPiece (α ⊕ β) j ∧ y = xi ⊗ₜ[R] yi}

Δ^c preserves the edge-count grading ([MCB25] Lemma 1.2.10, p. 37): the coproduct of a basis forest lies in the span of homogeneous tensors xi ⊗ yi with degrees summing to the forest's edge count. With edge-count additivity over the product (disjoint union) and comulCN_coassoc, this gives the lemma's graded bialgebra structure on V^c(𝔉_{SO_0}).