Unordered rooted trees

An unordered rooted tree with vertices labelled in α is a RoseTree α modulo the permutation of children at every vertex: the quotient UnorderedTree α := Quotient RoseTree.isSetoid. In the Connes–Kreimer literature, as in Foissy's introduction, these are the rooted trees and the ordered ones the planar rooted trees. The identity criterion is RoseTree.Perm (Core/Data/RoseTree/Perm.lean); this file owns the quotient: the projection mk, the lifting API, the lifted invariants, and the constructor node on Multiset children, under which the grafting B⁺ of a multiset of trees is well defined.

Main definitions

• UnorderedTree, UnorderedTree.mk: the quotient and its projection; operations descend through Quotient.lift and proofs through Quotient.inductionOn, as for Multiset.
• UnorderedTree.cons: adjoin a tree as a further child of the root, the transport of the list cons on children; it is left-commutative, so Multiset.foldr builds the constructor UnorderedTree.node on a multiset of children computably.
• UnorderedTree.induction_on, UnorderedTree.fold: induction and recursion on a tree as a label over a multiset of trees.
• UnorderedTree.para: recursion in which each step also sees the children themselves, so that subtree-sensitive functions are defined on the quotient with no invariance proof.

References

• L. Foissy, An introduction to Hopf algebras of trees

The quotient type

def UnorderedTree (α : Type u_1) : Type u_1

An unordered rooted tree with α-labelled vertices, the quotient of RoseTree α by the permutation of children at every vertex (RoseTree.Perm).

Equations

• UnorderedTree α = Quotient RoseTree.isSetoid

def UnorderedTree.mk {α : Type u_1} (t : RoseTree α) : UnorderedTree α

The canonical projection from ordered to nonplanar trees.

Equations

• UnorderedTree.mk t = ⟦t⟧

theorem UnorderedTree.mk_eq_mk_iff {α : Type u_1} {t s : RoseTree α} : mk t = mk s ↔ t.Perm s

@[simp]

theorem UnorderedTree.quot_mk_eq_mk {α : Type u_1} (t : RoseTree α) : ⟦t⟧ = mk t

Leaves and lifted counts

@[reducible, inline]

abbrev UnorderedTree.leaf {α : Type u_1} (a : α) : UnorderedTree α

A nonplanar leaf labeled a.

Equations

• UnorderedTree.leaf a = UnorderedTree.mk (RoseTree.leaf a)

def UnorderedTree.numNodes {α : Type u_1} : UnorderedTree α → ℕ

The number of vertices of a nonplanar tree.

Equations

• UnorderedTree.numNodes = Quotient.lift RoseTree.numNodes ⋯

@[simp]

theorem UnorderedTree.numNodes_mk {α : Type u_1} (t : RoseTree α) : (mk t).numNodes = t.numNodes

@[simp]

theorem UnorderedTree.numNodes_leaf {α : Type u_1} (a : α) : (leaf a).numNodes = 1

def UnorderedTree.numLeaves {α : Type u_1} : UnorderedTree α → ℕ

The number of childless vertices of a nonplanar tree.

Equations

• UnorderedTree.numLeaves = Quotient.lift RoseTree.numLeaves ⋯

@[simp]

theorem UnorderedTree.numLeaves_mk {α : Type u_1} (t : RoseTree α) : (mk t).numLeaves = t.numLeaves

@[simp]

theorem UnorderedTree.numLeaves_leaf {α : Type u_1} (a : α) : (leaf a).numLeaves = 1

def UnorderedTree.arity {α : Type u_1} : UnorderedTree α → ℕ

The number of children of the root.

Equations

• UnorderedTree.arity = Quotient.lift RoseTree.arity ⋯

@[simp]

theorem UnorderedTree.arity_mk {α : Type u_1} (t : RoseTree α) : (mk t).arity = t.arity

@[simp]

theorem UnorderedTree.arity_leaf {α : Type u_1} (a : α) : (leaf a).arity = 0

def UnorderedTree.height {α : Type u_1} : UnorderedTree α → ℕ

The number of vertices on a longest root-to-leaf path.

Equations

• UnorderedTree.height = Quotient.lift RoseTree.height ⋯

@[simp]

theorem UnorderedTree.height_mk {α : Type u_1} (t : RoseTree α) : (mk t).height = t.height

@[simp]

theorem UnorderedTree.height_leaf {α : Type u_1} (a : α) : (leaf a).height = 1

Destructors and node injectivity

