Bridge: GrossmanLarson product = Oudom-Guin ★ on basis

[OG08] [foissy-2021]

For the pre-Lie algebra L = InsertionAlgebra α (rooted trees with vertex-insertion product), the Oudom-Guin construction gives an associative product ★ on S(L). This file bridges that abstract construction to the concrete Grossman-Larson product on ConnesKreimer R (Nonplanar α) via a canonical algebra isomorphism.

Main definitions

• ckIsoSymmetricAlgebra : algebra equivalence SymmetricAlgebra R (Nonplanar α →₀ R) ≃ₐ[R] ConnesKreimer R (Nonplanar α). Composed from mathlib equivalences: SymmetricAlgebra.equivMvPolynomial (with Finsupp.basisSingleOne) + MvPolynomial σ R = AddMonoidAlgebra R (σ →₀ ℕ) (definitional) + AddMonoidAlgebra.domCongr with Multiset.toFinsupp.symm.

Main theorems

• gl_product_eq_oudomGuinStar (Q5c) : ★ transported via ckIsoSymmetricAlgebra equals the Grossman-Larson product. Proved sorry-free 2026-06-12.

• GrossmanLarson.mul_assoc_basis_via_oudom_guin_pbw (Q6) : closure of mul_assoc_basis for R = ℤ using oudomGuinStar_assoc + Q5c. Proved sorry-free 2026-06-12 (Q3 + Q5c both closed).

Status

Q3 + Q5c + Q6 chain fully proved. Grossman-Larson associativity over ℤ is now established via the OG ★ bridge. #print axioms RootedTree.GrossmanLarson.mul_assoc_basis_via_oudom_guin_pbw yields [propext, Classical.choice, Quot.sound] (no sorryAx).

§1: The carrier iso

SymmetricAlgebra ℤ (Nonplanar α →₀ ℤ) ≃ₐ ConnesKreimer ℤ (Nonplanar α).

This is a direct composition of three mathlib equivalences. Lifts to arbitrary R after InsertionAlgebra is generalized (deferred).

noncomputable def RootedTree.ckIsoSymmetricAlgebra {α : Type u_1} [DecidableEq (Nonplanar α)] : SymmetricAlgebra ℤ (InsertionAlgebra α) ≃ₐ[ℤ] ConnesKreimer ℤ (Nonplanar α)

The carrier iso from SymmetricAlgebra ℤ (InsertionAlgebra α) to ConnesKreimer ℤ (Nonplanar α) = GrossmanLarson ℤ α.

InsertionAlgebra α = Nonplanar α →₀ ℤ has the canonical Finsupp.basisSingleOne indexed by Nonplanar α. Apply SymmetricAlgebra.equivMvPolynomial to get MvPolynomial (Nonplanar α) ℤ, which is definitionally AddMonoidAlgebra ℤ (Nonplanar α →₀ ℕ). Then AddMonoidAlgebra.domCongr via the additive equiv (Nonplanar α →₀ ℕ) ≃+ Multiset (Nonplanar α) (= Multiset.toFinsupp.symm) lands in AddMonoidAlgebra ℤ (Multiset (Nonplanar α)); the final ConnesKreimer.toFinsuppAlgEquiv.symm wraps that bare carrier into the ConnesKreimer structure.

Equations

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

§1b: Basis identification

The iso ckIsoSymmetricAlgebra sends ι (single t 1) to of' (singleton t). This is the basis-level fingerprint we use to translate proofs between SymAlg ℤ (InsertionAlgebra α) and ConnesKreimer ℤ (Nonplanar α).

theorem RootedTree.ckIsoSymmetricAlgebra_ι_single {α : Type u_1} [DecidableEq (Nonplanar α)] (t : Nonplanar α) : ckIsoSymmetricAlgebra ((SymmetricAlgebra.ι ℤ (InsertionAlgebra α)) (Finsupp.single t 1)) = ConnesKreimer.of' {t}

The iso sends ι(single t 1) (basis element of SymAlg) to of'(singleton t) (basis element of CK).

§2: Q5c — bridge oudomGuinStar ↔ GrossmanLarson.product

The two products on ConnesKreimer ℤ (Nonplanar α):

• Disjoint-union (the CommSemiring instance): of' F * of' G = of' (F + G).
• Grossman-Larson (the custom Mul on GrossmanLarson R α): of' F * of' G = Σ_{G₁ ⊆ G} of'(insertion F G₁) · (G - G₁).

The Oudom-Guin ★ on SymmetricAlgebra ℤ (InsertionAlgebra α), transported via ckIsoSymmetricAlgebra, equals the Grossman-Larson product (NOT the disjoint-union one). This is the content of Q5c.

