Grossman-Larson Hopf algebra on forests of nonplanar rooted trees

@cite{grossman-larson-1989} @cite{foissy-typed-decorated-rooted-trees-2018} @cite{marcolli-chomsky-berwick-2025}

The Grossman-Larson product ⋆ is the associative non-commutative product on ConnesKreimer R (Nonplanar α), dual to the disjoint-union product. Together with the appropriate coproduct, it yields a Hopf algebra dual to the Connes-Kreimer Hopf algebra.

MCB targets

The GL framework is the unification that lets MCB's three coproducts (Δ^c, Δ^d, Δ^ρ) share one substrate (see memory/project_mcb_unification_rationale.md). Specifically:

• Lemma 1.2.10 (Δ^c bialgebra on V(F_{SO_0})): closed via the GL-CK duality once R.5/R.6/R.7 sorries land. See Coproduct/TraceNonplanar.lean.
• Lemma 1.2.11 (Δ^ρ Hopf algebra on V(\tilde F_{SO_0})): currently has a parallel proof in Coproduct/PruningNonplanar.lean (Foissy clean coassoc); R.8 will redo via GL duality and delete the parallel.
• Lemma 1.7.3 (Insertion Lie Algebra of §1.7 = Lie algebra of primitives in H^∨ after 1 − α quotient): direct consequence of the GL-dual Lie bracket, with MCB Def 1.7.1's binary ◁_e being the binary specialization (NOT a parallel algebra; see feedback_mcb_section_1_7_not_foissy.md).
• Δ^d (MCB Def 1.2.5): falls out as a different extraction policy
  • projection from the same framework (NOT a parallel substrate; see project_mcb_unification_rationale.md).

Construction

For trees T₁, T₂ : Nonplanar α:

• The insertion operator T₁ • T₂ sums over each vertex v of T₁ the tree obtained by grafting T₂ at v as a new child. Reduces to Nonplanar.insertSum T₁ T₂ from PreLie/Nonplanar.lean (whose convention is insertSum T_host T_graft).
• For a single tree T and a forest F, F • T is the forest obtained by replacing one occurrence of a tree S ∈ F with S augmented by T grafted at one of its vertices: F • T = Σ_{S ∈ F, v ∈ V(S)} (F.erase S + {S[v ↦ T]}). Implemented as insertTreeForest.
• For a multi-tree operand G_forest, the multi-tree insertion F • G is defined as the all-at-once sum over assignments of each tree in G to a vertex of the original F. Importantly, this is NOT the iterated single-tree insertion: those don't commute (see feedback_inserttree_does_not_commute.md). The correct definition is F • G_forest = Σ_{f : G_forest → V(F)} of' (F with each T ∈ G grafted at f(T)), implemented as Planar.insertionForest in MultiGraft.lean and lifted to H as insertion below.

The Grossman-Larson product is given by Foissy 2021 Theorem 5.1:

