The operator B⁻

This file defines the linear map B⁻_a on ConnesKreimer R (UnorderedTree α). It sends a one-tree forest whose root is labelled a to the forest of that root's children, and every other basis forest to 0, so it undoes the grafting operator B⁺_a of Coproduct/Pruning.lean. Oudom and Guin use the pair B⁺, B⁻ to identify the Grossman–Larson algebra with their product on a symmetric algebra (their Proposition 4.1).

Under the symmetry-weighted pairing, B⁻_a is the transpose of B⁺_a, and it satisfies B⁻_a (x ⋆ y) = ε(x) • B⁻_a y + B⁻_a x ⋆ y for the Grossman–Larson product. With the multiplicativity of the counit (GrossmanLarson.counit_product), these drive the induction that proves the duality of Coproduct/PruningDuality.lean.

Main definitions

• GrossmanLarson.bMinusLin: the linear map B⁻_a; bMinusTree and bMinusBasis are its values on trees and on basis forests.

Main results

• GrossmanLarson.bMinusLin_pairing_adjoint, GrossmanLarson.isAdjointPair_bMinusLin_bPlusLin: ⟨B⁻_a x, y⟩ = ⟨x, B⁺_a y⟩.
• GrossmanLarson.insertion_of'_singleton_node: grafting into the tree node a A is B⁺_a (A ⋆ B).
• GrossmanLarson.bMinusLin_gl_mul: B⁻_a (x ⋆ y) = ε(x) • B⁻_a y + B⁻_a x ⋆ y.
• GrossmanLarson.pairing_apply_bPlus_gl_mul: ⟨x ⋆ y, B⁺_a z⟩ in terms of B⁻_a.

References

• [OG08]
• [Foi21]

B⁻_a on trees and basis forests

noncomputable def GrossmanLarson.bMinusTree {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (a : α) (T : UnorderedTree α) : ConnesKreimer R (UnorderedTree α)

bMinusTree a T is the forest of children of T when its root is labelled a, else 0.

Equations

• GrossmanLarson.bMinusTree a T = if T.value = a then ConnesKreimer.of' T.children else 0

@[simp]

theorem GrossmanLarson.bMinusTree_node {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (a : α) (F : UnorderedTree.Forest (UnorderedTree α)) : bMinusTree a (UnorderedTree.node a F) = ConnesKreimer.of' F

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

bMinusBasis a F is bMinusTree a T when F = {T}, and 0 otherwise. It is stated through card, map and sum so that it is a function on multisets.

Equations

• GrossmanLarson.bMinusBasis a F = if Multiset.card F = 1 then (Multiset.map (GrossmanLarson.bMinusTree a) F).sum else 0

@[simp]

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

@[simp]

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

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

bMinusBasis a vanishes on basis forests other than a single tree with root a.

The linear map

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

bMinusLin a is the linear extension of bMinusBasis a.

Equations

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

@[simp]

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

Transpose of B⁺_a

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

On basis forests, ⟨B⁻_a (of' F), of' G⟩ = ⟨of' F, B⁺_a (of' G)⟩; both sides count the symmetries of F when F = {node a G}.

theorem GrossmanLarson.isAdjointPair_bMinusLin_bPlusLin {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (a : α) : pairing.IsAdjointPair pairing ⇑(bMinusLin a) ⇑(ConnesKreimer.bPlusLin a)

B⁻_a and B⁺_a are an adjoint pair for the symmetry-weighted pairing.

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

⟨B⁻_a x, y⟩ = ⟨x, B⁺_a y⟩.

B⁻_a and the Grossman–Larson product

The identity B⁻_a (x ⋆ y) = ε(x) • B⁻_a y + B⁻_a x ⋆ y reduces to basis forests x = of' A. If A is not a single tree with root a, both sides vanish or agree by counting trees. If A = {node a A'}, grafting into node a A' is B⁺_a of the product A' ⋆ B (UnorderedTree.insertionMultiset_singleton_node).

theorem GrossmanLarson.insertion_of'_singleton_node {R : Type u_1} [CommSemiring R] {α : Type u_2} (a : α) (A B : UnorderedTree.Forest (UnorderedTree α)) : (insertion (ConnesKreimer.of' {UnorderedTree.node a A})) (ConnesKreimer.of' B) = (ConnesKreimer.bPlusLin a) ((product (ConnesKreimer.of' A)) (ConnesKreimer.of' B))

Grafting of' B into the single tree node a A is B⁺_a of the Grossman–Larson product of' A ⋆ of' B: each guest is either a new child of the root or grafted into a tree of A.

theorem GrossmanLarson.bMinusLin_gl_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (a : α) (x y : ConnesKreimer R (UnorderedTree α)) : (bMinusLin a) ((product x) y) = ConnesKreimer.counit x • (bMinusLin a) y + (product ((bMinusLin a) x)) y

B⁻_a (x ⋆ y) = ε(x) • B⁻_a y + B⁻_a x ⋆ y.

theorem GrossmanLarson.pairing_apply_bPlus_gl_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq α] (a : α) (X Y z : ConnesKreimer R (UnorderedTree α)) : (pairing ((product X) Y)) ((ConnesKreimer.bPlusLin a) z) = ConnesKreimer.counit X * (pairing ((bMinusLin a) Y)) z + (pairing ((product ((bMinusLin a) X)) Y)) z

⟨X ⋆ Y, B⁺_a z⟩ = ε(X) · ⟨B⁻_a Y, z⟩ + ⟨B⁻_a X ⋆ Y, z⟩.