Proof strategy (mirrors Q3's per-tprod closure):

1. Lift Y via algHomL_surjective to Y = algHomL(tprod m a) and induct on m.
2. m = 0: Y = 1. LHS = ckIso X. RHS = (op (ckIso X)) * 1 = op (ckIso X) (via GrossmanLarson.mul_one).
3. m + 1: Y = D · ι v where D = algHomL(tprod m init), v = a(last).
   • LHS via oudomGuinStar_mul_ι_split: ckIso(X ★ (D · ι v)) decomposes into 3 terms involving (X★D)○ιv, (X★D)·ιv, X★(D○ιv).
   • IH at D closes ckIso(X★D) → op(ckIso X) * op(ckIso D).
   • IH summand-wise at D○ιv (which is a sum of m-tprods via oudomGuinCirc_algHomL_tprod_ι) closes X★(D○ιv).
   • Intertwining substrate (ckIso_circ_intertwine_insertion) connects OG ○ to GL insertion.
   • RHS via GL_product_split_mul_ι (the GL Foissy split substrate) decomposes into matching 3 terms.

The proof structure is wired below; the two substrate lemmas ckIso_circ_intertwine_insertion and GL_product_split_mul_ι are both proved sorry-free below.

Sub-substrates for Q5c's substrate 1

Three combinatorial bridges that substrate 1 (ckIso_circ_intertwine_insertion) will use:

1. RoseTree-level bridge: RoseTree.Pathed.insertion T [s] = RoseTree.insertSum T s. Foissy's multi-graft on single-host-single-guest reduces to the simpler insertSum. Uses multiGraft_singleton + listChoices xs 1 = xs.map [·]

   • insertSum_eq_coe_map_insertAt.

2. Nonplanar bridge: Nonplanar.insertionMultiset {t} {s} = (Nonplanar.insertSum t s).map (fun r => {r}). Descends (1) through Quotient.mk using insertionForest_singleton + mk_insertSum.

3. GL Leibniz substrate: insertion(op(A *_CK B))(op(of'({v}))) = op(unop(insertion(op A)(op(of'({v})))) *_CK B) + op(A *_CK unop(insertion(op B)(op(of'({v}))))). Derived from existing Nonplanar.insertionMultiset_add_host (powerset of {v} collapses to the Leibniz split) + bilinear extension.

Each is a standalone combinatorial lemma; all three are proved below.

Local op/unop simp lemmas

GrossmanLarson.op and GrossmanLarson.unop are identity coercions between ConnesKreimer ℤ (Nonplanar α) and GrossmanLarson ℤ α (which are definitionally equal). The forwarded AddCommMonoid and Module ℤ instances make op/unop ℤ-linear; the lemmas below let simp cleanly push op/unop through +, 0, and •.

Substrate 2: GL guest-splitting identity (OG Prop 2.7(ii) GL side)

The four-term identity below is the GL-side analog of Oudom-Guin's splitting lemma (Prop 2.7(ii)). It is the route for the per-tprod m+1 induction of gl_product_eq_oudomGuinStar_tprod, using the singleton case Nonplanar.insertionMultiset_singleton_assoc.

theorem RootedTree.gl_product_eq_oudomGuinStar {α : Type u_1} [DecidableEq (Nonplanar α)] (X Y : SymmetricAlgebra ℤ (InsertionAlgebra α)) : ckIsoSymmetricAlgebra (PreLie.OudomGuinCirc.oudomGuinStar X Y) = GrossmanLarson.op (ckIsoSymmetricAlgebra X) * GrossmanLarson.op (ckIsoSymmetricAlgebra Y)

Q5c: the OG ★ product, transported via ckIsoSymmetricAlgebra, equals the Grossman-Larson product on ConnesKreimer ℤ (Nonplanar α).

Lifted from gl_product_eq_oudomGuinStar_tprod via algHomL_surjective

• TA_linearMap_ext_tprod for Y. Mirrors Q3's lifting pattern (oudomGuinStar_assoc). Proved sorry-free 2026-06-12.

§3: Q6 — mul_assoc_basis for R = ℤ via Q3 + Q5

Combining oudomGuinStar_assoc (Q3, proved sorry-free in OudomGuinCirc.lean) with gl_product_eq_oudomGuinStar (Q5c, proved above) closes mul_assoc_basis for R = ℤ.

theorem RootedTree.GrossmanLarson.mul_assoc_basis_via_oudom_guin_pbw {α : Type u_1} [DecidableEq (Nonplanar α)] (F₁ F₂ F₃ : Forest (Nonplanar α)) : of' F₁ * of' F₂ * of' F₃ = of' F₁ * (of' F₂ * of' F₃)

Q6 (for R = ℤ): associativity of the Grossman-Larson product on basis.

Both Q3 (oudomGuinStar_assoc) and Q5c (gl_product_eq_oudomGuinStar) are proved sorry-free; this theorem combines them.