F ⋆ G = Σ_{G₁ ⊆ G_forest} (F • of' G₁) · of' (G_forest - G₁)

where the sum is over sub-multisets of G_forest and · is the disjoint-union product on ConnesKreimer R (Nonplanar α).

Type alias

GrossmanLarson R α is a type alias for ConnesKreimer R (Nonplanar α) that overrides the default disjoint-union Mul with the Grossman-Larson product. Mirrors mathlib's MultiplicativeOpposite pattern: same underlying carrier, different multiplication.

Status

[UPSTREAM] candidate. Skeleton API (basis embeddings, single-tree insertion, multi-tree insertion, GL product, Mul instance), with mul_one and one_mul proved and mul_assoc reduced (via triple Finsupp.addHom_ext) to the basis-vector lemma mul_assoc_basis, which carries the remaining sorry. The Semigroup/Monoid typeclass instances for the GL product are NOT registered until mul_assoc_basis lands — only the forwarding theorems are stated.

The Grossman-Larson Hopf algebra carrier

def RootedTree.GrossmanLarson (R : Type u_1) [CommSemiring R] (α : Type u_2) : Type (max u_2 u_1)

The Hopf algebra of forests of nonplanar rooted trees, equipped (via the Mul instance below) with the Grossman-Larson product.

Equations

• RootedTree.GrossmanLarson R α = RootedTree.ConnesKreimer R (RootedTree.Nonplanar α)

Forwarded module instances

These propagate from the underlying ConnesKreimer carrier without exposing the disjoint-union Mul (which would clash with the Grossman-Larson Mul defined later).

@[implicit_reducible]

noncomputable instance RootedTree.GrossmanLarson.instAddCommMonoid {R : Type u_1} [CommSemiring R] {α : Type u_2} : AddCommMonoid (GrossmanLarson R α)

Equations

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

@[implicit_reducible]

noncomputable instance RootedTree.GrossmanLarson.instModule {R : Type u_1} [CommSemiring R] {α : Type u_2} : Module R (GrossmanLarson R α)

Equations

• RootedTree.GrossmanLarson.instModule = { smul := RootedTree.GrossmanLarson.instModule._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

noncomputable instance RootedTree.GrossmanLarson.instOne {R : Type u_1} [CommSemiring R] {α : Type u_2} : One (GrossmanLarson R α)

Equations

• RootedTree.GrossmanLarson.instOne = { one := RootedTree.GrossmanLarson.instOne._aux_1 }

@[implicit_reducible]

instance RootedTree.GrossmanLarson.instFunLike {R : Type u_1} [CommSemiring R] {α : Type u_2} : FunLike (GrossmanLarson R α) (Forest (Nonplanar α)) R

Equations

• RootedTree.GrossmanLarson.instFunLike = { coe := RootedTree.GrossmanLarson.instFunLike._aux_1, coe_injective' := ⋯ }

Underlying-carrier coercions

The type alias GrossmanLarson R α := ConnesKreimer R (Nonplanar α) makes the carriers definitionally equal, but Lean does not always unfold def for type ascription or instance resolution. Explicit identity-coercion helpers op/unop (mirroring MulOpposite.op / unop from mathlib) let us reach the underlying disjoint-union Mul when defining the GL product, without exposing the disjoint-union Mul on GrossmanLarson R α itself.

def RootedTree.GrossmanLarson.op {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (Nonplanar α)) : GrossmanLarson R α

Reinterpret a ConnesKreimer R (Nonplanar α) element as a GrossmanLarson R α element (identity at the carrier level).

Equations

• RootedTree.GrossmanLarson.op x = x

def RootedTree.GrossmanLarson.unop {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : GrossmanLarson R α) : ConnesKreimer R (Nonplanar α)

Reinterpret a GrossmanLarson R α element as a ConnesKreimer R (Nonplanar α) element (identity at the carrier level).

Equations

• x.unop = x

@[simp]

theorem RootedTree.GrossmanLarson.op_unop {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : GrossmanLarson R α) : op x.unop = x

@[simp]

theorem RootedTree.GrossmanLarson.unop_op {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (Nonplanar α)) : (op x).unop = x

Smart constructors

The basis-embedding constructors are inherited from the underlying ConnesKreimer via definitional equality.

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

Embed a forest as a basis vector.

Equations

• RootedTree.GrossmanLarson.of' F = RootedTree.ConnesKreimer.of' F

noncomputable def RootedTree.GrossmanLarson.ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (t : Nonplanar α) : GrossmanLarson R α

Embed a single tree as a singleton-forest basis vector.

Equations

• RootedTree.GrossmanLarson.ofTree t = RootedTree.ConnesKreimer.ofTree t

@[simp]

theorem RootedTree.GrossmanLarson.of'_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} : of' 0 = 1

Single-tree insertion

insertTreeForest T F : GrossmanLarson R α is the basis-level forest-insertion operator: for each occurrence of a tree S ∈ F (with multiplicity), sum over each grafting summand S' ∈ Nonplanar.insertSum S T (S host, T graft, summed over vertices of S) the basis vector for the resulting forest S ::ₘ F.erase S with S replaced by S'. The convention Nonplanar.insertSum T_host T_graft is fixed by PreLie/Defs.lean (verified against test + card_insertSum_eq_weight).

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

Forest-level single-tree insertion: graft T at one vertex of one tree of F, summed over (tree, vertex).

Equations

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

@[simp]

theorem RootedTree.GrossmanLarson.insertTreeForest_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) : insertTreeForest T 0 = 0

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

ℤ-linear extension of insertTreeForest T to GrossmanLarson R α.

Equations

• RootedTree.GrossmanLarson.insertTree T = Finsupp.linearCombination R (RootedTree.GrossmanLarson.insertTreeForest T)

@[simp]

theorem RootedTree.GrossmanLarson.insertTree_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : Nonplanar α) (F : Forest (Nonplanar α)) : (insertTree T) (of' F) = insertTreeForest T F

theorem RootedTree.GrossmanLarson.insertTreeForest_cons {R : Type u_1} [CommSemiring R] {α : Type u_2} (T S : Nonplanar α) (F : Forest (Nonplanar α)) : insertTreeForest T (S ::ₘ F) = (Multiset.map (fun (S' : Nonplanar α) => of' (S' ::ₘ F)) (S.insertSum T)).sum + op ((of' {S}).unop * (insertTreeForest T F).unop)

Leibniz cons decomposition for insertTreeForest (GL-level form). GL-level corollary of unop_insertTreeForest_cons via the definitional identity of op and unop.

Multi-tree insertion (the insertion operator F • G)

The bilinear operator F • G : GrossmanLarson R α for F G : H inserts each tree of G (counted with multiplicity) at a vertex of the original F. Specifically, for F = of' F_forest and G = of' G_forest:

F • G = Σ_{f : G_forest → V(F_forest)} of' (F_forest with each T ∈ G grafted at f(T))

where the sum is over functions from G_forest's elements to vertices of F_forest (counted with multiplicity).

This is well-defined on G_forest as a multiset because the result is invariant under permutation of G_forest's elements (the function-sum doesn't care about the order of G_forest's indexing).

This is NOT iterated single-tree insertion: insertTree applications do not commute (single-tree insertions add new vertices that subsequent insertions could graft into, breaking permutation-invariance). See feedback_inserttree_does_not_commute.md for the counterexample (F = {leaf a}, T₁ = leaf b, T₂ = node(c, [d]) gives 3 vs 2 summands for the two orders) and the correct semantics. The earlier scaffold that defined insertForest via Multiset.foldr of insertTree was based on this misreading and has been removed.

Implementation status: defined via Foissy 2021 Theorem 5.1's combinatorial formula at the planar level (PreLie/MultiGraft.lean's Planar.insertionForest), descended through Nonplanar.mk (Nonplanar.insertionMultiset), then bilinear-extended via Finsupp.linearCombination. The substrate invariance theorems (PlanarEquiv on host/guest, Perm on multiset arguments) are stated as sorry'd theorems in MultiGraftNonplanar.lean. Closing those substrate sorries unblocks all of R.5.3/4/5 + R.6 + R.7.

noncomputable def RootedTree.GrossmanLarson.insertionBasis {R : Type u_1} [CommSemiring R] {α : Type u_2} (F_basis G_basis : Forest (Nonplanar α)) : GrossmanLarson R α

Basis-level multi-graft on Multiset forests: each pair (F_basis, G_basis) produces a multiset of grafted forests, summed as basis vectors in H = ConnesKreimer R (Nonplanar α).

Equations

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

noncomputable def RootedTree.GrossmanLarson.insertion {R : Type u_1} [CommSemiring R] {α : Type u_2} : GrossmanLarson R α →ₗ[R] GrossmanLarson R α →ₗ[R] GrossmanLarson R α

The bilinear insertion operator F • G : GrossmanLarson R α. Defined as the bilinear extension of insertionBasis via Finsupp.linearCombination twice (once over G's basis, once over F's via insertionBasisLin).

Equations

• RootedTree.GrossmanLarson.insertion = (Finsupp.linearCombination R RootedTree.GrossmanLarson.insertionBasisLin✝).flip

theorem RootedTree.GrossmanLarson.insertion_of'_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : Forest (Nonplanar α)) : (insertion (of' F)) (of' G) = insertionBasis F G

Bridge: on basis vectors, insertion (of' F) (of' G) = insertionBasis F G. Unfolds the bilinear extension on both basis arguments.

Grossman-Larson product

The associative product F ⋆ G is defined via the Foissy 2021 closed form (sum over sub-multisets of G's underlying forest). The disjoint-union * used inside the definition is the underlying ConnesKreimer multiplication, exposed via type ascription (the def GrossmanLarson R α := ConnesKreimer R (Nonplanar α) makes the ascription a no-op).

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

Forest-level Grossman-Larson product.

Equations

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

noncomputable def RootedTree.GrossmanLarson.product {R : Type u_1} [CommSemiring R] {α : Type u_2} : GrossmanLarson R α →ₗ[R] GrossmanLarson R α →ₗ[R] GrossmanLarson R α

The Grossman-Larson product F ⋆ G : GrossmanLarson R α, bilinear in both arguments.

Equations

• RootedTree.GrossmanLarson.product = (Finsupp.linearCombination R RootedTree.GrossmanLarson.productForestLin✝).flip

Multiplicative structure

The Mul instance is registered now. The Semigroup/Monoid instances are intentionally NOT registered until associativity is proved (registering them prematurely would silently propagate the open sorry through any [Semigroup]-using consumer). The forwarding theorems mul_one, one_mul, mul_assoc are stated for downstream convenience but carry the same sorrys.

@[implicit_reducible]

noncomputable instance RootedTree.GrossmanLarson.instMul {R : Type u_1} [CommSemiring R] {α : Type u_2} : Mul (GrossmanLarson R α)

Equations

• RootedTree.GrossmanLarson.instMul = { mul := fun (x y : RootedTree.GrossmanLarson R α) => (RootedTree.GrossmanLarson.product x) y }

theorem RootedTree.GrossmanLarson.mul_def {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : GrossmanLarson R α) : x * y = (product x) y

theorem RootedTree.GrossmanLarson.of'_mul_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : Forest (Nonplanar α)) : of' F * of' G = (of' F).productForest G

Basis form of the GL product: (of' F) * (of' G) = productForest (of' F) G. Reduces the linearCombination-extended product to the explicit powerset-sum formula.

Unit lemmas

Helper lemmas: insertionBasis F_basis 0 = of' F_basis (Foissy's empty- guest case) and insertionBasis 0 G_basis = if G_basis = 0 then 1 else 0 (empty-host case). These let mul_one and one_mul reduce via the powerset formula.

theorem RootedTree.GrossmanLarson.mul_one {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : GrossmanLarson R α) : F * 1 = F

Right unit. mul_one for the GL product. The powerset (0:Multiset).powerset = {0} collapses to a single summand, which reduces via insertion_one_right to F.

theorem RootedTree.GrossmanLarson.one_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : GrossmanLarson R α) : 1 * F = F

Left unit. one_mul for the GL product. The powerset sum in productForest 1 G_basis collapses to a single non-zero summand at G₁ = 0 (via productForest_one_left), giving of' G_basis. The outer linearCombination then reduces to F.sum single = F.

Bilinearity reduction for mul_assoc

The full statement of mul_assoc is reduced to the basis-vector case mul_assoc_basis via three nested Finsupp.addHom_ext invocations. Each side of F₁ * F₂ * F₃ = F₁ * (F₂ * F₃) is presented as an AddMonoidHom in one of the three variables (the other two held fixed), the two AddMonoidHoms are shown equal by checking on Finsupp.single F r basis elements, and the singleton case reduces via scalar pull-out (through LinearMap.map_smul on product) to the basis-vector mul_assoc_basis statement.

This avoids fighting the GrossmanLarson R α := ConnesKreimer R (Nonplanar α) def-opacity issues that bite Finsupp.induction_linear on GL elements: all the heavy lifting happens at the underlying Finsupp level.

theorem RootedTree.GrossmanLarson.mul_assoc {R : Type u_1} [CommSemiring R] {α : Type u_2} (F₁ F₂ F₃ : GrossmanLarson R α) : F₁ * F₂ * F₃ = F₁ * (F₂ * F₃)

Associativity. Proved by triple bilinearity reduction (Finsupp.addHom_ext thrice) to mul_assoc_basis. The combinatorial heart of associativity lives in mul_assoc_basis; this proof just handles the linear-extension boilerplate.