The B⁻ operator on the symmetric algebra of the insertion algebra

For each color a : α, this file constructs the linear operator B⁻_a on SL = SymmetricAlgebra ℤ (InsertionAlgebra α) from [OG08]: on a generator ι (ofTree t) it returns the product ∏ c ∈ rootChildren t, ι (ofTree c) if rootValue t = a and 0 otherwise, and it vanishes on scalars and on products of two or more generators. It is the SL-side analog of bMinusLin on the Connes-Kreimer side (BMinus.lean).

The operator is built on the tensor algebra degree by degree and descended to SL through SymmetricAlgebra.algHom.

Main definitions

• RootedTree.SymAlg.bMinusLin_SL: the operator B⁻_a : SL →ₗ[ℤ] SL.

Main results

• bMinusLin_SL_ιTree: the defining values on embedded trees.
• iotaTree_node_via_circ: every tree is the circle product of its singleton root with its children-forest, the root-grafting identity displayed in §3.1 of [OG08].
• bMinusLin_SL_oudomGuinStar: the cocycle identity B⁻_a (A ★ B) = ε(A) • B⁻_a B + B⁻_a A ★ B from the proof of Prop 3.2 of [OG08].
• bMinusLin_ckIso: transport of B⁻_a along ckIsoSymmetricAlgebra.

[UPSTREAM] candidate.

References

• [OG08]

Per-tree basis assignment

noncomputable def RootedTree.SymAlg.ιTree {α : Type u_1} (t : Nonplanar α) : SymmetricAlgebra ℤ (InsertionAlgebra α)

Embedding of a single tree into SL: SymmetricAlgebra.ι applied to InsertionAlgebra.ofTree.

Equations

• RootedTree.SymAlg.ιTree t = (SymmetricAlgebra.ι ℤ (RootedTree.InsertionAlgebra α)) (RootedTree.InsertionAlgebra.ofTree t)

noncomputable def RootedTree.SymAlg.psiA_basis {α : Type u_1} (a : α) (t : Nonplanar α) : SymmetricAlgebra ℤ (InsertionAlgebra α)

The value of B⁻_a on a tree t: the SL-product of ι (ofTree c) over the root's children if rootValue t = a, else 0.

Equations

• RootedTree.SymAlg.psiA_basis a t = if t.rootValue = a then (Multiset.map (fun (c : RootedTree.Nonplanar α) => RootedTree.SymAlg.ιTree c) t.rootChildren).prod else 0

Linear extension to the insertion algebra

noncomputable def RootedTree.SymAlg.psiA_L {α : Type u_1} (a : α) : InsertionAlgebra α →ₗ[ℤ] SymmetricAlgebra ℤ (InsertionAlgebra α)

The psiA operator on L: linear extension of psiA_basis via Finsupp.lift.

Equations

• RootedTree.SymAlg.psiA_L a = (Finsupp.lift (SymmetricAlgebra ℤ (RootedTree.InsertionAlgebra α)) ℤ (RootedTree.Nonplanar α)) (RootedTree.SymAlg.psiA_basis a)

@[simp]

theorem RootedTree.SymAlg.psiA_L_ofTree {α : Type u_1} (a : α) (t : Nonplanar α) : (psiA_L a) (InsertionAlgebra.ofTree t) = psiA_basis a t

Per-degree multilinear maps

psiA_multi a n is the Fin n → LL multilinear map that vanishes on n ≠ 1 and applies psiA_L a to the single argument when n = 1.

@[simp]

theorem RootedTree.SymAlg.psiA_multi_one_apply {α : Type u_1} (a : α) (f : Fin 1 → InsertionAlgebra α) : (RootedTree.SymAlg.psiA_multi_one✝ a) f = (psiA_L a) (f 0)

noncomputable def RootedTree.SymAlg.psiA_multi {α : Type u_1} (a : α) (n : ℕ) : MultilinearMap ℤ (fun (x : Fin n) => InsertionAlgebra α) (SymmetricAlgebra ℤ (InsertionAlgebra α))

Per-degree multilinear map. Vanishes outside n = 1.

Equations

• RootedTree.SymAlg.psiA_multi a 0 = 0
• RootedTree.SymAlg.psiA_multi a 1 = RootedTree.SymAlg.psiA_multi_one✝ a
• RootedTree.SymAlg.psiA_multi a n.succ.succ = 0

@[simp]

theorem RootedTree.SymAlg.psiA_multi_zero {α : Type u_1} (a : α) : psiA_multi a 0 = 0

@[simp]

theorem RootedTree.SymAlg.psiA_multi_one_eq {α : Type u_1} (a : α) : psiA_multi a 1 = RootedTree.SymAlg.psiA_multi_one✝ a

@[simp]

theorem RootedTree.SymAlg.psiA_multi_succ_succ {α : Type u_1} (a : α) (n : ℕ) : psiA_multi a (n + 2) = 0

Lifts to tensor powers