The root value and the children (as a multiset of nonplanar trees) are RoseTree.Perm-invariant, so they descend to UnorderedTree. Node injectivity, mk_node_eq_mk_node_iff, is RoseTree.perm_node_iff read through mk.

def UnorderedTree.value {α : Type u_1} : UnorderedTree α → α

The root value of a nonplanar tree.

Equations

• UnorderedTree.value = Quotient.lift RoseTree.value ⋯

@[simp]

theorem UnorderedTree.value_mk {α : Type u_1} (t : RoseTree α) : (mk t).value = t.value

theorem UnorderedTree.perm_children_map_mk {α : Type u_1} {t s : RoseTree α} (h : t.Perm s) : ↑(List.map mk t.children) = ↑(List.map mk s.children)

def UnorderedTree.children {α : Type u_1} : UnorderedTree α → Multiset (UnorderedTree α)

The children of a nonplanar tree, as a multiset of nonplanar trees.

Equations

• UnorderedTree.children = Quotient.lift (fun (t : RoseTree α) => ↑(List.map UnorderedTree.mk t.children)) ⋯

@[simp]

theorem UnorderedTree.children_mk {α : Type u_1} (t : RoseTree α) : (mk t).children = ↑(List.map mk t.children)

theorem UnorderedTree.mk_node_eq_mk_node_iff {α : Type u_1} {a b : α} {cs ds : List (RoseTree α)} : mk (RoseTree.node a cs) = mk (RoseTree.node b ds) ↔ a = b ∧ ↑(List.map mk cs) = ↑(List.map mk ds)

Adjoining a child, and the node constructor

cons c t adjoins c as a further child of the root of t; it is the transport of the list cons on children lists and is left-commutative, so node a F is its Multiset.foldr over the children F starting from the leaf a. Both are computable, and node_mk_tree_list reads node back on a list of planar children.

def UnorderedTree.cons {α : Type u_1} (c t : UnorderedTree α) : UnorderedTree α

Adjoin a tree as a further child of the root.

Equations

• c.cons t = Quotient.liftOn₂ c t (fun (c t : RoseTree α) => UnorderedTree.mk (RoseTree.node t.value (c :: t.children))) ⋯

@[simp]

theorem UnorderedTree.cons_mk {α : Type u_1} (c : RoseTree α) (a : α) (cs : List (RoseTree α)) : (mk c).cons (mk (RoseTree.node a cs)) = mk (RoseTree.node a (c :: cs))

instance UnorderedTree.instLeftCommutativeCons {α : Type u_1} : LeftCommutative cons

def UnorderedTree.node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : UnorderedTree α

Build an unordered tree from a label and a multiset of children, by adjoining the children one at a time to the leaf.

Equations

• UnorderedTree.node a F = Multiset.foldr UnorderedTree.cons (UnorderedTree.leaf a) F

@[simp]

theorem UnorderedTree.node_zero {α : Type u_1} (a : α) : node a 0 = leaf a

theorem UnorderedTree.node_cons {α : Type u_1} (a : α) (c : UnorderedTree α) (F : Multiset (UnorderedTree α)) : node a (c ::ₘ F) = c.cons (node a F)

@[simp]

theorem UnorderedTree.cons_node {α : Type u_1} (a : α) (c : UnorderedTree α) (F : Multiset (UnorderedTree α)) : c.cons (node a F) = node a (c ::ₘ F)

theorem UnorderedTree.node_mk_tree_list {α : Type u_1} (a : α) (ps : List (RoseTree α)) : node a ↑(List.map mk ps) = mk (RoseTree.node a ps)

theorem UnorderedTree.node_pair_mk {α : Type u_1} (a : α) (p q : RoseTree α) : node a {mk p, mk q} = mk (RoseTree.node a [p, q])

theorem UnorderedTree.forest_inductionOn {α : Type u_1} {motive : Multiset (UnorderedTree α) → Prop} (F : Multiset (UnorderedTree α)) (h : ∀ (cs : List (RoseTree α)), motive ↑(List.map mk cs)) : motive F

Structural induction and recursion

An unordered tree is a label over a multiset of unordered trees. induction_on, fold and para are the induction, recursion and paramorphism principles of that description; a function defined through them needs no proof of invariance under RoseTree.Perm.

theorem UnorderedTree.induction_on {α : Type u_1} {motive : UnorderedTree α → Prop} (t : UnorderedTree α) (node : ∀ (a : α) (F : Multiset (UnorderedTree α)), (∀ (c : UnorderedTree α), c ∈ F → motive c) → motive (node a F)) : motive t

