Documentation

Linglib.Core.Algebra.RootedTree.Coproduct.TraceGrading

Edge-count grading of the Δ^c bialgebra #

[MCB25]

The graded subspaces of ConnesKreimer R (Nonplanar (α ⊕ β)) under the edge-count grading (Forest.edgeCount, Core/Data/RoseTree/Nonplanar.lean), 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).

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 (Forest.edgeCount_add), and edge conservation through the trace cut machinery is cutSummandsCN_edgeCount (Core/Combinatorics/RootedTree/Cut.lean).

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

Graded piece V_n: the subspace of ConnesKreimer R (Nonplanar X) spanned by forests with exactly n edges.

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

    Homogeneous tensor span at fixed total edge degree #

    source
    theorem ConnesKreimer.comulCAlgHomN_of'_mem_gradedSpan {R : Type u_1} [CommRing R] {α : Type u_2} {β : Type u_3} (τ : RoseTree.Nonplanar (α ⊕ β) → β) (F : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar (α ⊕ β))) :
    (comulCAlgHomN τ) (of' F) ∈ Submodule.span R {y : TensorProduct R (ConnesKreimer R (RoseTree.Nonplanar (α ⊕ β))) (ConnesKreimer R (RoseTree.Nonplanar (α ⊕ β))) | ∃ (i : ℕ) (j : ℕ) (_ : i + j = RoseTree.Nonplanar.Forest.edgeCount F) (xi : ConnesKreimer R (RoseTree.Nonplanar (α ⊕ β))) (yi : ConnesKreimer R (RoseTree.Nonplanar (α ⊕ β))), 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}).