Single-tree pre-Lie product insertSum on RoseTree α and Nonplanar α

[foissy-typed-decorated-rooted-trees-2018] [chapoton-livernet-2001] [MCB25]

The vertex-grafting pre-Lie product on n-ary rooted trees: for trees T₁, T₂, T₁ ◁ T₂ is the multiset of all trees obtained by grafting T₂ as a new child of some vertex of T₁:

T₁ ◁ T₂ = Σ_{v ∈ V(T₁)} graft(v, T₁, T₂)

This file contains both the ordered definition (Foissy 2018 Prop 2.2, Chapoton-Livernet) on RoseTree α and its descent through Nonplanar.mk to the nonplanar carrier.

Reference

[foissy-typed-decorated-rooted-trees-2018] Proposition 2.2 defines the multiple pre-Lie product on D-decorated T-typed rooted trees (D = decoration set, T = edge type set). Specialized to T = {*} (single edge type) and decoration set α, this is exactly insertSum.

[chapoton-livernet-2001] introduced the original CL pre-Lie product on undecorated rooted trees, of which the present construction is the decorated extension.

Relation to MCB §1.7

[MCB25] Definition 1.7.1 (book p. 77) defines a DIFFERENT pre-Lie product on nonplanar BINARY rooted trees with leaf labels in SO_0 (internal vertices unlabeled), via edge subdivision. The two are distinct algebras on distinct carriers — neither is a specialization of the other. Both satisfy the abstract pre-Lie identity (mathlib's RightPreLieAlgebra); a future binary substrate file would add a separate RightPreLieAlgebra instance for MCB §1.7.

File scope

• §1: insertSum definition + simp lemmas + leaf case.
• §2: Decomposition (insertSum_eq_coe_map_insertAt).
• §3: Cardinality (card_insertSum_eq_numNodes), derived from §2.
• §4: Cons-decomposition projection helpers (descent).
• §5: Right invariance (PermEquiv on T₂).
• §6: List-side perm + componentwise PermEquiv invariance.
• §7: Left invariance (PermStep / PermEquiv on T₁).
• §8: Native Nonplanar.insertSum via Quotient.lift₂.
• §9: Quotient-unfolding lemma + Nonplanar cardinality.
• §10: Sanity tests.

Sibling files:

• Path.lean / Insert.lean — path-based vertex enumeration + grafting (Pathed.vertices, Pathed.insertAt).
• Insertion.lean — multi-tree multi-vertex grafting (Foissy 2021).
• Algebra.lean — RightPreLieAlgebra ℤ instance.

insertSum — the vertex-grafting product

Mutually recursive on (RoseTree, List RoseTree). Each summand of insertSum T₁ T₂ corresponds to a choice of vertex v in T₁; the corresponding tree replaces v's children list cs with T₂ :: cs. This is a paramorphic recursion — the original children list is reused to rebuild the grafted node — so it is written by hand rather than as a fold.

def RoseTree.insertSum {α : Type u_1} : RoseTree α → RoseTree α → Multiset (RoseTree α)

The pre-Lie product T₁ ◁ T₂ on RoseTree α (vertex grafting): the multiset of all trees obtained by grafting T₂ as a new child of some vertex of T₁.

Equations

• (RoseTree.node a cs).insertSum x✝ = RoseTree.node a (x✝ :: cs) ::ₘ Multiset.map (fun (cs' : List (RoseTree α)) => RoseTree.node a cs') (RoseTree.insertSumList cs x✝)

def RoseTree.insertSumList {α : Type u_1} : List (RoseTree α) → RoseTree α → Multiset (List (RoseTree α))

Auxiliary: graft T₂ inside one of the entries of a children list, returning the multiset of resulting children-lists (one per vertex inside the list).

Equations

• RoseTree.insertSumList [] x✝ = 0
• RoseTree.insertSumList (c :: cs) x✝ = Multiset.map (fun (c' : RoseTree α) => c' :: cs) (c.insertSum x✝) + Multiset.map (fun (cs' : List (RoseTree α)) => c :: cs') (RoseTree.insertSumList cs x✝)

def RoseTree.«term_◁_» : Lean.TrailingParserDescr

Notation T₁ ◁ T₂ for insertSum T₁ T₂. The right-triangular Unicode glyph matches Foissy's typesetting. Scoped to avoid clashing with mathlib's LeftPreLieRing notation.

Equations

• RoseTree.«term_◁_» = Lean.ParserDescr.trailingNode `RoseTree.«term_◁_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◁ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem RoseTree.insertSum_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) (T₂ : RoseTree α) : (node a cs).insertSum T₂ = node a (T₂ :: cs) ::ₘ Multiset.map (fun (cs' : List (RoseTree α)) => node a cs') (insertSumList cs T₂)

@[simp]

theorem RoseTree.insertSumList_nil {α : Type u_1} (T₂ : RoseTree α) : insertSumList [] T₂ = 0

@[simp]

theorem RoseTree.insertSumList_cons {α : Type u_1} (c : RoseTree α) (cs : List (RoseTree α)) (T₂ : RoseTree α) : insertSumList (c :: cs) T₂ = Multiset.map (fun (c' : RoseTree α) => c' :: cs) (c.insertSum T₂) + Multiset.map (fun (cs' : List (RoseTree α)) => c :: cs') (insertSumList cs T₂)

@[simp]

theorem RoseTree.insertSum_leaf {α : Type u_1} (a : α) (T₂ : RoseTree α) : (leaf a).insertSum T₂ = {node a [T₂]}

A leaf has exactly one summand: graft T₂ at the root.

Decomposition — insertSum via Pathed.vertices + Pathed.insertAt

Bridge lemma between the recursive (Multiset) formulation of insertSum in §1 and the per-path (List) formulation in Path.lean / Insert.lean. The lemma is the basis for the pre-Lie identity proof in Algebra.lean: each summand of insertSum T₁ T₂ is uniquely identified by a path into T₁.

theorem RoseTree.insertSum_eq_coe_map_insertAt {α : Type u_1} (T₁ T₂ : RoseTree α) : T₁.insertSum T₂ = ↑(List.map (fun (p : Pathed.Path) => Pathed.insertAt p T₂ T₁) (Pathed.vertices T₁))

Decomposition lemma: T₁ ◁ T₂ equals the multiset of Pathed.insertAt p T₂ T₁ for p ranging over Pathed.vertices T₁.

theorem RoseTree.insertSumList_eq_coe_map_pathInsertAt_aux {α : Type u_1} (a : α) (pre cs : List (RoseTree α)) (T₂ : RoseTree α) : Multiset.map (fun (cs' : List (RoseTree α)) => node a (pre ++ cs')) (insertSumList cs T₂) = ↑(List.map (fun (p : Pathed.Path) => Pathed.insertAt p T₂ (node a (pre ++ cs))) (Pathed.verticesAux pre.length cs))

Auxiliary: with pre siblings before the cs-tail being grafted in, children-list grafting through pre-prefixed RoseTree.node a equals the path-based insertions at offset pre.length into the original host RoseTree.node a (pre ++ cs).

Cardinality — card (T₁ ◁ T₂) = T₁.numNodes

Each vertex of T₁ contributes one summand. Both counts fall out of the §2 decomposition: card (T₁ ◁ T₂) = (vertices T₁).length = T₁.numNodes, so no numNodes-mirroring induction is needed.

theorem RoseTree.card_insertSum_eq_length_vertices {α : Type u_1} (T₁ T₂ : RoseTree α) : (T₁.insertSum T₂).card = (Pathed.vertices T₁).length

The number of summands in T₁ ◁ T₂ equals (vertices T₁).length.

theorem RoseTree.card_insertSum_eq_numNodes {α : Type u_1} (T₁ T₂ : RoseTree α) : (T₁.insertSum T₂).card = T₁.numNodes

The number of summands in T₁ ◁ T₂ equals T₁.numNodes (total vertex count).

Sanity tests at compile time

Descent of insertSum through Nonplanar.mk

The descent layer: lift RoseTree.insertSum to Nonplanar α via Quotient.lift₂, requiring invariance under PermEquiv on both arguments.

Cons-decomposition of insertSumList-projection

Helper lemma used by both §5 right-invariance and §6 list permutation proofs. The cons case of insertSumList cs T₂ splits into a per-head grafting (in insertSum c T₂) plus a per-tail grafting (in insertSumList tail T₂); after projection through mk ∘ node a, the two halves are clean two-summand decompositions with simpler wrappers than the raw Multiset.map_map form.

Right invariance — T₂ → T₂'

If T₂ ≡ T₂' (PermEquiv), then (T₁ ◁ T₂).map mk = (T₁ ◁ T₂').map mk for any T₁. Mutually inducted with the children-list version insertSumList.

theorem RootedTree.Nonplanar.insertSum_permEquiv_right {α : Type u_1} (T₁ : RoseTree α) {T₂ T₂' : RoseTree α} (h : T₂.PermEquiv T₂') : Multiset.map mk (T₁.insertSum T₂) = Multiset.map mk (T₁.insertSum T₂')

Right invariance for insertSum.

List-side mk-projection of insertSumList

Two key properties of (insertSumList cs T₂).map (mk ∘ .node a): Perm-invariance in cs and componentwise PermEquiv-invariance.

Left invariance — T₁ → T₁' via PermStep induction

theorem RootedTree.Nonplanar.insertSum_permStep_left {α : Type u_1} {T₁ T₁' : RoseTree α} (h : T₁.PermStep T₁') (T₂ : RoseTree α) : Multiset.map mk (T₁.insertSum T₂) = Multiset.map mk (T₁'.insertSum T₂)

Left invariance for insertSum under a single PermStep on T₁.

EqvGen lift to PermEquiv

theorem RootedTree.Nonplanar.insertSum_permEquiv_left {α : Type u_1} {T₁ T₁' : RoseTree α} (h : T₁.PermEquiv T₁') (T₂ : RoseTree α) : Multiset.map mk (T₁.insertSum T₂) = Multiset.map mk (T₁'.insertSum T₂)

Left invariance under PermEquiv on T₁. Standard EqvGen recipe.

Native Nonplanar.insertSum via Quotient.lift₂

def RootedTree.Nonplanar.insertSum {α : Type u_1} : Nonplanar α → Nonplanar α → Multiset (Nonplanar α)

The vertex-grafting pre-Lie product on Nonplanar α: lifted from the ordered RoseTree.insertSum via Quotient.lift₂, using the invariance lemmas from §5 and §7.

Equations

• RootedTree.Nonplanar.insertSum = Quotient.lift₂ (fun (t₁ t₂ : RoseTree α) => Multiset.map RootedTree.Nonplanar.mk (t₁.insertSum t₂)) ⋯

def RootedTree.Nonplanar.«term_◁_» : Lean.TrailingParserDescr

Notation T₁ ◁ T₂ for Nonplanar.insertSum T₁ T₂. Scoped to the Nonplanar namespace to coexist with the tree-level ◁.

Equations

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

Quotient-unfolding lemma + Nonplanar cardinality

@[simp]

theorem RootedTree.Nonplanar.mk_insertSum {α : Type u_1} (t₁ t₂ : RoseTree α) : (mk t₁).insertSum (mk t₂) = Multiset.map mk (t₁.insertSum t₂)

Quotient unfolding: Nonplanar.insertSum (mk t₁) (mk t₂) is the multiset of nonplanar grafting summands obtained by projecting the ordered grafting summands.

theorem RootedTree.Nonplanar.card_insertSum_eq_numNodes {α : Type u_1} (T₁ T₂ : Nonplanar α) : (T₁.insertSum T₂).card = T₁.numNodes

The number of summands of T₁ ◁ T₂ equals T₁.numNodes, i.e., the nonplanar tree-vertex count of T₁.

Sanity tests