Planar Rooted Trees and Forests

This file gives explicit names and basic APIs for planar rooted trees and ordered forests. The underlying tree types are the existing PTree and PLTree; the forest types are lists, so sibling order is retained.

Main definitions

• PlanarTree and PlanarForest
• LPlanarTree and LPlanarForest
• conversion maps to the non-planar quotients

@[reducible, inline]

abbrev HopfAlgebras.PlanarTree : Type

Non-empty planar rooted trees.

Equations

• HopfAlgebras.PlanarTree = HopfAlgebras.PTree

@[reducible, inline]

abbrev HopfAlgebras.PlanarForest : Type

Ordered forests of non-empty planar rooted trees.

Equations

• HopfAlgebras.PlanarForest = List HopfAlgebras.PlanarTree

@[reducible, inline]

abbrev HopfAlgebras.LPlanarTree (α : Type u) : Type u

Non-empty labelled planar rooted trees.

Equations

• HopfAlgebras.LPlanarTree α = HopfAlgebras.PLTree α

@[reducible, inline]

abbrev HopfAlgebras.LPlanarForest (α : Type u) : Type u

Ordered forests of labelled planar rooted trees.

Equations

• HopfAlgebras.LPlanarForest α = List (HopfAlgebras.LPlanarTree α)

def HopfAlgebras.PlanarTree.node (ts : PlanarForest) : PlanarTree

Build a planar tree from its ordered list of children.

Equations

• HopfAlgebras.PlanarTree.node ts = HopfAlgebras.PTree.node ts

def HopfAlgebras.PlanarTree.bullet : PlanarTree

The one-vertex planar rooted tree.

Equations

• HopfAlgebras.PlanarTree.bullet = HopfAlgebras.PTree.bullet

def HopfAlgebras.PlanarTree.chain2 : PlanarTree

A two-vertex planar rooted tree.

Equations

• HopfAlgebras.PlanarTree.chain2 = HopfAlgebras.PTree.chain2

def HopfAlgebras.PlanarTree.chain3 : PlanarTree

A three-vertex planar chain.

Equations

• HopfAlgebras.PlanarTree.chain3 = HopfAlgebras.PTree.chain3

def HopfAlgebras.PlanarTree.cherry : PlanarTree

A root with two bullet children.

Equations

• HopfAlgebras.PlanarTree.cherry = HopfAlgebras.PTree.cherry

def HopfAlgebras.PlanarTree.order (t : PlanarTree) : ℕ

The number of vertices of a planar rooted tree.

Equations

• t.order = HopfAlgebras.PTree.order t

def HopfAlgebras.PlanarTree.treeFactorial (t : PlanarTree) : ℕ

Butcher's tree factorial.

Equations

• t.treeFactorial = HopfAlgebras.PTree.treeFactorial t

def HopfAlgebras.PlanarTree.butcherProduct (ts : PlanarForest) (t : PlanarTree) : PlanarTree

Attach an ordered forest as the first children of the root.

Equations

• HopfAlgebras.PlanarTree.butcherProduct ts t = HopfAlgebras.PTree.butcherProduct ts t

def HopfAlgebras.PlanarTree.toRootedTree (t : PlanarTree) : RootedTree

Forget the planar embedding by quotienting sibling order.

Equations

• t.toRootedTree = HopfAlgebras.RootedTree.ofPTree t

@[simp]

theorem HopfAlgebras.PlanarTree.node_eq (ts : PlanarForest) : node ts = PTree.node ts

@[simp]

theorem HopfAlgebras.PlanarTree.order_node (ts : PlanarForest) : (node ts).order = 1 + PTree.orderList ts

@[simp]

theorem HopfAlgebras.PlanarTree.order_bullet : bullet.order = 1

@[simp]

theorem HopfAlgebras.PlanarTree.order_chain2 : chain2.order = 2

@[simp]

theorem HopfAlgebras.PlanarTree.order_chain3 : chain3.order = 3

@[simp]

theorem HopfAlgebras.PlanarTree.order_cherry : cherry.order = 3

theorem HopfAlgebras.PlanarTree.order_pos (t : PlanarTree) : 0 < t.order

