Insertion Lie algebra ≅ primitives in the dual Hopf algebra (MCB Lemma 1.7.3)

[MCB25]

The architectural payoff of Phase E.3 (R.5–R.9): the GL/CK duality framework is designed precisely to make MCB Lemma 1.7.3 expressible.

MCB Lemma 1.7.3 (book p. 78): The insertion Lie algebra of Lemma 1.7.2 is the Lie algebra of primitive elements in the dual Hopf algebra of the Hopf algebra of workspaces.

Proof sketch (book p. 79): take dual basis δ_F (delta on forests); primitives in H^∨ are the δ_T (single-tree only); the dual product δ_{T_1} ⋆ δ_{T_2} expands as Σ_T c^T_{T_1,T_2} δ_T where c^T_{T_1,T_2} counts insertions; the Lie bracket on primitives matches the insertion bracket from §1.7.2.

Substrate (general, mathlib upstream candidate)

• Bialgebra.IsDualPrimitive — a linear functional L : H →ₗ[R] R is "primitive in the dual" iff L(xy) = L(x)·ε(y) + ε(x)·L(y). Equivalent to being primitive in H^∨ viewed as a coalgebra dual to H's algebra.
• Bialgebra.dualPrimitives — the submodule of dual primitives.
• Bialgebra.convBracket — the convolution Lie bracket [L₁, L₂] := L₁ ⋆ L₂ - L₂ ⋆ L₁ using mathlib's WithConv.

These are sorry-free general lemmas; potential mathlib upstream.

Specialization to Connes-Kreimer

