Planar Pre-Lie Grafting

This file defines the planar rooted-tree grafting operation which underlies the pre-Lie product on rooted trees. The operation returns the list of all planar trees obtained by grafting the first tree at one vertex of the second tree.

def BSeries.PTree.preLieGrafts (s : HopfAlgebras.PTree) : HopfAlgebras.PTree → List HopfAlgebras.PTree

All planar trees obtained by grafting s at one vertex of t.

Equations

• BSeries.PTree.preLieGrafts s (HopfAlgebras.PTree.node ts) = HopfAlgebras.PTree.node (s :: ts) :: List.map HopfAlgebras.PTree.node (BSeries.PTree.preLieGraftsList s ts)

def BSeries.PTree.preLieGraftsList (s : HopfAlgebras.PTree) : List HopfAlgebras.PTree → List (List HopfAlgebras.PTree)

Child-list replacements induced by grafting s at one vertex of a child.

Equations

• One or more equations did not get rendered due to their size.
• BSeries.PTree.preLieGraftsList s [] = []

@[simp]

theorem BSeries.PTree.preLieGrafts_node (s : HopfAlgebras.PTree) (ts : List HopfAlgebras.PTree) : preLieGrafts s (HopfAlgebras.PTree.node ts) = HopfAlgebras.PTree.node (s :: ts) :: List.map HopfAlgebras.PTree.node (preLieGraftsList s ts)

@[simp]

theorem BSeries.PTree.preLieGraftsList_nil (s : HopfAlgebras.PTree) : preLieGraftsList s [] = []

@[simp]