@[simp]

theorem HopfAlgebras.PlanarTree.treeFactorial_node (ts : PlanarForest) : (node ts).treeFactorial = (node ts).order * PTree.treeFactorialList ts

@[simp]

theorem HopfAlgebras.PlanarTree.treeFactorial_bullet : bullet.treeFactorial = 1

@[simp]

theorem HopfAlgebras.PlanarTree.treeFactorial_chain2 : chain2.treeFactorial = 2

@[simp]

theorem HopfAlgebras.PlanarTree.treeFactorial_chain3 : chain3.treeFactorial = 6

@[simp]

theorem HopfAlgebras.PlanarTree.treeFactorial_cherry : cherry.treeFactorial = 3

theorem HopfAlgebras.PlanarTree.treeFactorial_pos (t : PlanarTree) : 0 < t.treeFactorial

theorem HopfAlgebras.PlanarTree.treeFactorial_ne_zero (t : PlanarTree) : t.treeFactorial ≠ 0

@[simp]

theorem HopfAlgebras.PlanarTree.butcherProduct_nil (t : PlanarTree) : butcherProduct [] t = t

@[simp]

theorem HopfAlgebras.PlanarTree.order_butcherProduct (ts : PlanarForest) (t : PlanarTree) : (butcherProduct ts t).order = PTree.orderList ts + t.order

@[simp]

theorem HopfAlgebras.PlanarTree.butcherProduct_assoc (ts us : PlanarForest) (t : PlanarTree) : butcherProduct ts (butcherProduct us t) = butcherProduct (ts ++ us) t

@[simp]

theorem HopfAlgebras.PlanarTree.order_toRootedTree (t : PlanarTree) : t.toRootedTree.order = t.order

@[simp]

theorem HopfAlgebras.PlanarTree.treeFactorial_toRootedTree (t : PlanarTree) : t.toRootedTree.treeFactorial = t.treeFactorial

theorem HopfAlgebras.PlanarTree.toRootedTree_eq_iff {t u : PlanarTree} : t.toRootedTree = u.toRootedTree ↔ PTree.Perm t u

def HopfAlgebras.PlanarForest.empty : PlanarForest

The empty ordered planar forest.

Equations

• HopfAlgebras.PlanarForest.empty = []

def HopfAlgebras.PlanarForest.singleton (t : PlanarTree) : PlanarForest

The ordered forest with one tree.

Equations

• HopfAlgebras.PlanarForest.singleton t = [t]

def HopfAlgebras.PlanarForest.append (ts us : PlanarForest) : PlanarForest

Concatenate ordered forests.

Equations

• ts.append us = ts ++ us

def HopfAlgebras.PlanarForest.order (ts : PlanarForest) : ℕ

The sum of the orders of all trees in an ordered forest.

Equations

• ts.order = HopfAlgebras.PTree.orderList ts

def HopfAlgebras.PlanarForest.treeFactorial (ts : PlanarForest) : ℕ

Product of tree factorials over an ordered forest.

Equations

• ts.treeFactorial = HopfAlgebras.PTree.treeFactorialList ts

def HopfAlgebras.PlanarForest.graft (ts : PlanarForest) : PlanarTree

Graft an ordered forest onto one new root.

Equations

• ts.graft = HopfAlgebras.PlanarTree.node ts

def HopfAlgebras.PlanarForest.toRootedForest (ts : PlanarForest) : RootedForest

Forget order by mapping each planar tree to its non-planar quotient.

Equations

• ts.toRootedForest = ↑(List.map HopfAlgebras.RootedTree.ofPTree ts)

@[simp]

theorem HopfAlgebras.PlanarForest.empty_eq : empty = []

@[simp]

theorem HopfAlgebras.PlanarForest.singleton_eq (t : PlanarTree) : singleton t = [t]

@[simp]

theorem HopfAlgebras.PlanarForest.append_eq (ts us : PlanarForest) : ts.append us = ts ++ us

@[simp]

theorem HopfAlgebras.PlanarForest.order_empty : empty.order = 0

@[simp]

theorem HopfAlgebras.PlanarForest.order_nil : order [] = 0