noncomputable def RootedTree.SymAlg.psiA_pi {α : Type u_1} (a : α) (n : ℕ) : TensorPower ℤ n (InsertionAlgebra α) →ₗ[ℤ] SymmetricAlgebra ℤ (InsertionAlgebra α)

Per-degree lift of psiA_multi a n to the n-th tensor power.

Equations

• RootedTree.SymAlg.psiA_pi a n = PiTensorProduct.lift (RootedTree.SymAlg.psiA_multi a n)

@[simp]

theorem RootedTree.SymAlg.psiA_pi_tprod {α : Type u_1} (a : α) (n : ℕ) (g : Fin n → InsertionAlgebra α) : (psiA_pi a n) ((PiTensorProduct.tprod ℤ) g) = (psiA_multi a n) g

Assembly across degrees

noncomputable def RootedTree.SymAlg.psiA_graded {α : Type u_1} (a : α) : (DirectSum ℕ fun (n : ℕ) => TensorPower ℤ n (InsertionAlgebra α)) →ₗ[ℤ] SymmetricAlgebra ℤ (InsertionAlgebra α)

The maps psiA_pi a n assembled into a linear map from the direct sum of all tensor powers.

Equations

• RootedTree.SymAlg.psiA_graded a = DirectSum.toModule ℤ ℕ (SymmetricAlgebra ℤ (RootedTree.InsertionAlgebra α)) fun (n : ℕ) => RootedTree.SymAlg.psiA_pi a n

@[simp]

theorem RootedTree.SymAlg.psiA_graded_of {α : Type u_1} (a : α) (n : ℕ) (x : TensorPower ℤ n (InsertionAlgebra α)) : (psiA_graded a) ((DirectSum.of (fun (n : ℕ) => TensorPower ℤ n (InsertionAlgebra α)) n) x) = (psiA_pi a n) x

The tensor-algebra-level operator

noncomputable def RootedTree.SymAlg.psiA_tensor {α : Type u_1} (a : α) : TensorAlgebra ℤ (InsertionAlgebra α) →ₗ[ℤ] SymmetricAlgebra ℤ (InsertionAlgebra α)

The TA-side psiA operator, assembled from per-degree psiA_pi via TensorAlgebra.equivDirectSum.

Equations

• RootedTree.SymAlg.psiA_tensor a = RootedTree.SymAlg.psiA_graded a ∘ₗ TensorAlgebra.equivDirectSum.toLinearMap

@[simp]

theorem RootedTree.SymAlg.psiA_tensor_tprod {α : Type u_1} (a : α) (n : ℕ) (f : Fin n → InsertionAlgebra α) : (psiA_tensor a) ((TensorAlgebra.tprod ℤ (InsertionAlgebra α) n) f) = (psiA_multi a n) f

Definitional bridges

Kernel vanishing

psiA_tensor a vanishes on ker algHomL: it is 0 on every tprod of degree ≥ 2, and any wrapped r * (ι X * ι Y) * d element has degree ≥ 2, so both swap-orderings map to 0.

Descent to the symmetric algebra

noncomputable def RootedTree.SymAlg.bMinusLin_SL {α : Type u_1} (a : α) : SymmetricAlgebra ℤ (InsertionAlgebra α) →ₗ[ℤ] SymmetricAlgebra ℤ (InsertionAlgebra α)

The B⁻_a operator on SL ([OG08]), descended from psiA_tensor a through algHomL via Submodule.liftQ.

Equations

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

Basic identities

theorem RootedTree.SymAlg.bMinusLin_SL_algHomL {α : Type u_1} (a : α) (z : TensorAlgebra ℤ (InsertionAlgebra α)) : (bMinusLin_SL a) (PreLie.OudomGuinCircConstruct.algHomL z) = (psiA_tensor a) z

bMinusLin_SL a factors through algHomL: bMinusLin_SL a (algHomL z) = psiA_tensor a z.

@[simp]

theorem RootedTree.SymAlg.bMinusLin_SL_ι {α : Type u_1} (a : α) (x : InsertionAlgebra α) : (bMinusLin_SL a) ((SymmetricAlgebra.ι ℤ (InsertionAlgebra α)) x) = (psiA_L a) x

bMinusLin_SL a (ι x) = psiA_L a x.

@[simp]

theorem RootedTree.SymAlg.bMinusLin_SL_ιTree {α : Type u_1} (a : α) (t : Nonplanar α) : (bMinusLin_SL a) (ιTree t) = psiA_basis a t

bMinusLin_SL a (ιTree t) = psiA_basis a t.

@[simp]

theorem RootedTree.SymAlg.bMinusLin_SL_one {α : Type u_1} (a : α) : (bMinusLin_SL a) 1 = 0

B⁻_a vanishes on 1.

Length-one extraction

bMinusLin_SL extracts only the length-one component:

• bMinusLin_SL_ι_mul_ι: vanishing on products of two generators.
• bMinusLin_SL_ι_mul_eps: bMinusLin_SL a (ι Z * Y) = ε(Y) • bMinusLin_SL a (ι Z).
• bMinusLin_SL_ι_star: bMinusLin_SL a (ι Y ★ B) = psiA_L a (circByT_total Y B).