Induction on an unordered tree proves motive t for all t from motive (node a F) given motive c for every child c ∈ F.

def UnorderedTree.fold {α : Type u_1} {β : Type u_2} (f : α → Multiset β → β) : UnorderedTree α → β

The catamorphism replaces each node a F by f a of the multiset of folded children.

Equations

• UnorderedTree.fold f = Quotient.lift (RoseTree.fold fun (a : α) (bs : List β) => f a ↑bs) ⋯

theorem UnorderedTree.fold_mk {α : Type u_1} {β : Type u_2} (f : α → Multiset β → β) (t : RoseTree α) : fold f (mk t) = RoseTree.fold (fun (a : α) (bs : List β) => f a ↑bs) t

@[simp]

theorem UnorderedTree.fold_node {α : Type u_1} {β : Type u_2} (f : α → Multiset β → β) (a : α) (F : Multiset (UnorderedTree α)) : fold f (node a F) = f a (Multiset.map (fold f) F)

def UnorderedTree.para {α : Type u_1} {β : Type u_2} (f : α → Multiset (UnorderedTree α × β) → β) (t : UnorderedTree α) : β

The paramorphism passes f a each child together with its value. It is the fold into pairs whose first component rebuilds the subtree.

Equations

• UnorderedTree.para f t = (UnorderedTree.fold (fun (a : α) (ps : Multiset (UnorderedTree α × β)) => (UnorderedTree.node a (Multiset.map Prod.fst ps), f a ps)) t).2

@[simp]

theorem UnorderedTree.para_node {α : Type u_1} {β : Type u_2} (f : α → Multiset (UnorderedTree α × β) → β) (a : α) (F : Multiset (UnorderedTree α)) : para f (node a F) = f a (Multiset.map (fun (t : UnorderedTree α) => (t, para f t)) F)

The destructors of a node

@[simp]

theorem UnorderedTree.value_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : (node a F).value = a

@[simp]

theorem UnorderedTree.children_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : (node a F).children = F

theorem UnorderedTree.node_eta {α : Type u_1} (t : UnorderedTree α) : node t.value t.children = t

@[simp]

theorem UnorderedTree.node_inj {α : Type u_1} {a b : α} {F G : Multiset (UnorderedTree α)} : node a F = node b G ↔ a = b ∧ F = G

theorem UnorderedTree.node_injective {α : Type u_1} (a : α) : Function.Injective (node a)

Node count of a node

theorem UnorderedTree.numNodes_pos {α : Type u_1} (t : UnorderedTree α) : 0 < t.numNodes

@[simp]

theorem UnorderedTree.numNodes_node {α : Type u_1} (a : α) (F : Multiset (UnorderedTree α)) : (node a F).numNodes = (Multiset.map numNodes F).sum + 1

Height of a node

theorem UnorderedTree.height_lt_of_mem {α : Type u_1} (T : UnorderedTree α) (F : Multiset (UnorderedTree α)) (hT : T ∈ F) (a : α) : T.height < (node a F).height

Functoriality

def UnorderedTree.map {α : Type u_1} {β : Type u_2} (f : α → β) : UnorderedTree α → UnorderedTree β

Relabel every vertex of a nonplanar tree.

Equations

• UnorderedTree.map f = Quotient.map (RoseTree.map f) ⋯

theorem UnorderedTree.map_mk {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) : map f (mk t) = mk (RoseTree.map f t)

theorem UnorderedTree.map_leaf {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f (leaf a) = leaf (f a)

@[simp]

theorem UnorderedTree.map_id {α : Type u_1} (t : UnorderedTree α) : map id t = t

theorem UnorderedTree.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (t : UnorderedTree α) : map g (map f t) = map (g ∘ f) t

theorem UnorderedTree.map_node {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (cs : Multiset (UnorderedTree α)) : map f (node a cs) = node (f a) (Multiset.map (map f) cs)

@[simp]

theorem UnorderedTree.value_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).value = f t.value

theorem UnorderedTree.map_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : Function.Injective (map f)

Counting interactions

@[simp]

theorem UnorderedTree.numNodes_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).numNodes = t.numNodes

@[simp]

theorem UnorderedTree.height_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).height = t.height

@[simp]

theorem UnorderedTree.arity_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).arity = t.arity

@[simp]

theorem UnorderedTree.numLeaves_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : UnorderedTree α) : (map f t).numLeaves = t.numLeaves