@[simp]

theorem HopfAlgebras.PlanarForest.order_cons (t : PlanarTree) (ts : PlanarForest) : order (t :: ts) = t.order + ts.order

@[simp]

theorem HopfAlgebras.PlanarForest.order_singleton (t : PlanarTree) : (singleton t).order = t.order

@[simp]

theorem HopfAlgebras.PlanarForest.order_append (ts us : PlanarForest) : (ts.append us).order = ts.order + us.order

theorem HopfAlgebras.PlanarForest.order_eq_zero_iff (ts : PlanarForest) : ts.order = 0 ↔ ts = []

@[simp]

theorem HopfAlgebras.PlanarForest.treeFactorial_empty : empty.treeFactorial = 1

@[simp]

theorem HopfAlgebras.PlanarForest.treeFactorial_nil : treeFactorial [] = 1

@[simp]

theorem HopfAlgebras.PlanarForest.treeFactorial_cons (t : PlanarTree) (ts : PlanarForest) : treeFactorial (t :: ts) = t.treeFactorial * ts.treeFactorial

@[simp]

theorem HopfAlgebras.PlanarForest.treeFactorial_singleton (t : PlanarTree) : (singleton t).treeFactorial = t.treeFactorial

@[simp]

theorem HopfAlgebras.PlanarForest.treeFactorial_append (ts us : PlanarForest) : (ts.append us).treeFactorial = ts.treeFactorial * us.treeFactorial

theorem HopfAlgebras.PlanarForest.treeFactorial_pos (ts : PlanarForest) : 0 < ts.treeFactorial

theorem HopfAlgebras.PlanarForest.treeFactorial_ne_zero (ts : PlanarForest) : ts.treeFactorial ≠ 0

@[simp]

theorem HopfAlgebras.PlanarForest.order_graft (ts : PlanarForest) : ts.graft.order = 1 + ts.order

@[simp]

theorem HopfAlgebras.PlanarForest.treeFactorial_graft (ts : PlanarForest) : ts.graft.treeFactorial = (1 + ts.order) * ts.treeFactorial

@[simp]

theorem HopfAlgebras.PlanarForest.order_toRootedForest (ts : PlanarForest) : ts.toRootedForest.order = ts.order

@[simp]

theorem HopfAlgebras.PlanarForest.treeFactorial_toRootedForest (ts : PlanarForest) : ts.toRootedForest.treeFactorial = ts.treeFactorial

theorem HopfAlgebras.PlanarForest.graft_toRootedForest (ts : PlanarForest) : ts.toRootedForest.graft = ts.graft.toRootedTree

def HopfAlgebras.LPlanarTree.node {α : Type u} (a : α) (ts : LPlanarForest α) : LPlanarTree α

Build a labelled planar tree from a root label and ordered children.

Equations

• HopfAlgebras.LPlanarTree.node a ts = HopfAlgebras.PLTree.node a ts

def HopfAlgebras.LPlanarTree.erase {α : Type u} (t : LPlanarTree α) : PlanarTree

Forget labels from a labelled planar tree.

Equations

• t.erase = HopfAlgebras.PLTree.erase t

def HopfAlgebras.LPlanarTree.constLabel {α : Type u} (a : α) (t : PlanarTree) : LPlanarTree α

Label every vertex of a planar tree by the same label.

Equations

• HopfAlgebras.LPlanarTree.constLabel a t = HopfAlgebras.PLTree.constLabel a t

def HopfAlgebras.LPlanarTree.rootLabel {α : Type u} (t : LPlanarTree α) : α

The label at the root.

Equations

• t.rootLabel = HopfAlgebras.PLTree.rootLabel t

def HopfAlgebras.LPlanarTree.map {α : Type u} {β : Type v} (f : α → β) (t : LPlanarTree α) : LPlanarTree β

Change every label in a labelled planar tree.

Equations

• HopfAlgebras.LPlanarTree.map f t = HopfAlgebras.PLTree.map f t

def HopfAlgebras.LPlanarTree.order {α : Type u} (t : LPlanarTree α) : ℕ

The number of vertices.

