The B- operator and the B+/B- pairing adjoint #
The B-_a operator on ConnesKreimer R (Nonplanar α)
([foissy-typed-decorated-rooted-trees-2018]'s B⁻ on decorated trees) is the
transpose of the grafting operator B+_a (Coproduct/Pruning.lean) under
the symmetry-weighted pairing (GrossmanLarson/Pairing.lean). On basis
elements:
B-_a (of' F) = if F = {Nonplanar.node a F'} for some F' then of' F' else 0
i.e., B-_a projects a singleton forest with an a-labeled root tree to
that tree's children forest, and vanishes otherwise.
Main definitions #
GrossmanLarson.bMinusTree,GrossmanLarson.bMinusBasis,GrossmanLarson.bMinusLin— B-_a per tree, per basis forest, and as a linear endomorphism.
Main results #
GrossmanLarson.isAdjointPair_bMinusLin_bPlusLin,GrossmanLarson.bMinusLin_pairing_adjoint— the transpose property⟨B-_a x, y⟩ = ⟨x, B+_a y⟩([OG08] Prop 3.2 substrate).GrossmanLarson.bMinusLin_gl_mul— the derivation identityB-(A ∗ B) = ε(A) B-(B) + B-(A) ∗ B([OG08] §3.2), whose duality argument the transpose property anchors.
bMinusTree and bMinusBasis #
Per-tree B-_a: the children forest when the root is labeled a,
else 0 — Foissy's B⁻ on trees
([foissy-typed-decorated-rooted-trees-2018]).
Equations
- GrossmanLarson.bMinusTree a T = if T.rootValue = a then GrossmanLarson.of' T.rootChildren else 0
Instances For
The B-_a operator on basis forests: bMinusTree on singletons, 0
otherwise. Stated via card/map/sum, which carry the descent to
the Multiset quotient.
Equations
- GrossmanLarson.bMinusBasis a F = if Multiset.card F = 1 then (Multiset.map (GrossmanLarson.bMinusTree a) F).sum else 0
Instances For
bMinusBasis a vanishes on basis forests that are not
singleton-a-rooted.
The B-_a linear map: linear extension of bMinusBasis via Finsupp.lift.
Equations
Instances For
B+/B- pairing adjoint #
Adjoint of bPlusLin a w.r.t. the symmetry-weighted pairing, on
basis elements: both sides are [F = {node a G}] · forestAutCard F.
B+/B- adjointness under the symmetry-weighted pairing, in mathlib's
LinearMap.IsAdjointPair packaging.
B+/B- adjoint under the symmetry-weighted pairing, pointwise:
⟨B-_a x, y⟩ = ⟨x, B+_a y⟩ for all a, x, y.
The OG derivation identity B-_a(x *_GL y) = ε(x) • B-_a y + B-_a x *_GL y #
OG paper [OG08] §3.2 proves this identity on the S(L)
side; on the CK carrier it is the direct identity
bMinusLin a (x *_GL y) = counit(x) • bMinusLin a y + bMinusLin a x *_GL y.
This identity says bMinusLin a is a "1-cocycle" with respect to *_GL
in the sense B-(xy) = ε(x) B-(y) + B-(x) y.
The proof reduces to the basis case x = of' A, y = of' B and
case-analyzes on A:
A = 0: counit = 1, B-_a (of' 0) = 0; identity reduces toB-_a (of' B) = B-_a (of' B).|A| ≥ 2: both sides 0 by length grading (B-_a vanishes on non-singletons).|A| = 1with root label ≠ a: both sides 0 (B-_a kills non-a-rooted singletons).|A| = 1with root label = a (A = {node a A'}): the combinatorial heart.
The hard case reduces to the substrate lemma:
insertion (of' {node a A'}) (of' B) = bPlusLin a (of' A' *_GL of' B)
(grafting B into the only tree of {node a A'} = a-rooting the GL
product). This is singleton_node_a_insertion_eq_bPlus_gl_mul below.
Key combinatorial substrate: grafting of' B into the
singleton-a-rooted host {node a A'} equals the a-rooting (via
bPlusLin a) of the GL product of' A' *_GL of' B.
Intuition: a result tree T' = node a (children of node a A' with B grafted)
has root label a (preserved by NIM) and children formed by either
(i) a B-tree prepended at root, or (ii) a B-tree grafted into an A'
subtree. The partition of B's grafting positions exactly matches
the powerset decomposition of of' A' *_GL of' B = Σ_{B₁ ⊆ B} (insertion (of' A') (of' B₁)) *_CK of'(B - B₁). Each summand of
the GL sum, a-rooted via bPlusLin a, yields a corresponding tree
in the NIM enumeration.
Proved from the NIM-level decomposition
Nonplanar.insertionMultiset_singleton_node
(PreLie/InsertionNonplanar.lean).
The derivation identity #
Helpers for bMinusLin_gl_mul_basis #
The OG derivation identity: bMinusLin a is a 1-cocycle
with respect to the GL product:
B-_a (x *_GL y) = ε(x) • B-_a y + B-_a x *_GL y.
Both sides are bilinear in (x, y) (product is bundled bilinear), so
basis extensionality reduces to bMinusLin_gl_mul_basis.
Duality recurrences #
The base and step cases of the GL/CK duality induction
(Coproduct/PruningDuality.lean): ε is multiplicative for the GL
product, and pairing against B⁺ₐ z unfolds through the B⁺/B⁻ adjoint
and the derivation identity bMinusLin_gl_mul.
ε is multiplicative for the GL product #
The cardinality preservation lemma Nonplanar.insertionMultiset_card_eq
(every F' ∈ NIM(A, B) has |F'| = |A|) and its planar substrate
RoseTree.Pathed.insertionForest_length now live in
Linglib.Core.Algebra.RootedTree.PreLie.InsertionNonplanar.
The counit ε on CK is multiplicative for the GL product: both sides
of ε (x ⋆ y) = ε x · ε y are bilinear (product is bundled), so basis
extensionality reduces to counit_gl_mul_basis.
Phase D's pairing-side recurrence #
The pairing-side recurrence: ⟨X ⋆ Y, B+_a z⟩ unfolds via the B+/B-
adjoint + the derivation identity:
⟨X ⋆ Y, B+_a z⟩ = ε(X) · ⟨B-_a Y, z⟩ + ⟨B-_a X ⋆ Y, z⟩.