• deltaSingleton T — the dual basis element δ_T : CK R (Nonplanar α) →ₗ[R] R extracting the coefficient of the singleton forest {T}.
• deltaSingleton_isDualPrimitive — δ_T is a dual primitive (sorry-free).
• mcb_lemma_1_7_3_dualPrimitive — corollary that the convolution Lie bracket of two single-tree deltas is again a dual primitive (sorry-free).
• mcb_lemma_1_7_3_explicit — the full Lemma 1.7.3 in Δ^ρ form: [δ_{T₁}, δ_{T₂}](of' {T}) = countSingleCutsRho T T₁ T₂ − countSingleCutsRho T T₂ T₁. Substrate-faithful analog of MCB's c^T_{T₁,T₂} − c^T_{T₂,T₁} using Δ^ρ (deletion) semantics rather than Δ^c (trace-leaf). The Δ^c version follows via the strip bijection in Coproduct/DeletionNonplanar.lean.

What this file does NOT do

• Does not formalize the 1-α quotient (would make H a genuine connected Hopf algebra; not needed for the statement on the bialgebra).
• Does not state a full Lie algebra isomorphism between the insertion Lie algebra and dual primitives (only closure under bracket).
• Does not establish the bijection of book Figure 1.6 (would require R.5.5 + R.7 sorries to close first).

Status

[UPSTREAM] candidate for the Bialgebra.IsDualPrimitive / dualPrimitives / convBracket substrate (sorry-free, including IsDualPrimitive.convBracket_mem — closure under bracket).

§1: Dual primitives — general Bialgebra substrate

def Bialgebra.IsDualPrimitive {R : Type u_1} [CommSemiring R] {H : Type u_2} [Semiring H] [Bialgebra R H] (L : H →ₗ[R] R) : Prop

A linear functional L : H →ₗ[R] R is primitive in the dual of a bialgebra H if it satisfies the derivation-like identity: L(x * y) = L(x) · counit(y) + counit(x) · L(y).

Equivalently, L is primitive in the bialgebra-theoretic sense when viewed as an element of the dual H^∨: the coproduct on H^∨ is dual to the product on H, so Δ_{H^∨}(L) = L ⊗ ε + ε ⊗ L reads as the above identity after pairing against x ⊗ y.

Equations

• Bialgebra.IsDualPrimitive L = ∀ (x y : H), L (x * y) = L x * CoalgebraStruct.counit y + CoalgebraStruct.counit x * L y

def Bialgebra.dualPrimitives {R : Type u_1} [CommSemiring R] {H : Type u_2} [Semiring H] [Bialgebra R H] : Submodule R (H →ₗ[R] R)

The submodule of dual primitives in H →ₗ[R] R.

Equations

• Bialgebra.dualPrimitives = { carrier := {L : H →ₗ[R] R | Bialgebra.IsDualPrimitive L}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Bialgebra.mem_dualPrimitives {R : Type u_1} [CommSemiring R] {H : Type u_2} [Semiring H] [Bialgebra R H] (L : H →ₗ[R] R) : L ∈ dualPrimitives ↔ IsDualPrimitive L

§2: Convolution Lie bracket

Sweedler representation of a product

Coalgebra.Repr.mul builds a Repr for x * y in a Bialgebra from Reprs of x and y, via the bialgebra axiom comul (xy) = comul x * comul y. This is the key helper for any Sweedler-style proof that works with products in a bialgebra; missing from mathlib.

noncomputable def Coalgebra.Repr.mul {R : Type u_1} {H : Type u_2} [CommSemiring R] [Semiring H] [Bialgebra R H] {x y : H} {ιx : Type u_3} {ιy : Type u_4} (𝓡x : Repr R x ιx) (𝓡y : Repr R y ιy) : Repr R (x * y) (ιx × ιy)

Sweedler representation of x * y: given Reprs 𝓡x : Repr R x and 𝓡y : Repr R y in a bialgebra H, the product x * y has Repr indexed by 𝓡x.index ×ˢ 𝓡y.index with left (i, j) = 𝓡x.left i * 𝓡y.left j and right (i, j) = 𝓡x.right i * 𝓡y.right j.

Mathlib gap.

Equations

• 𝓡x.mul 𝓡y = { index := 𝓡x.index ×ˢ 𝓡y.index, left := fun (p : ιx × ιy) => 𝓡x.left p.1 * 𝓡y.left p.2, right := fun (p : ιx × ιy) => 𝓡x.right p.1 * 𝓡y.right p.2, eq := ⋯ }

noncomputable def Bialgebra.convBracket {R : Type u_1} [CommRing R] {H : Type u_2} [Semiring H] [Bialgebra R H] (L₁ L₂ : H →ₗ[R] R) : H →ₗ[R] R

The convolution Lie bracket on linear functionals H →ₗ[R] R, using mathlib's WithConv convolution product: [L₁, L₂] := L₁ ⋆ L₂ - L₂ ⋆ L₁.

Equations

• Bialgebra.convBracket L₁ L₂ = (WithConv.toConv L₁ * WithConv.toConv L₂ - WithConv.toConv L₂ * WithConv.toConv L₁).ofConv

theorem Bialgebra.IsDualPrimitive.convBracket_mem {R : Type u_1} [CommRing R] {H : Type u_2} [Semiring H] [Bialgebra R H] {L₁ L₂ : H →ₗ[R] R} (h₁ : IsDualPrimitive L₁) (h₂ : IsDualPrimitive L₂) : IsDualPrimitive (convBracket L₁ L₂)

Closure of dual primitives under the convolution Lie bracket.

Proof structure (Sweedler-style, standard textbook result). Using IsDualPrimitive on L₁ and L₂, expand (L₁ ⋆ L₂)(xy) = (L₁ ⋆ L₂)(x) · ε(y) + ε(x) · (L₁ ⋆ L₂)(y) + L₁(x) · L₂(y) + L₂(x) · L₁(y) via Sweedler notation (Lemma IsDualPrimitive.convMul_apply_mul). The "cross terms" L₁(x)·L₂(y) + L₂(x)·L₁(y) are symmetric in (L₁, L₂), so they cancel in the difference (L₁ ⋆ L₂)(xy) - (L₂ ⋆ L₁)(xy). The remaining terms are exactly ((L₁ ⋆ L₂) - (L₂ ⋆ L₁))(x) · ε(y) + ε(x) · ((L₁ ⋆ L₂) - (L₂ ⋆ L₁))(y), which is [L₁, L₂](x) · ε(y) + ε(x) · [L₁, L₂](y). ∎

§3: Specialization to Connes-Kreimer + MCB Lemma 1.7.3

noncomputable def RootedTree.ConnesKreimer.deltaSingleton {R : Type u_1} [CommRing R] {α : Type u_2} (T : Nonplanar α) : ConnesKreimer R (Nonplanar α) →ₗ[R] R

The delta functional on a singleton forest: extracts the coefficient of {T} (the forest containing only T) from a Connes-Kreimer element.

Equations

• RootedTree.ConnesKreimer.deltaSingleton T = RootedTree.ConnesKreimer.lcoeff {T}

@[simp]

theorem RootedTree.ConnesKreimer.deltaSingleton_of'_self {R : Type u_1} [CommRing R] [CharZero R] [NoZeroDivisors R] {α : Type u_2} (T : Nonplanar α) : (deltaSingleton T) (of' {T}) = 1

theorem RootedTree.ConnesKreimer.deltaSingleton_of'_other {R : Type u_1} [CommRing R] [CharZero R] [NoZeroDivisors R] {α : Type u_2} (T : Nonplanar α) (F : Forest (Nonplanar α)) (hF : F ≠ {T}) : (deltaSingleton T) (of' F) = 0

