Associativity of the Grossman-Larson product via Oudom-Guin 2004 Lemma 2.10 #
@cite{oudom-guin-2008} @cite{foissy-typed-decorated-rooted-trees-2018}
Closes GrossmanLarson.mul_assoc_basis (and thus mul_assoc) via the
direct algebraic argument of Oudom-Guin (arXiv:math/0404457) §2,
Lemma 2.10 — the canonical paragraph-1 construction in pre-Lie / Hopf
algebra theory. Does not require PBW.
Structure #
The proof reduces to two algebraic identities on H = ConnesKreimer R (Nonplanar α)
(viewed as the symmetric algebra S(L) where L = InsertionAlgebra):
insertion_mul_distrib(Prop 2.7.iii):(AB) ∘ C = (A ∘ C_(1))(B ∘ C_(2))— multi-graft distributes over the disjoint-union product via the shuffle coproduct.insertion_assoc_shuffled(Prop 2.7.v):(A ∘ B) ∘ C = A ∘ ((B ∘ C_(1)) C_(2))— multi-graft is "associative" up to shuffle re-indexing.
Both are stated in basis form using Multiset.powerset (the explicit form of the
shuffle Δ on each summand). Lemma 2.10's chain then closes
mul_assoc_basis in a few rewrites + cocommutativity of the powerset sum.
Why this approach #
The Oudom-Guin construction gives an associative product on S(L) for ANY
pre-Lie algebra L. The proof is purely algebraic — no PBW, no
combinatorial bijection at the insertionMultiset level. Closing
mul_assoc_basis this way produces upstream-worthy substrate (currently
absent from mathlib's pre-Lie module).
Status #
DEPRECATED 2026-05-16 as the active path. See
scratch/pivot_to_prelie_pbw.md and Linglib/Core/Algebra/PreLie/ OudomGuinCirc.lean. The basis-level chain mul_assoc_basis_via_oudom_guin
attempts to prove Prop 2.7.iii / 2.7.v combinatorially over forests; the
pivoted approach proves them at the abstract S(L) level (where Prop
2.7.iii is by definition and Prop 2.7.v is a 10-line induction), then
specializes.
Files in this layer that remain useful:
§1 insertion_mul_distrib(Prop 2.7.iii at basis level) — proven and reusable as a sanity check or specialization target for the abstract result.§3cocommutativity helpers — generic, reusable.
Files DEPRECATED (sorries here are NOT on the GL-associativity critical path under the pivot):
§2 insertion_assoc_shuffled— reduces toinsertionMultiset_assoc(A3.3 sorry). Will be derived from abstract Prop 2.7.v after the pivot's Q1-Q5 lands.§4b mul_assoc_basis_via_oudom_guin— the chain proof. Replaced bymul_assoc_basis_via_prelie_pbw(future, derived fromOudomGuinCirc.oudomGuinStar_assoc+ Q5 bridge).
[UPSTREAM] candidate via the pivoted route, not this file.
§1: Prop 2.7.iii — ∘ distributes over disjoint union via shuffle Δ #
The shuffle coproduct decomposition on each forest argument C is realized
explicitly as the sum over C.powerset of the partition (C₁, C - C₁).
The proof of Prop 2.7.iii at the GL/CK level reduces to a combinatorial
identity on Nonplanar.insertionMultiset (= NIM), which we state
separately and prove by descent from the planar insertionForest.
Deep substrate: multi-graft into a disjoint union of host forests
decomposes as a Multiset.bind over guest partitions. This is the
combinatorial heart of Prop 2.7.iii at the basis level.
NIM(A + B, C) = Σ_{C₁ ⊆ C} {X_A + X_B : X_A ∈ NIM(A, C₁), X_B ∈ NIM(B, C-C₁)}
Proved via descent through Planar.Pathed.hostBucketSum and the powerset
bridge Planar.Pathed.listChoices_bridge_powerset_paired, plus
insertionForest_msform_invariance_guests to bridge planar guests with
canonical Quotient.out representatives.
Prop 2.7.iii (Oudom-Guin 2004): for basis forests A, B, C, the
multi-graft of (A · B) (disjoint-union product) into C distributes
as a sum over partitions of C, with each part inserted into A vs B
independently.
(A · B) ∘ C = Σ_{C₁ ⊆ C} (A ∘ C₁) · (B ∘ (C - C₁))
Proved from insertionMultiset_add_host + bilinearity of CK's
disjoint-union product ·.
§2: Prop 2.7.v — ∘ "associativity" up to shuffle Δ #
The headline combinatorial identity: when grafting C into (A ∘ B),
each tree of C can land at an A-vertex (preserved) or a B-vertex
(from the inserted B). This splits C into "going into B" (which becomes
guests of B in a recursive multi-graft) vs "going directly to A as
siblings of B" (after B has been multi-grafted).
Deep substrate: the combinatorial heart of Prop 2.7.v at the
basis level. Iterated multi-graft NIM(NIM(A,B), C) re-indexes as
a triple-bind over partitions of C.
(NIM A B).bind (X ↦ NIM X C) =
C.powerset.bind (C₁ ↦ (NIM B C₁).bind (X' ↦ NIM A (X' + (C - C₁))))
Each tree of C either lands at an A-vertex (in the
"sibling-of-B" piece C - C₁) or at a B-vertex (in the
"guest-of-B" piece C₁, after B has been multi-grafted with that
piece). The triple-bind structure on the RHS sums over the
partition C₁ + (C - C₁) = C, then over multi-grafted-B-trees
X' ∈ NIM B C₁, then over the A-side insertions of the resulting
forest X' + (C - C₁).
TODO: prove by descent from Planar.Pathed.insertionForest's
associativity (Foissy 2021 §5), lifted through Nonplanar.mk + Perm
invariance. Major substrate, parallel to insertionMultiset_add_host.
Prop 2.7.v (Oudom-Guin 2004): for basis forests A, B, C,
(A ∘ B) ∘ C = A ∘ Σ_{C₁ ⊆ C} (B ∘ C₁) · (C - C₁)
The substantive combinatorial heart. Restates the multi-graft "associativity": grafting C into (A with B grafted in) equals grafting "B with the going-into-B portion of C grafted in, alongside the going-directly-to-A portion of C" into A.
Proved from insertionMultiset_assoc (the NIM-level triple-bind
identity) + bilinearity of insertion and of'_add.
§3: Cocommutativity of the shuffle sum #
The sum-over-powerset is symmetric under the partition swap
(C₁, C - C₁) ↔ (C - C₁, C₁), since Multiset.powerset is closed under
complement. This is the "cocommutativity of Δ" component of Lemma 2.10.
Cocommutativity of shuffle Δ: a sum over C.powerset is invariant
under the partition swap.
Specifically: Σ_{C₁ ⊆ C} f(C₁, C - C₁) = Σ_{C₁ ⊆ C} f(C - C₁, C₁)
where the implicit complementation is a bijection on C.powerset.
Used in Lemma 2.10's chain to reindex one of the three triple-partition
sums for B_(2) ∘ C matching.
§4: Closing mul_assoc_basis via Oudom-Guin Lemma 2.10's chain #
The 6-line algebraic chain:
(A * B) * C = (((A ∘ B_(1)) B_(2)) ∘ C_(1)) C_(2) — def of *
= ((A ∘ B_(1)) ∘ C_(1))(B_(2) ∘ C_(2)) C_(3) — insertion_mul_distrib
= (A ∘ ((B_(1) ∘ C_(1)) C_(2)))(B_(2) ∘ C_(3)) C_(4) — insertion_assoc_shuffled
= (A ∘ ((B_(1) ∘ C_(1)) C_(3)))(B_(2) ∘ C_(2)) C_(4) — powerset_partition_swap (on C-trio)
= A * ((B ∘ C_(1)) C_(2)) — def of *
= A * (B * C)
The trio re-indexing on C uses powerset_partition_swap to swap the
"goes into B_(1)" piece of C with the "goes into B_(2)" piece, which
re-pairs the four-way C-partition into the right form for the RHS.
§4a: Generalized building blocks #
The chain manipulates GL elements that are themselves sums of basis
vectors (the output of insertion, a sum-over-partition, ...). To keep
the chain's rewrites compositional, we lift two basis-form identities to
LinearMap-general form via standard linearity arguments.
The lifts are routine Finsupp.induction_linear (zero / additive /
scalar-of-basis) reductions to the basis form.
Push X * of' G to the explicit powerset sum form for ANY X.
Generalization of of'_mul_of' + productForest unfolding to non-basis
LEFT factor.
Stated via product (the bilinear underlying map of *) to avoid
Finsupp/GrossmanLarson type-alias mismatches in the induction.
Corollary: mul_of'_sum_form (the * form, given by mul_def).
LEFT-form distributivity of * over Multiset.sum:
(of' A) * (Σ s) = Σ ((of' A) * s_i). The Grossman-Larson product
* is bilinear (via product : GL →ₗ[R] GL →ₗ[R] GL), so pushing
through Multiset.sum is straightforward — the Mul instance
rewires * as product, and product (of' A) is a LinearMap.
Mirror of insertion_sum_right but for the GL product. Used in
Lemma 2.10's chain to expand (of' A) * (B * C) after substituting
B * C as a sum-form.
insertion distributes over a Multiset.sum in its first argument
(since the LinearMap on the first arg pushes through Multiset.sum).
insertion distributes over a Multiset.sum in its second argument.
Generalized insertion_mul_distrib: the bracketed LEFT factor of
μ(X, of' Y) may be any GL element. Reduces by linearity in X to
the basis case insertion_mul_distrib.
Generalized insertion_assoc_shuffled: the LEFT factor of the outer
iterated insertion may be ANY GL element. Reduces by linearity to
the basis case.
§4b: Lemma 2.10's chain — mul_assoc_basis proved #
The chain expands (of'A * of'B) * of'C step-by-step:
(of'A * of'B) * of'C = productForest (of'A * of'B) C(bymul_of')of'A * of'B = productForest (of'A) B(byof'_mul_of'); expand both levels ofproductForestto nested sums.- Apply
insertion_mul_distrib_gento split eachinsertion(μ(...), of'C₁)along a sub-partitionC₂ ⊆ C₁. - Apply
insertion_assoc_shuffled(basis form is enough — the LEFT factor at this point isinsertion (of' A) (of' B₁), which only becomes a sum after the assoc-rewrite ofinsertion_assoc_shuffled_gen, but here we're at fixedB₁so the basis form applies). - After all these rewrites, the LHS has a four-way C-partition:
C₂, C₁ - C₂, C - C₁plus another implicitB-derived split. - Re-index the C-partition via
powerset_partition_swap. - Similarly expand the RHS, observe that after
powerset_partition_swapthe two expressions are syntactically the same multiset sum.
Helpers for the chain proof #
Each helper expresses one stage of the LHS or RHS expansion.
Bridge between LHS and RHS NIM forms #
After lhs_after_assoc + rhs_quintuple_form, both sides are NIM-bind sums
over partitions of F₂ and F₃. The bridge uses the labeled host
decomposition lemma: summing over (B₁ ⊆ F₂, X' ∈ NIM B₁ D', YB ∈ NIM (F₂-B₁) (C₁'-D'))
gives a multiset of (X', YB) pairs that matches (Z, P_Z) ↦ (P_Z, Z-P_Z)
for Z ∈ NIM F₂ C₁'.
This is essentially insertionMultiset_add_host "labeled" — it tracks not just
which trees of Z came from grafting into B₁ vs F₂-B₁ at the multiset-quotient
level, but as a labeled structure.
The bijection works because each tree of Z = X' + YB ∈ NIM F₂ C₁' corresponds
to a unique tree of F₂ (via the multi-graft semantics), so picking P_Z ⊆ Z
determines B₁ ⊆ F₂ (the corresponding sub-multiset) uniquely.