InsertionAlgebra α — pre-Lie algebra on (Nonplanar α) →₀ ℤ

@cite{foissy-typed-decorated-rooted-trees-2018} @cite{chapoton-livernet-2001}

The bilinear extension of Nonplanar.insertSum to the free ℤ-module (Nonplanar α) →₀ ℤ gives a RightPreLieAlgebra ℤ instance, realizing Foissy 2018 Proposition 2.2 specialized to a single edge type (matching the Nonplanar α carrier from PreLie/Nonplanar.lean).

Carrier

def InsertionAlgebra (α : Type*) := Nonplanar α →₀ ℤ

A type alias (à la MonoidAlgebra k G := G →₀ k) gives a fresh slot for a custom non-pointwise Mul. The custom multiplication is the bilinear extension of Nonplanar.insertSum, which on singletons satisfies single t 1 * single s 1 = (Nonplanar.insertSum t s).toFinsupp.mapℤ (where the multiset of grafting summands is converted to a Finsupp, each summand contributing 1).

The pre-Lie identity

Foissy 2018 Definition 2.1 (page 6) defines a multiple pre-Lie algebra by the identity x •_{t'} (y •_t z) − (x •_{t'} y) •_t z = x •_t (z •_{t'} y) − (x •_t z) •_{t'} y

Specializing to a single edge type collapses both subscripts and gives: x • (y • z) − (x • y) • z = x • (z • y) − (x • z) • y

i.e., (x • y) • z − x • (y • z) = (x • z) • y − x • (z • y), which is exactly mathlib's RightPreLieRing axiom associator x y z = associator x z y.

Proof structure (Foissy 2018 Proposition 2.2)

By bilinearity, suffices on singletons. For T₁ T₂ T₃ : Nonplanar α:

1. Decompose (T₁ • T₂) • T₃ as Σ_{v ∈ V(T₁), u ∈ V(insertAt v T₂)} insertAt u T₃ (insertAt v T₂).
2. Classify each u via Vertex.classifyEquiv (R.3b §9):
   • lifted g (g ∈ V(T₂)): contribution = insertAt v (insertAt g T₃) T₁ by insertAt_lift_eq_nested. Sums to T₁ • (T₂ • T₃). Cancels in (T₁ • T₂) • T₃ − T₁ • (T₂ • T₃).
   • preserved w (w ∈ V(T₁), w ≠ v): contribution = insertAt (preserveOf v w h T₂) T₃ (insertAt v T₂) = insertAt (preserveOf w v h.symm T₃) T₂ by insertAt_commute_diff. This re-keys (v, w) ↔ (w, v): summand of (T₁ • T₃) • T₂ in the symmetric class.
   • sourceSelf (u = v itself, v carries both T₂ and T₃ as new children): contribution = node a (T₃ :: T₂ :: cs) (for v = root). Symmetric counterpart: node a (T₂ :: T₃ :: cs). Equal as Nonplanar trees (children-list permutation), making this case cancellable in Nonplanar but not Planar.

The Nonplanar-only swap-cancellation in the sourceSelf case is what distinguishes the Nonplanar pre-Lie algebra from the (non-existent) Planar one.

Mathlib upstream considerations

InsertionAlgebra is noncomputable because Nonplanar α is a Quotient and DecidableEq (Nonplanar α) requires canonicalization (typically via [LinearOrder α] and recursive children-list sorting). For mathlib upstream, a sibling DecidableEq (Nonplanar α) instance under [LinearOrder α] would let consumers opt into computability; that's deferred to a separate file (Combinatorics/RootedTree/Nonplanar/Decidable.lean?).

The pattern matches mathlib's LieAlgebra.UniversalEnveloping and TensorProduct: noncomputable for "abstract algebraic structure where evaluation isn't the point."

Main definitions

• InsertionAlgebra α — the carrier Nonplanar α →₀ ℤ with custom Mul.
• ofTree / ofMultiset — smart constructors for basis vectors.
• instMul — bilinear extension of Nonplanar.insertSum.

Main theorems

• assoc_symm — the pre-Lie identity (associator symmetry on the right).
• instRightPreLieRing / instRightPreLieAlgebra — typeclass instances.

Carrier + module instances

def RootedTree.InsertionAlgebra (α : Type u_1) : Type u_1

The insertion algebra on Nonplanar α: the free ℤ-module on Nonplanar α with multiplication given by the bilinear extension of Nonplanar.insertSum. Defined as a type alias of Nonplanar α →₀ ℤ (the MonoidAlgebra pattern) so that we can attach a custom Mul.

Equations

• RootedTree.InsertionAlgebra α = (RootedTree.Nonplanar α →₀ ℤ)

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instAddCommGroup {α : Type u_1} : AddCommGroup (InsertionAlgebra α)

Equations

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

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instModule {α : Type u_1} : Module ℤ (InsertionAlgebra α)

Equations

• RootedTree.InsertionAlgebra.instModule = { toDistribMulAction := (AddCommGroup.toIntModule (RootedTree.InsertionAlgebra α)).toDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

instance RootedTree.InsertionAlgebra.instInhabited {α : Type u_1} : Inhabited (InsertionAlgebra α)

Equations

• RootedTree.InsertionAlgebra.instInhabited = { default := RootedTree.InsertionAlgebra.instInhabited._aux_1 }

@[implicit_reducible]

instance RootedTree.InsertionAlgebra.instFunLike {α : Type u_1} : FunLike (InsertionAlgebra α) (Nonplanar α) ℤ

Equations

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

Smart constructor + custom Mul

ofTree t is the basis vector Finsupp.single t 1. The custom Mul is the bilinear extension of Nonplanar.insertSum, computed via Finsupp.sum.

noncomputable def RootedTree.InsertionAlgebra.ofTree {α : Type u_1} (t : Nonplanar α) : InsertionAlgebra α

The basis vector for a single tree.

Equations

• RootedTree.InsertionAlgebra.ofTree t = Finsupp.single t 1

theorem RootedTree.InsertionAlgebra.ofTree_apply {α : Type u_1} (t : Nonplanar α) : ofTree t = Finsupp.single t 1

noncomputable def RootedTree.InsertionAlgebra.ofMultiset {α : Type u_1} (m : Multiset (Nonplanar α)) : InsertionAlgebra α

Convert a Multiset (Nonplanar α) to an InsertionAlgebra α by summing each element as a singleton basis vector. Bypasses Multiset.toFinsupp (which requires DecidableEq) by using Multiset.sum over (Finsupp.single · 1)-valued maps.

Equations

• RootedTree.InsertionAlgebra.ofMultiset m = (Multiset.map (fun (t : RootedTree.Nonplanar α) => Finsupp.single t 1) m).sum

@[simp]

theorem RootedTree.InsertionAlgebra.ofMultiset_zero {α : Type u_1} : ofMultiset 0 = 0

@[simp]

theorem RootedTree.InsertionAlgebra.ofMultiset_singleton {α : Type u_1} (t : Nonplanar α) : ofMultiset {t} = ofTree t

@[simp]

theorem RootedTree.InsertionAlgebra.ofMultiset_add {α : Type u_1} (m₁ m₂ : Multiset (Nonplanar α)) : ofMultiset (m₁ + m₂) = ofMultiset m₁ + ofMultiset m₂

@[simp]

theorem RootedTree.InsertionAlgebra.ofMultiset_cons {α : Type u_1} (t : Nonplanar α) (m : Multiset (Nonplanar α)) : ofMultiset (t ::ₘ m) = ofTree t + ofMultiset m

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instMul {α : Type u_1} : Mul (InsertionAlgebra α)

The bilinear extension of Nonplanar.insertSum: for singletons, single t 1 * single s 1 = ofMultiset (Nonplanar.insertSum t s). Defined via Finsupp.sum, which gives a clean bilinear extension over (Nonplanar α →₀ ℤ).

Equations

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

theorem RootedTree.InsertionAlgebra.mul_def {α : Type u_1} (x y : InsertionAlgebra α) : x * y = Finsupp.sum x fun (t : Nonplanar α) (a : ℤ) => Finsupp.sum y fun (s : Nonplanar α) (b : ℤ) => (a * b) • ofMultiset (t.insertSum s)

@[simp]

theorem RootedTree.InsertionAlgebra.ofTree_mul_ofTree {α : Type u_1} (t s : Nonplanar α) : ofTree t * ofTree s = ofMultiset (t.insertSum s)

The headline computation: on singletons, multiplication is the bilinear extension of Nonplanar.insertSum.

Bilinearity + NonUnitalNonAssocRing

The custom Mul is bilinear by construction (built from Finsupp.sum). Standard lemmas: zero_mul, mul_zero, left_distrib, right_distrib. With these, InsertionAlgebra α becomes a NonUnitalNonAssocRing.

@[simp]

theorem RootedTree.InsertionAlgebra.zero_mul {α : Type u_1} (x : InsertionAlgebra α) : 0 * x = 0

@[simp]

theorem RootedTree.InsertionAlgebra.mul_zero {α : Type u_1} (x : InsertionAlgebra α) : x * 0 = 0

theorem RootedTree.InsertionAlgebra.add_mul {α : Type u_1} (x y z : InsertionAlgebra α) : (x + y) * z = x * z + y * z

theorem RootedTree.InsertionAlgebra.mul_add {α : Type u_1} (x y z : InsertionAlgebra α) : x * (y + z) = x * y + x * z

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instMulZeroClass {α : Type u_1} : MulZeroClass (InsertionAlgebra α)

Equations

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

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instDistrib {α : Type u_1} : Distrib (InsertionAlgebra α)

Equations

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

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instNonUnitalNonAssocSemiring {α : Type u_1} : NonUnitalNonAssocSemiring (InsertionAlgebra α)

Equations

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

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instNonUnitalNonAssocRing {α : Type u_1} : NonUnitalNonAssocRing (InsertionAlgebra α)

Equations

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

Source-self swap PlanarEquiv

The pre-Lie identity reduces, after the lifted/preserved cancellations, to a mk-equality between two singleton trees that differ by a children-list swap at the source vertex e. Realized by structural induction on e : Path + t₁ : Planar α: a swapAtRoot PlanarStep at the root-path case, recurse_lift at the in-child cases. This is the only Nonplanar-specific cancellation in the pre-Lie identity proof; everything else holds at the planar level.

Multiset bilinearity helpers

The custom Mul is bilinear, so multiplying an ofMultiset against a single basis vector (or vice versa) yields an ofMultiset of a bind of the underlying grafting product. These helpers chain into the double-grafting form needed by the pre-Lie identity.

Triple-product unfolding

Two glue lemmas reducing ofTree T₁ * ofTree T₂ * ofTree T₃ (and the right-associated form) to ofMultiset of a Multiset.bind chain. These are the chain ofTree_mul_ofTree → ofMultiset_mul_ofTree (left-assoc) and ofTree_mul_ofTree → ofTree_mul_ofMultiset (right-assoc). Used in assoc_symm_singleton (§5) to drop into Multiset arithmetic.

Path-indexed bind reformulation

Two reformulation lemmas that convert (t₁ ◁ t₂).bind (T ↦ T ◁ t₃) and (Pathed.vertices t₁).bind (fun e => map (insertAt (lift e q) t₃) to the clean path-indexed and cross-term forms used by assoc_symm_planar.

Planar 3-class identity

The planar Multiset (Nonplanar α) equality at the heart of the pre-Lie identity. After Quotient.inductionOn₃ reduces to planar t₁ t₂ t₃, the pre-Lie associator's two halves rearrange to this form. The proof uses vertices_insertAt_decomp to split each (insertAt v t₂) ◁ t₃ into preserved + sourceSelf + lifted classes:

• Lifted cancels with the cross term (LHS₂ / RHS₂) via insertAt_lift_eq_nested + Multiset.bind_bind.
• Preserved cancels at PLANAR level (no Nonplanar quotient needed) via insertAt_commute_diff + (v, w) ↔ (w, v) re-keying.
• SourceSelf cancels at NONPLANAR level via mk_insertAt_sourceSelf_swap (the only Nonplanar-specific step).

Singleton-reduction lemma

The pre-Lie identity (x*y)*z - x*(y*z) = (x*z)*y - x*(z*y) is bilinear in each of x, y, z. By bilinearity, it suffices to prove on singletons ofTree T₁, ofTree T₂, ofTree T₃ for T₁ T₂ T₃ : Nonplanar α.

This section sets up the singleton reduction; the actual identity proof is in §6.

theorem RootedTree.InsertionAlgebra.assoc_symm_singleton {α : Type u_1} (T₁ T₂ T₃ : Nonplanar α) : ofTree T₁ * ofTree T₂ * ofTree T₃ - ofTree T₁ * (ofTree T₂ * ofTree T₃) = ofTree T₁ * ofTree T₃ * ofTree T₂ - ofTree T₁ * (ofTree T₃ * ofTree T₂)

The pre-Lie identity on singletons. After Quotient.inductionOn₃ reduces to planar t₁, t₂, t₃, the four triple products unfold via ofTree_triple_left/right to ofMultiset of planar bind chains projected through Nonplanar.mk. The combinatorial identity is assoc_symm_planar.

Scalar pull-out for the custom Mul

The custom Mul is bilinear in the ℤ-coefficients: (c • x) * y = c • (x * y) and x * (c • y) = c • (x * y). Proved by direct unfolding of mul_def + Finsupp.sum_smul_index' + Finsupp.smul_sum. These are needed by the basis case of assoc_symm's triple Finsupp.induction_linear.

Pre-Lie identity

The headline. By bilinearity, reduces to assoc_symm_singleton.

theorem RootedTree.InsertionAlgebra.assoc_symm {α : Type u_1} (x y z : InsertionAlgebra α) : x * y * z - x * (y * z) = x * z * y - x * (z * y)

The pre-Lie identity on InsertionAlgebra α: (x * y) * z - x * (y * z) = (x * z) * y - x * (z * y).

By trilinearity (three nested Finsupp.addHom_ext), reduces to assoc_symm_three_singletons.

RightPreLieRing instance

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instRightPreLieRing {α : Type u_1} : RightPreLieRing (InsertionAlgebra α)

The headline algebraic structure: InsertionAlgebra α is a right pre-Lie ring, with the Vertex.classifyEquiv-driven pre-Lie identity of assoc_symm.

Equations

• RootedTree.InsertionAlgebra.instRightPreLieRing = { toNonUnitalNonAssocRing := RootedTree.InsertionAlgebra.instNonUnitalNonAssocRing, assoc_symm' := ⋯ }

RightPreLieAlgebra ℤ instance

InsertionAlgebra α is a RightPreLieAlgebra over ℤ: the ℤ-module structure plus scalar-tower / smul-comm-class follows from the ℤ-bilinear Mul.

@[implicit_reducible]

noncomputable instance RootedTree.InsertionAlgebra.instRightPreLieAlgebra {α : Type u_1} : RightPreLieAlgebra ℤ (InsertionAlgebra α)

Equations

• RootedTree.InsertionAlgebra.instRightPreLieAlgebra = { toModule := RootedTree.InsertionAlgebra.instModule, toIsScalarTower := ⋯, toSMulCommClass := ⋯ }