B- operator on ConnesKreimer R (Nonplanar α) and the B+/B- pairing adjoint

[OG08] [foissy-typed-decorated-rooted-trees-2018]

The B-_a operator is the transpose of B+_a (defined in Coproduct/PruningNonplanar.lean) under the symmetry-weighted pairing (defined in GrossmanLarsonPairing.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 containing an a-labeled root tree to the children-forest of that tree, and gives 0 otherwise (on multi-tree forests, empty forest, or singletons with a different root label).

Headline result

• bMinusLin_pairing_adjoint: ⟨B-_a x, y⟩ = ⟨x, B+_a y⟩ for all a : α, x y : ConnesKreimer R (Nonplanar α).

This is the OG Prop 3.2 substrate: the transpose property anchors the duality argument for B-(A ∗ B) = ε(A) B-(B) + B-(A) ∗ B ([OG08] §3.2; deferred to a sibling file).

Why this file (OG-faithful Q5c route)

Per [[feedback-substrate2-not-og]], Q5c's substrate 2 was a linglib-invented identity that embeds A3.3 difficulty. OG's actual route in Prop 3.2 uses B+/B- duality with Δ^ρ instead. This file provides the B+/B- adjoint property — the foundation of that route.

bMinusBasis via per-list branching with perm-invariance

noncomputable def RootedTree.GrossmanLarson.bMinusBasis {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : ConnesKreimer R (Nonplanar α)

The B-_a operator on basis-key forests. Defined via Quotient.liftOn from bMinusList, using bMinusList_perm for well-definedness.

Equations

• RootedTree.GrossmanLarson.bMinusBasis a F = Quotient.liftOn F (RootedTree.GrossmanLarson.bMinusList✝ a) ⋯

@[simp]

theorem RootedTree.GrossmanLarson.bMinusBasis_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : bMinusBasis a 0 = 0

@[simp]

theorem RootedTree.GrossmanLarson.bMinusBasis_singleton_node {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : bMinusBasis a {Nonplanar.node a F} = of' F

bMinusLin a — linear extension

noncomputable def RootedTree.GrossmanLarson.bMinusLin {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) : ConnesKreimer R (Nonplanar α) →ₗ[R] ConnesKreimer R (Nonplanar α)

The B-_a linear map: linear extension of bMinusBasis via Finsupp.lift.

Equations

• RootedTree.GrossmanLarson.bMinusLin a = RootedTree.ConnesKreimer.linearLift (RootedTree.GrossmanLarson.bMinusBasis a)

@[simp]

theorem RootedTree.GrossmanLarson.bMinusLin_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) : (bMinusLin a) (of' F) = bMinusBasis a F

B+/B- pairing adjoint

theorem RootedTree.GrossmanLarson.bMinusLin_pairing_adjoint_basis {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F G : Forest (Nonplanar α)) : (pairing ((bMinusLin a) (of' F))) (of' G) = (pairing (of' F)) ((ConnesKreimer.bPlusLin a) (of' G))

Adjoint of bPlusLin a w.r.t. the symmetry-weighted pairing. On basis: ⟨B-_a (of' F), of' G⟩ = ⟨of' F, B+_a (of' G)⟩.

theorem RootedTree.GrossmanLarson.bMinusLin_pairing_adjoint {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (x y : ConnesKreimer R (Nonplanar α)) : (pairing ((bMinusLin a) x)) y = (pairing x) ((ConnesKreimer.bPlusLin a) y)

B+/B- adjoint under the symmetry-weighted pairing: ⟨B-_a x, y⟩ = ⟨x, B+_a y⟩ for all a, x, y. Reduces to bMinusLin_pairing_adjoint_basis via bilinearity.

Phase C: OG-style 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 side (under the algebra iso ckIso), this becomes 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 to B-_a (of' B) = B-_a (of' B).
• |A| ≥ 2: both sides 0 by length grading (B-_a vanishes on non-singletons).
• |A| = 1 with root label ≠ a: both sides 0 (B-_a kills non-a-rooted singletons).
• |A| = 1 with 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.

Phase C main theorem

theorem RootedTree.GrossmanLarson.bMinusBasis_eq_zero_of_not_singleton_a {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (F : Forest (Nonplanar α)) (h : ¬∃ (G' : Forest (Nonplanar α)), F = {Nonplanar.node a G'}) : bMinusBasis a F = 0

bMinusLin a is the constant function 0 on basis forests that are not singleton-a-rooted. Helper for the easy cases of Phase C.

Helpers for bMinusLin_gl_mul_basis

theorem RootedTree.GrossmanLarson.bMinusLin_gl_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (x y : ConnesKreimer R (Nonplanar α)) : (bMinusLin a) (op x * op y) = ConnesKreimer.counit x • (bMinusLin a) y + (op ((bMinusLin a) x) * op y).unop

Phase C main theorem (OG-style): 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.

Reduces by ConnesKreimer.induction_linear (twice) to the basis case bMinusLin_gl_mul_basis.