Equations

• t.order = HopfAlgebras.PLTree.order t

def HopfAlgebras.LPlanarTree.treeFactorial {α : Type u} (t : LPlanarTree α) : ℕ

Butcher's tree factorial, ignoring labels.

Equations

• t.treeFactorial = HopfAlgebras.PLTree.treeFactorial t

def HopfAlgebras.LPlanarTree.butcherProduct {α : Type u} (ts : LPlanarForest α) (t : LPlanarTree α) : LPlanarTree α

Attach an ordered labelled forest as the first children of the root.

Equations

• HopfAlgebras.LPlanarTree.butcherProduct ts t = HopfAlgebras.PLTree.butcherProduct ts t

def HopfAlgebras.LPlanarTree.toRootedTree {α : Type u} (t : LPlanarTree α) : LRootedTree α

Forget planar order by quotienting recursively by sibling permutations.

Equations

• t.toRootedTree = HopfAlgebras.LRootedTree.ofPLTree t

@[simp]

theorem HopfAlgebras.LPlanarTree.node_eq {α : Type u} (a : α) (ts : LPlanarForest α) : node a ts = PLTree.node a ts

@[simp]

theorem HopfAlgebras.LPlanarTree.erase_node {α : Type u} (a : α) (ts : LPlanarForest α) : (node a ts).erase = PlanarTree.node (List.map erase ts)

@[simp]

theorem HopfAlgebras.LPlanarTree.rootLabel_node {α : Type u} (a : α) (ts : LPlanarForest α) : (node a ts).rootLabel = a

@[simp]

theorem HopfAlgebras.LPlanarTree.order_node {α : Type u} (a : α) (ts : LPlanarForest α) : (node a ts).order = 1 + PLTree.orderList ts

@[simp]

theorem HopfAlgebras.LPlanarTree.map_node {α : Type u} {β : Type v} (f : α → β) (a : α) (ts : LPlanarForest α) : map f (node a ts) = node (f a) (List.map (map f) ts)

@[simp]

theorem HopfAlgebras.LPlanarTree.map_id {α : Type u} (t : LPlanarTree α) : map (fun (a : α) => a) t = t

@[simp]