theorem BSeries.PTree.preLieGraftsList_cons (s t : HopfAlgebras.PTree) (ts : List HopfAlgebras.PTree) : preLieGraftsList s (t :: ts) = List.map (fun (t' : HopfAlgebras.PTree) => t' :: ts) (preLieGrafts s t) ++ List.map (fun (us : List HopfAlgebras.PTree) => t :: us) (preLieGraftsList s ts)

@[simp]

theorem BSeries.PTree.preLieGrafts_bullet (s : HopfAlgebras.PTree) : preLieGrafts s HopfAlgebras.PTree.bullet = [HopfAlgebras.PTree.node [s]]

theorem BSeries.PTree.length_preLieGrafts (s t : HopfAlgebras.PTree) : (preLieGrafts s t).length = t.order

theorem BSeries.PTree.length_preLieGraftsList (s : HopfAlgebras.PTree) (ts : List HopfAlgebras.PTree) : (preLieGraftsList s ts).length = HopfAlgebras.PTree.orderList ts

theorem BSeries.PTree.order_of_mem_preLieGrafts (s : HopfAlgebras.PTree) {t u : HopfAlgebras.PTree} : u ∈ preLieGrafts s t → u.order = s.order + t.order

theorem BSeries.PTree.order_of_mem_preLieGraftsList (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} : us ∈ preLieGraftsList s ts → HopfAlgebras.PTree.orderList us = s.order + HopfAlgebras.PTree.orderList ts

theorem BSeries.PTree.preLieGrafts_listRelPerm_left {s s' : HopfAlgebras.PTree} (hs : s.Perm s') (t : HopfAlgebras.PTree) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (preLieGrafts s t) (preLieGrafts s' t)

theorem BSeries.PTree.preLieGraftsList_listRelPerm_left {s s' : HopfAlgebras.PTree} (hs : s.Perm s') (ts : List HopfAlgebras.PTree) : HopfAlgebras.PTree.ListRelPerm (List.Forall₂ HopfAlgebras.PTree.Perm) (preLieGraftsList s ts) (preLieGraftsList s' ts)

theorem BSeries.PTree.preLieGrafts_map_ofPTree_perm_left {s s' : HopfAlgebras.PTree} (hs : s.Perm s') (t : HopfAlgebras.PTree) : (List.map HopfAlgebras.RootedTree.ofPTree (preLieGrafts s t)).Perm (List.map HopfAlgebras.RootedTree.ofPTree (preLieGrafts s' t))

theorem BSeries.PTree.preLieGraftsList_map_ofPTree_perm_left {s s' : HopfAlgebras.PTree} (hs : s.Perm s') (ts : List HopfAlgebras.PTree) : (List.map (fun (us : List HopfAlgebras.PTree) => List.map HopfAlgebras.RootedTree.ofPTree us) (preLieGraftsList s ts)).Perm (List.map (fun (us : List HopfAlgebras.PTree) => List.map HopfAlgebras.RootedTree.ofPTree us) (preLieGraftsList s' ts))

theorem BSeries.PTree.preLieGraftsList_listRelPerm_node_of_perm (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} : ts.Perm us → HopfAlgebras.PTree.ListRelPerm (fun (vs ws : List HopfAlgebras.PTree) => (HopfAlgebras.PTree.node vs).Perm (HopfAlgebras.PTree.node ws)) (preLieGraftsList s ts) (preLieGraftsList s us)

theorem BSeries.PTree.preLieGraftsList_nodes_listRelPerm_of_perm (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} (h : ts.Perm us) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (List.map HopfAlgebras.PTree.node (preLieGraftsList s ts)) (List.map HopfAlgebras.PTree.node (preLieGraftsList s us))

theorem BSeries.PTree.preLieGraftsList_listRelPerm_node_of_forall₂_perm_grafts (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} : List.Forall₂ (fun (t u : HopfAlgebras.PTree) => t.Perm u ∧ HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (preLieGrafts s t) (preLieGrafts s u)) ts us → HopfAlgebras.PTree.ListRelPerm (fun (vs ws : List HopfAlgebras.PTree) => (HopfAlgebras.PTree.node vs).Perm (HopfAlgebras.PTree.node ws)) (preLieGraftsList s ts) (preLieGraftsList s us)

theorem BSeries.PTree.preLieGraftsList_nodes_listRelPerm_of_forall₂_perm_grafts (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} (h : List.Forall₂ (fun (t u : HopfAlgebras.PTree) => t.Perm u ∧ HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (preLieGrafts s t) (preLieGrafts s u)) ts us) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (List.map HopfAlgebras.PTree.node (preLieGraftsList s ts)) (List.map HopfAlgebras.PTree.node (preLieGraftsList s us))

theorem BSeries.PTree.preLieGrafts_node_listRelPerm_of_list_perm (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} (hp : ts.Perm us) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (preLieGrafts s (HopfAlgebras.PTree.node ts)) (preLieGrafts s (HopfAlgebras.PTree.node us))

theorem BSeries.PTree.preLieGrafts_node_listRelPerm_of_forall₂_perm_grafts (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} (h : List.Forall₂ (fun (t u : HopfAlgebras.PTree) => t.Perm u ∧ HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (preLieGrafts s t) (preLieGrafts s u)) ts us) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (preLieGrafts s (HopfAlgebras.PTree.node ts)) (preLieGrafts s (HopfAlgebras.PTree.node us))

theorem BSeries.PTree.preLieGrafts_listRelPerm_right (s : HopfAlgebras.PTree) {t u : HopfAlgebras.PTree} : t.Perm u → HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (preLieGrafts s t) (preLieGrafts s u)

theorem BSeries.PTree.forall₂_perm_preLieGrafts_of_forall₂_perm (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} : List.Forall₂ HopfAlgebras.PTree.Perm ts us → List.Forall₂ (fun (t u : HopfAlgebras.PTree) => t.Perm u ∧ HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PTree.Perm (preLieGrafts s t) (preLieGrafts s u)) ts us

theorem BSeries.PTree.preLieGrafts_map_ofPTree_perm_right (s : HopfAlgebras.PTree) {t t' : HopfAlgebras.PTree} (ht : t.Perm t') : (List.map HopfAlgebras.RootedTree.ofPTree (preLieGrafts s t)).Perm (List.map HopfAlgebras.RootedTree.ofPTree (preLieGrafts s t'))

theorem BSeries.PTree.preLieGraftsList_map_node_ofPTree_perm_right (s : HopfAlgebras.PTree) {ts us : List HopfAlgebras.PTree} (h : ts.Perm us) : (List.map (fun (vs : List HopfAlgebras.PTree) => HopfAlgebras.RootedTree.ofPTree (HopfAlgebras.PTree.node vs)) (preLieGraftsList s ts)).Perm (List.map (fun (vs : List HopfAlgebras.PTree) => HopfAlgebras.RootedTree.ofPTree (HopfAlgebras.PTree.node vs)) (preLieGraftsList s us))

def BSeries.PLTree.preLieGrafts {α : Type u} (s : HopfAlgebras.PLTree α) : HopfAlgebras.PLTree α → List (HopfAlgebras.PLTree α)

All labelled planar trees obtained by grafting s at one vertex of t.

Equations

• BSeries.PLTree.preLieGrafts s (HopfAlgebras.PLTree.node a ts) = HopfAlgebras.PLTree.node a (s :: ts) :: List.map (HopfAlgebras.PLTree.node a) (BSeries.PLTree.preLieGraftsList s ts)

def BSeries.PLTree.preLieGraftsList {α : Type u} (s : HopfAlgebras.PLTree α) : List (HopfAlgebras.PLTree α) → List (List (HopfAlgebras.PLTree α))

Child-list replacements induced by labelled pre-Lie grafting.

Equations

• One or more equations did not get rendered due to their size.
• BSeries.PLTree.preLieGraftsList s [] = []

@[simp]

theorem BSeries.PLTree.preLieGrafts_node {α : Type u} (s : HopfAlgebras.PLTree α) (a : α) (ts : List (HopfAlgebras.PLTree α)) : preLieGrafts s (HopfAlgebras.PLTree.node a ts) = HopfAlgebras.PLTree.node a (s :: ts) :: List.map (HopfAlgebras.PLTree.node a) (preLieGraftsList s ts)

@[simp]

theorem BSeries.PLTree.preLieGraftsList_nil {α : Type u} (s : HopfAlgebras.PLTree α) : preLieGraftsList s [] = []

@[simp]

theorem BSeries.PLTree.preLieGraftsList_cons {α : Type u} (s t : HopfAlgebras.PLTree α) (ts : List (HopfAlgebras.PLTree α)) : preLieGraftsList s (t :: ts) = List.map (fun (t' : HopfAlgebras.PLTree α) => t' :: ts) (preLieGrafts s t) ++ List.map (fun (us : List (HopfAlgebras.PLTree α)) => t :: us) (preLieGraftsList s ts)

theorem BSeries.PLTree.length_preLieGrafts {α : Type u} (s t : HopfAlgebras.PLTree α) : (preLieGrafts s t).length = t.order

theorem BSeries.PLTree.length_preLieGraftsList {α : Type u} (s : HopfAlgebras.PLTree α) (ts : List (HopfAlgebras.PLTree α)) : (preLieGraftsList s ts).length = HopfAlgebras.PLTree.orderList ts

theorem BSeries.PLTree.order_of_mem_preLieGrafts {α : Type u} (s : HopfAlgebras.PLTree α) {t u : HopfAlgebras.PLTree α} : u ∈ preLieGrafts s t → u.order = s.order + t.order

theorem BSeries.PLTree.order_of_mem_preLieGraftsList {α : Type u} (s : HopfAlgebras.PLTree α) {ts us : List (HopfAlgebras.PLTree α)} : us ∈ preLieGraftsList s ts → HopfAlgebras.PLTree.orderList us = s.order + HopfAlgebras.PLTree.orderList ts

theorem BSeries.PLTree.preLieGrafts_listRelPerm_left {α : Type u} {s s' : HopfAlgebras.PLTree α} (hs : s.Perm s') (t : HopfAlgebras.PLTree α) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (preLieGrafts s t) (preLieGrafts s' t)

theorem BSeries.PLTree.preLieGraftsList_listRelPerm_left {α : Type u} {s s' : HopfAlgebras.PLTree α} (hs : s.Perm s') (ts : List (HopfAlgebras.PLTree α)) : HopfAlgebras.PTree.ListRelPerm (List.Forall₂ HopfAlgebras.PLTree.Perm) (preLieGraftsList s ts) (preLieGraftsList s' ts)

theorem BSeries.PLTree.preLieGrafts_map_ofPLTree_perm_left {α : Type u} {s s' : HopfAlgebras.PLTree α} (hs : s.Perm s') (t : HopfAlgebras.PLTree α) : (List.map HopfAlgebras.LRootedTree.ofPLTree (preLieGrafts s t)).Perm (List.map HopfAlgebras.LRootedTree.ofPLTree (preLieGrafts s' t))

theorem BSeries.PLTree.preLieGraftsList_map_ofPLTree_perm_left {α : Type u} {s s' : HopfAlgebras.PLTree α} (hs : s.Perm s') (ts : List (HopfAlgebras.PLTree α)) : (List.map (fun (us : List (HopfAlgebras.PLTree α)) => List.map HopfAlgebras.LRootedTree.ofPLTree us) (preLieGraftsList s ts)).Perm (List.map (fun (us : List (HopfAlgebras.PLTree α)) => List.map HopfAlgebras.LRootedTree.ofPLTree us) (preLieGraftsList s' ts))

theorem BSeries.PLTree.preLieGraftsList_listRelPerm_node_of_perm {α : Type u} (s : HopfAlgebras.PLTree α) (a : α) {ts us : List (HopfAlgebras.PLTree α)} : ts.Perm us → HopfAlgebras.PTree.ListRelPerm (fun (vs ws : List (HopfAlgebras.PLTree α)) => (HopfAlgebras.PLTree.node a vs).Perm (HopfAlgebras.PLTree.node a ws)) (preLieGraftsList s ts) (preLieGraftsList s us)

theorem BSeries.PLTree.preLieGraftsList_nodes_listRelPerm_of_perm {α : Type u} (s : HopfAlgebras.PLTree α) (a : α) {ts us : List (HopfAlgebras.PLTree α)} (h : ts.Perm us) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (List.map (HopfAlgebras.PLTree.node a) (preLieGraftsList s ts)) (List.map (HopfAlgebras.PLTree.node a) (preLieGraftsList s us))

theorem BSeries.PLTree.preLieGraftsList_listRelPerm_node_of_forall₂_perm_grafts {α : Type u} (s : HopfAlgebras.PLTree α) (a : α) {ts us : List (HopfAlgebras.PLTree α)} : List.Forall₂ (fun (t u : HopfAlgebras.PLTree α) => t.Perm u ∧ HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (preLieGrafts s t) (preLieGrafts s u)) ts us → HopfAlgebras.PTree.ListRelPerm (fun (vs ws : List (HopfAlgebras.PLTree α)) => (HopfAlgebras.PLTree.node a vs).Perm (HopfAlgebras.PLTree.node a ws)) (preLieGraftsList s ts) (preLieGraftsList s us)

theorem BSeries.PLTree.preLieGraftsList_nodes_listRelPerm_of_forall₂_perm_grafts {α : Type u} (s : HopfAlgebras.PLTree α) (a : α) {ts us : List (HopfAlgebras.PLTree α)} (h : List.Forall₂ (fun (t u : HopfAlgebras.PLTree α) => t.Perm u ∧ HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (preLieGrafts s t) (preLieGrafts s u)) ts us) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (List.map (HopfAlgebras.PLTree.node a) (preLieGraftsList s ts)) (List.map (HopfAlgebras.PLTree.node a) (preLieGraftsList s us))

theorem BSeries.PLTree.preLieGrafts_node_listRelPerm_of_list_perm {α : Type u} (s : HopfAlgebras.PLTree α) (a : α) {ts us : List (HopfAlgebras.PLTree α)} (hp : ts.Perm us) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (preLieGrafts s (HopfAlgebras.PLTree.node a ts)) (preLieGrafts s (HopfAlgebras.PLTree.node a us))

theorem BSeries.PLTree.preLieGrafts_node_listRelPerm_of_forall₂_perm_grafts {α : Type u} (s : HopfAlgebras.PLTree α) (a : α) {ts us : List (HopfAlgebras.PLTree α)} (h : List.Forall₂ (fun (t u : HopfAlgebras.PLTree α) => t.Perm u ∧ HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (preLieGrafts s t) (preLieGrafts s u)) ts us) : HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (preLieGrafts s (HopfAlgebras.PLTree.node a ts)) (preLieGrafts s (HopfAlgebras.PLTree.node a us))

theorem BSeries.PLTree.preLieGrafts_listRelPerm_right {α : Type u} (s : HopfAlgebras.PLTree α) {t u : HopfAlgebras.PLTree α} : t.Perm u → HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (preLieGrafts s t) (preLieGrafts s u)

theorem BSeries.PLTree.forall₂_perm_preLieGrafts_of_forall₂_perm {α : Type u} (s : HopfAlgebras.PLTree α) {ts us : List (HopfAlgebras.PLTree α)} : List.Forall₂ HopfAlgebras.PLTree.Perm ts us → List.Forall₂ (fun (t u : HopfAlgebras.PLTree α) => t.Perm u ∧ HopfAlgebras.PTree.ListRelPerm HopfAlgebras.PLTree.Perm (preLieGrafts s t) (preLieGrafts s u)) ts us

theorem BSeries.PLTree.preLieGrafts_map_ofPLTree_perm_right {α : Type u} (s : HopfAlgebras.PLTree α) {t t' : HopfAlgebras.PLTree α} (ht : t.Perm t') : (List.map HopfAlgebras.LRootedTree.ofPLTree (preLieGrafts s t)).Perm (List.map HopfAlgebras.LRootedTree.ofPLTree (preLieGrafts s t'))

theorem BSeries.PLTree.preLieGraftsList_map_node_ofPLTree_perm_right {α : Type u} (s : HopfAlgebras.PLTree α) (a : α) {ts us : List (HopfAlgebras.PLTree α)} (h : ts.Perm us) : (List.map (fun (vs : List (HopfAlgebras.PLTree α)) => HopfAlgebras.LRootedTree.ofPLTree (HopfAlgebras.PLTree.node a vs)) (preLieGraftsList s ts)).Perm (List.map (fun (vs : List (HopfAlgebras.PLTree α)) => HopfAlgebras.LRootedTree.ofPLTree (HopfAlgebras.PLTree.node a vs)) (preLieGraftsList s us))

@[simp]

theorem BSeries.PLTree.erase_preLieGrafts {α : Type u} (s t : HopfAlgebras.PLTree α) : List.map HopfAlgebras.PLTree.erase (preLieGrafts s t) = PTree.preLieGrafts s.erase t.erase

@[simp]

theorem BSeries.PLTree.erase_preLieGraftsList {α : Type u} (s : HopfAlgebras.PLTree α) (ts : List (HopfAlgebras.PLTree α)) : List.map (fun (us : List (HopfAlgebras.PLTree α)) => List.map HopfAlgebras.PLTree.erase us) (preLieGraftsList s ts) = PTree.preLieGraftsList s.erase (List.map HopfAlgebras.PLTree.erase ts)

@[simp]

theorem BSeries.PLTree.map_preLieGrafts {α : Type u} {β : Type v} (f : α → β) (s t : HopfAlgebras.PLTree α) : List.map (HopfAlgebras.PLTree.map f) (preLieGrafts s t) = preLieGrafts (HopfAlgebras.PLTree.map f s) (HopfAlgebras.PLTree.map f t)

@[simp]

theorem BSeries.PLTree.map_preLieGraftsList {α : Type u} {β : Type v} (f : α → β) (s : HopfAlgebras.PLTree α) (ts : List (HopfAlgebras.PLTree α)) : List.map (fun (us : List (HopfAlgebras.PLTree α)) => List.map (HopfAlgebras.PLTree.map f) us) (preLieGraftsList s ts) = preLieGraftsList (HopfAlgebras.PLTree.map f s) (List.map (HopfAlgebras.PLTree.map f) ts)

@[simp]

theorem BSeries.PLTree.constLabel_preLieGrafts {α : Type u} (a : α) (s t : HopfAlgebras.PTree) : List.map (HopfAlgebras.PLTree.constLabel a) (PTree.preLieGrafts s t) = preLieGrafts (HopfAlgebras.PLTree.constLabel a s) (HopfAlgebras.PLTree.constLabel a t)

@[simp]

theorem BSeries.PLTree.constLabel_preLieGraftsList {α : Type u} (a : α) (s : HopfAlgebras.PTree) (ts : List HopfAlgebras.PTree) : List.map (fun (us : List HopfAlgebras.PTree) => List.map (HopfAlgebras.PLTree.constLabel a) us) (PTree.preLieGraftsList s ts) = preLieGraftsList (HopfAlgebras.PLTree.constLabel a s) (List.map (HopfAlgebras.PLTree.constLabel a) ts)