theorem RootedTree.ConnesKreimer.deltaSingleton_isDualPrimitive {R : Type u_1} [CommRing R] [CharZero R] [NoZeroDivisors R] {α : Type u_2} (T : Nonplanar α) : Bialgebra.IsDualPrimitive (deltaSingleton T)

The delta functional on a single tree is a dual primitive — i.e., it satisfies δ_T(x * y) = δ_T(x) · ε(y) + ε(x) · δ_T(y).

This is the bialgebraic content of MCB's observation (book p. 79) that primitives in H^∨ are exactly the single-tree deltas.

Proof: bilinear suffices reduction to a basis-pair statement, then smul_mul_smul_comm + ← of'_add factors the scalars out, leaving an unscaled basis identity. The basis identity is closed by case-split on F + G = {T} via Multiset cardinality (singleton forces one factor to be empty, the other to be {T}).

theorem RootedTree.ConnesKreimer.mcb_lemma_1_7_3_dualPrimitive {R : Type u_1} [CommRing R] [CharZero R] [NoZeroDivisors R] {α : Type u_2} (T₁ T₂ : Nonplanar α) : Bialgebra.IsDualPrimitive (Bialgebra.convBracket (deltaSingleton T₁) (deltaSingleton T₂))

MCB Lemma 1.7.3 (dual-primitive closure corollary): the convolution Lie bracket of two single-tree deltas is again a dual primitive, by IsDualPrimitive.convBracket_mem applied to deltaSingleton_isDualPrimitive.

§4: MCB Lemma 1.7.3 (full) — explicit count formula

The substantive bracket-counting form of MCB Lemma 1.7.3. Since our Bialgebra structure uses Δ^ρ (deletion remainder), the count is in terms of Δ^ρ cut summands rather than MCB's Δ^c (trace-leaf) version:

[δ_{T₁}, δ_{T₂}](of' {T}) = countSingleCutsRho T T₁ T₂ − countSingleCutsRho T T₂ T₁

where countSingleCutsRho T T₁ T₂ counts the Δ^ρ cut summands of T whose cut forest is exactly {T₁} and whose remainder is exactly T₂.

This is the substrate-faithful analog of MCB's c^T_{T₁,T₂}. The Δ^c-quotient version (with trace leaves at cut sites) would yield the same count under the bijection between Δ^ρ remainders and Δ^c trunks established in Coproduct/DeletionNonplanar.lean.

noncomputable def RootedTree.ConnesKreimer.countSingleCutsRho {α : Type u_2} (T T₁ T₂ : Nonplanar α) : ℕ

Δ^ρ single-cut count: number of Δ^ρ cut summands of T whose cut forest equals {T₁} and whose remainder tree equals T₂.

Equations

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

theorem RootedTree.ConnesKreimer.deltaSingleton_conv_apply_singleton {R : Type u_1} [CommRing R] [CharZero R] [NoZeroDivisors R] {α : Type u_2} (T T₁ T₂ : Nonplanar α) : (WithConv.toConv (deltaSingleton T₁) * WithConv.toConv (deltaSingleton T₂)).ofConv (of' {T}) = ↑(countSingleCutsRho T T₁ T₂)

The convolution (toConv δ_{T₁} * toConv δ_{T₂}).ofConv evaluated on a single-tree basis vector of' {T} equals the count of Δ^ρ cut summands of T extracting {T₁} and leaving T₂.

theorem RootedTree.ConnesKreimer.mcb_lemma_1_7_3_explicit {R : Type u_1} [CommRing R] [CharZero R] [NoZeroDivisors R] {α : Type u_2} (T T₁ T₂ : Nonplanar α) : (Bialgebra.convBracket (deltaSingleton T₁) (deltaSingleton T₂)) (of' {T}) = ↑(countSingleCutsRho T T₁ T₂) - ↑(countSingleCutsRho T T₂ T₁)

MCB Lemma 1.7.3 (Δ^ρ explicit form): the convolution Lie bracket of two single-tree deltas evaluated on a single-tree basis vector is the antisymmetrized count of single-tree Δ^ρ cuts:

[δ_{T₁}, δ_{T₂}](of' {T}) = countSingleCutsRho T T₁ T₂ − countSingleCutsRho T T₂ T₁

Substrate-faithful analog of the book's c^T_{T₁,T₂} − c^T_{T₂,T₁}. The Δ^c-quotient version (with trace leaves) would yield the same count via the strip bijection in Coproduct/DeletionNonplanar.lean.