The grafting pre-Lie product on rooted trees

This file defines the grafting product T ◁ S of two rooted trees: the multiset of the trees obtained by grafting S onto one vertex of T, that is, by making S a new child of that vertex. Chapoton and Livernet show that this product makes the rooted trees a basis of the free pre-Lie algebra; Foissy extends it to typed decorated trees.

The product is the one-guest case of the multi-insertion insertion T gs, which grafts every guest of gs at once, on planar trees and on nonplanar ones alike. Everything here is read off that general construction: the sum-over-vertices formula, the recursion on the root, and the pre-Lie identity.

Main definitions

• RoseTree.insertSum: the grafting product on planar trees, with notation T ◁ S.
• UnorderedTree.insertSum: the grafting product on nonplanar trees.

Main results

• RoseTree.insertSum_eq_map_multiGraft: T ◁ S sums the graftings of S over the vertices of T.
• RoseTree.insertSum_node: grafting at the root, or recursively inside one child.
• RoseTree.card_insertSum, UnorderedTree.card_insertSum: one summand per vertex of T.
• UnorderedTree.insertSum_bind_insertSum: grafting S₁ into T and then S₂ into the result is grafting S₁ ◁ S₂ into T plus grafting S₁ and S₂ into T at once.
• UnorderedTree.insertSum_assoc_symm: the associator of the grafting product is symmetric in its last two arguments, the right pre-Lie identity.

Implementation notes

The pre-Lie identity holds only once children are unordered: grafting S₁ and then S₂ at one vertex makes the new children [S₂, S₁], where grafting both at once makes them [S₁, S₂].

References

• [CL01]
• [Foi21]

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

The grafting product T ◁ S is the multiset of trees obtained by grafting S as a new first child of one vertex of T.

Equations

• T.insertSum S = T.insertion [S]

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

The grafting product T ◁ S is the multiset of trees obtained by grafting S as a new first child of one vertex of T.

Equations

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

theorem RoseTree.insertSum_eq_map_multiGraft {α : Type u_1} (T S : RoseTree α) : T.insertSum S = ↑(List.map (fun (p : List ℕ) => T.multiGraft [(p, S)]) T.vertices)

T ◁ S sums, over the vertices p of T, the grafting of S at p.

theorem RoseTree.insertSum_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) (S : RoseTree α) : (node a cs).insertSum S = node a (S :: cs) ::ₘ Multiset.map (node a) (insertionForest cs [S])

Grafting into a node either adds a child at the root or grafts inside the children.

@[simp]

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

theorem RoseTree.card_insertSum {α : Type u_1} (T S : RoseTree α) : (T.insertSum S).card = T.numNodes

The pre-Lie identity

theorem RoseTree.map_mk_bind_insertSum {α : Type u_1} (T S₁ S₂ : RoseTree α) : Multiset.map UnorderedTree.mk ((T.insertSum S₁).bind fun (x : RoseTree α) => x.insertSum S₂) = Multiset.map UnorderedTree.mk ((S₁.insertSum S₂).bind fun (x : RoseTree α) => T.insertSum x) + Multiset.map UnorderedTree.mk (T.insertion [S₁, S₂])

Grafting S₁ into T and then S₂ into the result is grafting S₁ ◁ S₂ into T, plus grafting S₁ and S₂ into T at once, once children are unordered.

theorem RoseTree.map_mk_bind_insertionForest {α : Type u_1} (F : List (RoseTree α)) (S₁ S₂ : RoseTree α) : Multiset.map (List.map UnorderedTree.mk) ((insertionForest F [S₁]).bind fun (x : List (RoseTree α)) => insertionForest x [S₂]) = Multiset.map (List.map UnorderedTree.mk) ((S₁.insertSum S₂).bind fun (x : RoseTree α) => insertionForest F [x]) + Multiset.map (List.map UnorderedTree.mk) (insertionForest F [S₁, S₂])

The forest case of map_mk_bind_insertSum. The trees of each forest keep their order, since only the children inside them are reordered.

def UnorderedTree.insertSum {α : Type u_1} (T S : UnorderedTree α) : Multiset (UnorderedTree α)

The grafting product on nonplanar trees, the insertion of a single guest.

Equations

• T.insertSum S = T.insertion {S}

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

The grafting product on nonplanar trees, the insertion of a single guest.

Equations

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

@[simp]

theorem UnorderedTree.mk_insertSum {α : Type u_1} (T S : RoseTree α) : (mk T).insertSum (mk S) = Multiset.map mk (T.insertSum S)

theorem UnorderedTree.card_insertSum {α : Type u_1} (T S : UnorderedTree α) : (T.insertSum S).card = T.numNodes

theorem UnorderedTree.insertSum_bind_insertSum {α : Type u_1} (T S₁ S₂ : UnorderedTree α) : ((T.insertSum S₁).bind fun (x : UnorderedTree α) => x.insertSum S₂) = ((S₁.insertSum S₂).bind fun (x : UnorderedTree α) => T.insertSum x) + T.insertion {S₁, S₂}

Grafting S₁ into T and then S₂ into the result is grafting S₁ ◁ S₂ into T, plus grafting S₁ and S₂ into T at once. This is the degree-two case T ∘ BX = (T ∘ B) ∘ X - T ∘ (B ∘ X) of Oudom and Guin's Proposition 3.7.

theorem UnorderedTree.insertSum_assoc_symm {α : Type u_1} (T S₁ S₂ : UnorderedTree α) : (((T.insertSum S₁).bind fun (x : UnorderedTree α) => x.insertSum S₂) + (S₂.insertSum S₁).bind fun (x : UnorderedTree α) => T.insertSum x) = ((T.insertSum S₂).bind fun (x : UnorderedTree α) => x.insertSum S₁) + (S₁.insertSum S₂).bind fun (x : UnorderedTree α) => T.insertSum x

The associator of the grafting product is symmetric in its last two arguments, so that (T ◁ S₁) ◁ S₂ - T ◁ (S₁ ◁ S₂) = (T ◁ S₂) ◁ S₁ - T ◁ (S₂ ◁ S₁), here stated without subtraction.

theorem UnorderedTree.insertionMultiset_singleton_singleton {α : Type u_1} (T S : UnorderedTree α) : insertionMultiset {T} {S} = Multiset.map (fun (x : UnorderedTree α) => {x}) (T.insertSum S)

One host and one guest give the grafting product, each output a one-tree forest.

theorem UnorderedTree.productMultiset_singleton_singleton {α : Type u_1} (T S : UnorderedTree α) : productMultiset {T} {S} = {T, S} ::ₘ Multiset.map (fun (x : UnorderedTree α) => {x}) (T.insertSum S)

Two one-tree forests multiply to their disjoint union and their graftings.