Transport along ckIsoSymmetricAlgebra

The transport identity bMinusLin a (ckIso X) = ckIso (bMinusLin_SL a X), via an ε-twisted Leibniz rule for the disjoint-union product on the Connes-Kreimer side.

Counit-Leibniz rule on forests

bMinusBasis a (F + G) splits according to which of F, G is empty: it equals bMinusBasis a G when F is empty, bMinusBasis a F when G is empty, and 0 when both are nonempty.

Counit-Leibniz rule on forest products

The transport identity

bMinusLin a (ckIso X) = ckIso (bMinusLin_SL a X) for all X : SL. The proof inducts on X via SymmetricAlgebra.induction. Two private helpers are added in service of the mul case: a CK-side counit-Leibniz rule (bMinusLin_mul_eps, bilinear extension of bMinusLin_of'_mul_of') and a bridge identifying counit ∘ ckIso with algebraMapInv (counit_ckIso).

Relocation candidates: bMinusLin_mul_eps belongs in BMinus.lean (CK substrate); deferred to avoid concurrent edits.

theorem RootedTree.SymAlg.bMinusLin_ckIso {α : Type u_1} [DecidableEq (Nonplanar α)] (a : α) (X : SymmetricAlgebra ℤ (InsertionAlgebra α)) : (GrossmanLarson.bMinusLin a) (ckIsoSymmetricAlgebra X) = ckIsoSymmetricAlgebra ((bMinusLin_SL a) X)

Transport of B⁻_a along ckIsoSymmetricAlgebra: bMinusLin a (ckIso X) = ckIso (bMinusLin_SL a X). Induction on X via SymmetricAlgebra.induction: the algebraMap/add cases are linearity, the ι x case routes through ckIsoSymmetricAlgebra_ι_single

• ckIso_prod_ιTree, and the mul case combines bMinusLin_SL_mul_eps (SL side) with bMinusLin_mul_eps + counit_ckIso (CK side).

Trees as circle products of root and children

The root-grafting identity displayed in §3.1 of [OG08]: in the free pre-Lie algebra of rooted trees,

• ∘ T₁ ... T_n  =  [tree with root • and children T₁, ..., T_n]

Here InsertionAlgebra α is the free pre-Lie algebra on α, and the identity takes the form ι (ofTree (node a A')) = ι (ofTree (leaf a)) ○ ∏ c ∈ A', ι (ofTree c) (iotaTree_node_via_circ).

theorem RootedTree.SymAlg.leaf_eq_node_zero {α : Type u_1} (a : α) : Nonplanar.leaf a = Nonplanar.node a 0

leaf a = node a 0: the singleton-vertex tree is the empty-children node.

Helpers for the cancellation argument

The tree-decomposition identity

theorem RootedTree.SymAlg.iotaTree_node_via_circ {α : Type u_1} (a : α) (A' : Multiset (Nonplanar α)) : (SymmetricAlgebra.ι ℤ (InsertionAlgebra α)) (InsertionAlgebra.ofTree (Nonplanar.node a A')) = (PreLie.OudomGuinCirc.oudomGuinCirc ((SymmetricAlgebra.ι ℤ (InsertionAlgebra α)) (InsertionAlgebra.ofTree (Nonplanar.leaf a)))) (Multiset.map (fun (c : Nonplanar α) => (SymmetricAlgebra.ι ℤ (InsertionAlgebra α)) (InsertionAlgebra.ofTree c)) A').prod

Every nonplanar tree is the circle product of its singleton-vertex root with its children-forest:

ι (ofTree (node a A')) = ι (ofTree (leaf a)) ○ ∏ c ∈ A', ι (ofTree c)

This is the root-grafting identity displayed in §3.1 of [OG08]. The induction is on the children-multiset cardinality; weight is conserved by subtree grafting and is not a valid measure.

The circle-product identity for psiA_L

psiA_L_circByT_total_eq: psiA_L a (circByT_total Y B) = oudomGuinStar (psiA_L a Y) B, consumed by the ι case of bMinusLin_SL_oudomGuinStar.

Helpers for the cocycle mul case

The cocycle identity

theorem RootedTree.SymAlg.bMinusLin_SL_oudomGuinStar {α : Type u_1} [DecidableEq (Nonplanar α)] (a : α) (A B : SymmetricAlgebra ℤ (InsertionAlgebra α)) : (bMinusLin_SL a) (PreLie.OudomGuinCirc.oudomGuinStar A B) = SymmetricAlgebra.algebraMapInv A • (bMinusLin_SL a) B + PreLie.OudomGuinCirc.oudomGuinStar ((bMinusLin_SL a) A) B

The cocycle identity for B⁻_a with respect to ★, from the proof of Prop 3.2 of [OG08]:

bMinusLin_SL a (A ★ B) = ε(A) • bMinusLin_SL a B + bMinusLin_SL a A ★ B

SL-side analog of the Connes-Kreimer-side bMinusLin_gl_mul.