theorem HopfAlgebras.LPlanarTree.map_comp {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (t : LPlanarTree α) : map g (map f t) = map (g ∘ f) t

@[simp]

theorem HopfAlgebras.LPlanarTree.map_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (t : PlanarTree) : map f (constLabel a t) = constLabel (f a) t

@[simp]

theorem HopfAlgebras.LPlanarTree.erase_constLabel {α : Type u} (a : α) (t : PlanarTree) : (constLabel a t).erase = t

@[simp]

theorem HopfAlgebras.LPlanarTree.rootLabel_constLabel {α : Type u} (a : α) (t : PlanarTree) : (constLabel a t).rootLabel = a

@[simp]

theorem HopfAlgebras.LPlanarTree.order_erase {α : Type u} (t : LPlanarTree α) : t.erase.order = t.order

@[simp]

theorem HopfAlgebras.LPlanarTree.order_map {α : Type u} {β : Type v} (f : α → β) (t : LPlanarTree α) : (map f t).order = t.order

@[simp]

theorem HopfAlgebras.LPlanarTree.erase_map {α : Type u} {β : Type v} (f : α → β) (t : LPlanarTree α) : (map f t).erase = t.erase

@[simp]

theorem HopfAlgebras.LPlanarTree.treeFactorial_erase {α : Type u} (t : LPlanarTree α) : t.erase.treeFactorial = t.treeFactorial

@[simp]

theorem HopfAlgebras.LPlanarTree.order_toRootedTree {α : Type u} (t : LPlanarTree α) : t.toRootedTree.order = t.order

@[simp]

theorem HopfAlgebras.LPlanarTree.treeFactorial_toRootedTree {α : Type u} (t : LPlanarTree α) : t.toRootedTree.treeFactorial = t.treeFactorial

@[simp]

theorem HopfAlgebras.LPlanarTree.erase_toRootedTree {α : Type u} (t : LPlanarTree α) : t.toRootedTree.erase = t.erase.toRootedTree

theorem HopfAlgebras.LPlanarTree.toRootedTree_eq_iff {α : Type u} {t u : LPlanarTree α} : t.toRootedTree = u.toRootedTree ↔ PLTree.Perm t u

def HopfAlgebras.LPlanarForest.empty {α : Type u} : LPlanarForest α

The empty ordered labelled planar forest.

Equations

• HopfAlgebras.LPlanarForest.empty = []

def HopfAlgebras.LPlanarForest.singleton {α : Type u} (t : LPlanarTree α) : LPlanarForest α

The ordered labelled forest with one tree.

Equations

• HopfAlgebras.LPlanarForest.singleton t = [t]

def HopfAlgebras.LPlanarForest.append {α : Type u} (ts us : LPlanarForest α) : LPlanarForest α

Concatenate ordered labelled forests.

Equations

• ts.append us = ts ++ us

def HopfAlgebras.LPlanarForest.erase {α : Type u} (ts : LPlanarForest α) : PlanarForest

Forget all labels.

Equations

• ts.erase = List.map HopfAlgebras.LPlanarTree.erase ts

def HopfAlgebras.LPlanarForest.constLabel {α : Type u} (a : α) (ts : PlanarForest) : LPlanarForest α

Label every vertex of every tree by the same label.

Equations

• HopfAlgebras.LPlanarForest.constLabel a ts = List.map (HopfAlgebras.LPlanarTree.constLabel a) ts

def HopfAlgebras.LPlanarForest.map {α : Type u} {β : Type v} (f : α → β) (ts : LPlanarForest α) : LPlanarForest β

Change every label in an ordered forest.

Equations

• HopfAlgebras.LPlanarForest.map f ts = List.map (HopfAlgebras.LPlanarTree.map f) ts

@[simp]

theorem HopfAlgebras.LPlanarForest.map_nil {α : Type u} {β : Type v} (f : α → β) : map f [] = []

@[simp]

theorem HopfAlgebras.LPlanarForest.map_append {α : Type u} {β : Type v} (f : α → β) (ts us : LPlanarForest α) : map f (ts ++ us) = map f ts ++ map f us

@[simp]

theorem HopfAlgebras.LPlanarForest.map_id {α : Type u} (ts : LPlanarForest α) : map (fun (a : α) => a) ts = ts

@[simp]

theorem HopfAlgebras.LPlanarForest.map_comp {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (ts : LPlanarForest α) : map g (map f ts) = map (g ∘ f) ts

@[simp]

theorem HopfAlgebras.LPlanarForest.map_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (ts : PlanarForest) : map f (constLabel a ts) = constLabel (f a) ts

def HopfAlgebras.LPlanarForest.order {α : Type u} (ts : LPlanarForest α) : ℕ

The sum of the orders of all trees in an ordered labelled forest.

Equations

• ts.order = HopfAlgebras.PLTree.orderList ts

def HopfAlgebras.LPlanarForest.treeFactorial {α : Type u} (ts : LPlanarForest α) : ℕ

Product of tree factorials over an ordered labelled forest.

Equations

• ts.treeFactorial = HopfAlgebras.PLTree.treeFactorialList ts

def HopfAlgebras.LPlanarForest.graft {α : Type u} (a : α) (ts : LPlanarForest α) : LPlanarTree α

Graft an ordered labelled forest onto one new labelled root.

Equations

• HopfAlgebras.LPlanarForest.graft a ts = HopfAlgebras.LPlanarTree.node a ts

def HopfAlgebras.LPlanarForest.toRootedForest {α : Type u} (ts : LPlanarForest α) : LRootedForest α

Forget planar order by quotienting all trees recursively.

Equations

• ts.toRootedForest = ↑(List.map HopfAlgebras.LRootedTree.ofPLTree ts)

@[simp]

theorem HopfAlgebras.LPlanarForest.erase_empty {α : Type u} : empty.erase = PlanarForest.empty

@[simp]

theorem HopfAlgebras.LPlanarForest.erase_cons {α : Type u} (t : LPlanarTree α) (ts : LPlanarForest α) : erase (t :: ts) = t.erase :: ts.erase

@[simp]

theorem HopfAlgebras.LPlanarForest.erase_append {α : Type u} (ts us : LPlanarForest α) : (ts.append us).erase = ts.erase.append us.erase

@[simp]

theorem HopfAlgebras.LPlanarForest.erase_constLabel {α : Type u} (a : α) (ts : PlanarForest) : (constLabel a ts).erase = ts

@[simp]

theorem HopfAlgebras.LPlanarForest.erase_map {α : Type u} {β : Type v} (f : α → β) (ts : LPlanarForest α) : (map f ts).erase = ts.erase

@[simp]

theorem HopfAlgebras.LPlanarForest.order_empty {α : Type u} : empty.order = 0

@[simp]

theorem HopfAlgebras.LPlanarForest.order_nil {α : Type u} : order [] = 0

@[simp]

theorem HopfAlgebras.LPlanarForest.order_cons {α : Type u} (t : LPlanarTree α) (ts : LPlanarForest α) : order (t :: ts) = t.order + ts.order

@[simp]

theorem HopfAlgebras.LPlanarForest.order_append {α : Type u} (ts us : LPlanarForest α) : (ts.append us).order = ts.order + us.order

@[simp]

theorem HopfAlgebras.LPlanarForest.order_erase {α : Type u} (ts : LPlanarForest α) : ts.erase.order = ts.order

@[simp]

theorem HopfAlgebras.LPlanarForest.order_map {α : Type u} {β : Type v} (f : α → β) (ts : LPlanarForest α) : (map f ts).order = ts.order

@[simp]

theorem HopfAlgebras.LPlanarForest.order_constLabel {α : Type u} (a : α) (ts : PlanarForest) : (constLabel a ts).order = ts.order

@[simp]

theorem HopfAlgebras.LPlanarForest.treeFactorial_empty {α : Type u} : empty.treeFactorial = 1

@[simp]

theorem HopfAlgebras.LPlanarForest.treeFactorial_nil {α : Type u} : treeFactorial [] = 1

@[simp]

theorem HopfAlgebras.LPlanarForest.treeFactorial_cons {α : Type u} (t : LPlanarTree α) (ts : LPlanarForest α) : treeFactorial (t :: ts) = t.treeFactorial * ts.treeFactorial

@[simp]

theorem HopfAlgebras.LPlanarForest.treeFactorial_append {α : Type u} (ts us : LPlanarForest α) : (ts.append us).treeFactorial = ts.treeFactorial * us.treeFactorial

@[simp]

theorem HopfAlgebras.LPlanarForest.treeFactorial_erase {α : Type u} (ts : LPlanarForest α) : ts.erase.treeFactorial = ts.treeFactorial

@[simp]

theorem HopfAlgebras.LPlanarForest.treeFactorial_constLabel {α : Type u} (a : α) (ts : PlanarForest) : (constLabel a ts).treeFactorial = ts.treeFactorial

@[simp]

theorem HopfAlgebras.LPlanarForest.order_graft {α : Type u} (a : α) (ts : LPlanarForest α) : (graft a ts).order = 1 + ts.order

@[simp]

theorem HopfAlgebras.LPlanarForest.erase_graft {α : Type u} (a : α) (ts : LPlanarForest α) : (graft a ts).erase = ts.erase.graft

@[simp]

theorem HopfAlgebras.LPlanarForest.rootLabel_graft {α : Type u} (a : α) (ts : LPlanarForest α) : (graft a ts).rootLabel = a

@[simp]

theorem HopfAlgebras.LPlanarForest.order_toRootedForest {α : Type u} (ts : LPlanarForest α) : ts.toRootedForest.order = ts.order

@[simp]

theorem HopfAlgebras.LPlanarForest.treeFactorial_toRootedForest {α : Type u} (ts : LPlanarForest α) : ts.toRootedForest.treeFactorial = ts.treeFactorial

@[simp]

theorem HopfAlgebras.LPlanarForest.erase_toRootedForest {α : Type u} (ts : LPlanarForest α) : ts.toRootedForest.erase = ts.erase.toRootedForest