Documentation

HopfAlgebras.Forests.Labelled

Labelled Rooted Forests #

This file defines labelled rooted forests as multisets of non-planar labelled rooted trees. It also defines labelled branches and labelled grafting, the analogue of the B_+ operator where the new root receives a specified label.

Main definitions #

LRootedForest α - non-planar labelled rooted forests
LRootedTree.branches - the forest below the root of a labelled tree
LRootedForest.graft - labelled grafting onto a new root
LRootedForest.butcherProduct - grafting a labelled forest onto a labelled tree root
LRootedForest.treeFactorial - product of labelled tree factorials
LRootedForest.erase - forget labels in a labelled forest
LRootedForest.mapLabels - change labels in a labelled forest

@[reducible, inline]

abbrev HopfAlgebras.LRootedForest (α : Type u) :

Non-planar labelled rooted forests.

Equations

HopfAlgebras.LRootedForest α = Multiset (HopfAlgebras.LRootedTree α)

Instances For

def HopfAlgebras.PLTree.ForestPerm {α : Type u} (ts us : List (PLTree α)) :

Two labelled planar tree lists represent the same non-planar labelled forest.

Equations

HopfAlgebras.PLTree.ForestPerm ts us = (↑(List.map HopfAlgebras.LRootedTree.ofPLTree ts) = ↑(List.map HopfAlgebras.LRootedTree.ofPLTree us))

Instances For

theorem HopfAlgebras.PLTree.ForestPerm.refl {α : Type u} (ts : List (PLTree α)) :

ForestPerm ts ts

theorem HopfAlgebras.PLTree.ForestPerm.symm {α : Type u} {ts us : List (PLTree α)} (h : ForestPerm ts us) :

ForestPerm us ts

theorem HopfAlgebras.PLTree.ForestPerm.trans {α : Type u} {ts us vs : List (PLTree α)} (h₁ : ForestPerm ts us) (h₂ : ForestPerm us vs) :

ForestPerm ts vs

theorem HopfAlgebras.PLTree.ForestPerm.of_list_perm {α : Type u} {ts us : List (PLTree α)} (h : ts.Perm us) :

ForestPerm ts us

theorem HopfAlgebras.PLTree.ForestPerm.of_forall₂_perm {α : Type u} {ts us : List (PLTree α)} (h : List.Forall₂ Perm ts us) :

ForestPerm ts us

theorem HopfAlgebras.PLTree.ForestPerm.cons_eq {α : Type u} {t u : PLTree α} {ts us : List (PLTree α)} (ht : LRootedTree.ofPLTree t = LRootedTree.ofPLTree u) (h : ForestPerm ts us) :

ForestPerm (t :: ts) (u :: us)

theorem HopfAlgebras.PLTree.ForestPerm.cons {α : Type u} {t u : PLTree α} {ts us : List (PLTree α)} (ht : t.Perm u) (h : ForestPerm ts us) :

ForestPerm (t :: ts) (u :: us)

theorem HopfAlgebras.PLTree.ForestPerm.append {α : Type u} {ts us vs ws : List (PLTree α)} (h₁ : ForestPerm ts us) (h₂ : ForestPerm vs ws) :

ForestPerm (ts ++ vs) (us ++ ws)

def HopfAlgebras.LRootedTree.branches {α : Type u} :

LRootedTree α → LRootedForest α

The forest immediately below the root of a non-planar labelled tree.

Equations

HopfAlgebras.LRootedTree.branches = Quotient.lift HopfAlgebras.LRootedTree.branchesAux✝ ⋯

Instances For

@[simp]

theorem HopfAlgebras.LRootedTree.branches_ofPLTree_node {α : Type u} (a : α) (ts : List (PLTree α)) :

(ofPLTree (PLTree.node a ts)).branches = ↑(List.map ofPLTree ts)

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

LRootedForest α

The empty labelled rooted forest.

Equations

HopfAlgebras.LRootedForest.empty = 0

Instances For

def HopfAlgebras.LRootedForest.singleton {α : Type u} (τ : LRootedTree α) :

LRootedForest α

The one-tree labelled forest.

Equations

HopfAlgebras.LRootedForest.singleton τ = {τ}

Instances For

def HopfAlgebras.LRootedForest.erase {α : Type u} (φ : LRootedForest α) :

Forget all labels in a labelled rooted forest.

Equations

φ.erase = Multiset.map HopfAlgebras.LRootedTree.erase φ

Instances For

def HopfAlgebras.LRootedForest.constLabel {α : Type u} (a : α) (φ : RootedForest) :

LRootedForest α

Label every vertex of a rooted forest by the same label.

Equations

HopfAlgebras.LRootedForest.constLabel a φ = Multiset.map (HopfAlgebras.LRootedTree.constLabel a) φ

Instances For

def HopfAlgebras.LRootedForest.mapLabels {α : Type u} {β : Type v} (f : α → β) (φ : LRootedForest α) :

LRootedForest β

Change all labels in a labelled rooted forest.

Equations

HopfAlgebras.LRootedForest.mapLabels f φ = Multiset.map (HopfAlgebras.LRootedTree.map f) φ

Instances For

def HopfAlgebras.LRootedForest.order {α : Type u} (φ : LRootedForest α) :

The total number of vertices in a labelled rooted forest.

Equations

φ.order = (Multiset.map HopfAlgebras.LRootedTree.order φ).sum

Instances For

def HopfAlgebras.LRootedForest.IsOfOrder {α : Type u} (φ : LRootedForest α) (n : ℕ) :

Predicate for labelled rooted forests of a fixed order.

Equations

φ.IsOfOrder n = (φ.order = n)

Instances For

def HopfAlgebras.LRootedForest.treeFactorial {α : Type u} (φ : LRootedForest α) :

The product of the tree factorials in a labelled rooted forest.

Equations

φ.treeFactorial = (Multiset.map HopfAlgebras.LRootedTree.treeFactorial φ).prod

Instances For

@[simp]

theorem HopfAlgebras.LRootedForest.erase_empty {α : Type u} :

empty.erase = RootedForest.empty

@[simp]

theorem HopfAlgebras.LRootedForest.constLabel_empty {α : Type u} (a : α) :

constLabel a RootedForest.empty = empty

@[simp]

theorem HopfAlgebras.LRootedForest.constLabel_zero {α : Type u} (a : α) :

constLabel a 0 = 0

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_empty {α : Type u} {β : Type v} (f : α → β) :

mapLabels f empty = empty

@[simp]

theorem HopfAlgebras.LRootedForest.order_empty {α : Type u} :

empty.order = 0

@[simp]

theorem HopfAlgebras.LRootedForest.order_zero {α : Type u} :

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_empty {α : Type u} :

empty.treeFactorial = 1

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_zero {α : Type u} :

treeFactorial 0 = 1

@[simp]

theorem HopfAlgebras.LRootedForest.erase_singleton {α : Type u} (τ : LRootedTree α) :

(singleton τ).erase = RootedForest.singleton τ.erase

theorem HopfAlgebras.LRootedForest.erase_out_perm {α : Type u} (φ : LRootedForest α) :

(List.map LRootedTree.erase (Quotient.out φ)).Perm (Quotient.out φ.erase)

theorem HopfAlgebras.LRootedForest.constLabel_out_perm {α : Type u} (a : α) (φ : RootedForest) :

(List.map (LRootedTree.constLabel a) (Quotient.out φ)).Perm (Quotient.out (constLabel a φ))

theorem HopfAlgebras.LRootedForest.mapLabels_out_perm {α : Type u} {β : Type v} (f : α → β) (φ : LRootedForest α) :

(List.map (LRootedTree.map f) (Quotient.out φ)).Perm (Quotient.out (mapLabels f φ))

@[simp]

theorem HopfAlgebras.LRootedForest.constLabel_singleton {α : Type u} (a : α) (τ : RootedTree) :

constLabel a (RootedForest.singleton τ) = singleton (LRootedTree.constLabel a τ)

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_singleton {α : Type u} {β : Type v} (f : α → β) (τ : LRootedTree α) :

mapLabels f (singleton τ) = singleton (LRootedTree.map f τ)

@[simp]

theorem HopfAlgebras.LRootedForest.order_singleton {α : Type u} (τ : LRootedTree α) :

(singleton τ).order = τ.order

theorem HopfAlgebras.LRootedForest.singleton_ne_zero {α : Type u} (τ : LRootedTree α) :

singleton τ ≠ 0

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_singleton {α : Type u} (τ : LRootedTree α) :

(singleton τ).treeFactorial = τ.treeFactorial

@[simp]

theorem HopfAlgebras.LRootedForest.erase_add {α : Type u} (φ ψ : LRootedForest α) :

(φ + ψ).erase = φ.erase + ψ.erase

@[simp]

theorem HopfAlgebras.LRootedForest.constLabel_add {α : Type u} (a : α) (φ ψ : RootedForest) :

constLabel a (φ + ψ) = constLabel a φ + constLabel a ψ

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_add {α : Type u} {β : Type v} (f : α → β) (φ ψ : LRootedForest α) :

mapLabels f (φ + ψ) = mapLabels f φ + mapLabels f ψ

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_id {α : Type u} (φ : LRootedForest α) :

mapLabels id φ = φ

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_comp {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (φ : LRootedForest α) :

mapLabels g (mapLabels f φ) = mapLabels (g ∘ f) φ

@[simp]

theorem HopfAlgebras.LRootedForest.erase_mapLabels {α : Type u} {β : Type v} (f : α → β) (φ : LRootedForest α) :

(mapLabels f φ).erase = φ.erase

@[simp]

theorem HopfAlgebras.LRootedForest.erase_constLabel {α : Type u} (a : α) (φ : RootedForest) :

(constLabel a φ).erase = φ

theorem HopfAlgebras.LRootedForest.constLabel_injective {α : Type u} (a : α) :

Function.Injective (constLabel a)

@[simp]

theorem HopfAlgebras.LRootedForest.constLabel_eq_constLabel_iff {α : Type u} (a : α) {φ ψ : RootedForest} :

constLabel a φ = constLabel a ψ ↔ φ = ψ

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (φ : RootedForest) :

mapLabels f (constLabel a φ) = constLabel (f a) φ

theorem HopfAlgebras.LRootedForest.mapLabels_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) :

Function.Injective (mapLabels f)

theorem HopfAlgebras.LRootedForest.mapLabels_eq_mapLabels_iff_of_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) {φ ψ : LRootedForest α} :

mapLabels f φ = mapLabels f ψ ↔ φ = ψ

@[simp]

theorem HopfAlgebras.LRootedForest.order_add {α : Type u} (φ ψ : LRootedForest α) :

(φ + ψ).order = φ.order + ψ.order

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_add {α : Type u} (φ ψ : LRootedForest α) :

(φ + ψ).treeFactorial = φ.treeFactorial * ψ.treeFactorial

@[simp]

theorem HopfAlgebras.LRootedForest.order_erase {α : Type u} (φ : LRootedForest α) :

φ.erase.order = φ.order

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_erase {α : Type u} (φ : LRootedForest α) :

φ.erase.treeFactorial = φ.treeFactorial

@[simp]

theorem HopfAlgebras.LRootedForest.order_ofPLTree_list {α : Type u} (ts : List (PLTree α)) :

order ↑(List.map LRootedTree.ofPLTree ts) = PLTree.orderList ts

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_ofPLTree_list {α : Type u} (ts : List (PLTree α)) :

treeFactorial ↑(List.map LRootedTree.ofPLTree ts) = PLTree.treeFactorialList ts

@[simp]

theorem HopfAlgebras.LRootedForest.order_constLabel {α : Type u} (a : α) (φ : RootedForest) :

(constLabel a φ).order = φ.order

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_constLabel {α : Type u} (a : α) (φ : RootedForest) :

(constLabel a φ).treeFactorial = φ.treeFactorial

@[simp]

theorem HopfAlgebras.LRootedForest.order_mapLabels {α : Type u} {β : Type v} (f : α → β) (φ : LRootedForest α) :

(mapLabels f φ).order = φ.order

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_mapLabels {α : Type u} {β : Type v} (f : α → β) (φ : LRootedForest α) :

(mapLabels f φ).treeFactorial = φ.treeFactorial

theorem HopfAlgebras.LRootedForest.treeFactorial_pos {α : Type u} (φ : LRootedForest α) :

0 < φ.treeFactorial

theorem HopfAlgebras.LRootedForest.treeFactorial_ne_zero {α : Type u} (φ : LRootedForest α) :

φ.treeFactorial ≠ 0

theorem HopfAlgebras.LRootedForest.order_coe_cons_pos {α : Type u} (τ : LRootedTree α) (ts : List (LRootedTree α)) :

0 < order ↑(τ :: ts)

@[simp]

theorem HopfAlgebras.LRootedForest.order_eq_zero_iff {α : Type u} (φ : LRootedForest α) :

φ.order = 0 ↔ φ = 0

theorem HopfAlgebras.LRootedForest.order_pos_iff_ne_zero {α : Type u} (φ : LRootedForest α) :

0 < φ.order ↔ φ ≠ 0

noncomputable def HopfAlgebras.LRootedForest.graft {α : Type u} (a : α) :

LRootedForest α → LRootedTree α

Graft all roots in a labelled forest onto a new root with label a.

Equations

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

Instances For

@[simp]

theorem HopfAlgebras.LRootedForest.graft_coe {α : Type u} (a : α) (ts : List (LRootedTree α)) :

graft a ↑ts = LRootedTree.ofPLTree (PLTree.node a (List.map Quotient.out ts))

@[simp]

theorem HopfAlgebras.LRootedForest.graft_empty {α : Type u} (a : α) :

graft a empty = LRootedTree.ofPLTree (PLTree.node a [])

@[simp]

theorem HopfAlgebras.LRootedForest.branches_graft {α : Type u} (a : α) (φ : LRootedForest α) :

(graft a φ).branches = φ

@[simp]

theorem HopfAlgebras.LRootedForest.rootLabel_graft {α : Type u} (a : α) (φ : LRootedForest α) :

(graft a φ).rootLabel = a

theorem HopfAlgebras.LRootedForest.graft_injective {α : Type u} (a : α) :

Function.Injective (graft a)

@[simp]

theorem HopfAlgebras.LRootedForest.graft_eq_graft_iff {α : Type u} (a : α) (φ ψ : LRootedForest α) :

graft a φ = graft a ψ ↔ φ = ψ

@[simp]

theorem HopfAlgebras.LRootedForest.graft_eq_graft_iff_rootLabel_branches {α : Type u} (a b : α) (φ ψ : LRootedForest α) :

graft a φ = graft b ψ ↔ a = b ∧ φ = ψ

theorem HopfAlgebras.LRootedForest.graft_ofPLTree_list {α : Type u} (a : α) (ts : List (PLTree α)) :

graft a ↑(List.map LRootedTree.ofPLTree ts) = LRootedTree.ofPLTree (PLTree.node a ts)

theorem HopfAlgebras.LRootedForest.ofPLTree_node_eq_of_forestPerm {α : Type u} (a : α) {ts us : List (PLTree α)} (h : PLTree.ForestPerm ts us) :

LRootedTree.ofPLTree (PLTree.node a ts) = LRootedTree.ofPLTree (PLTree.node a us)

@[simp]

theorem HopfAlgebras.LRootedForest.graft_branches_ofPLTree_node {α : Type u} (a : α) (ts : List (PLTree α)) :

graft a (LRootedTree.ofPLTree (PLTree.node a ts)).branches = LRootedTree.ofPLTree (PLTree.node a ts)

@[simp]

theorem HopfAlgebras.LRootedForest.graft_branches {α : Type u} (τ : LRootedTree α) :

graft τ.rootLabel τ.branches = τ

@[simp]

theorem HopfAlgebras.LRootedForest.order_graft {α : Type u} (a : α) (φ : LRootedForest α) :

(graft a φ).order = 1 + φ.order

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_graft {α : Type u} {β : Type v} (f : α → β) (a : α) (φ : LRootedForest α) :

LRootedTree.map f (graft a φ) = graft (f a) (mapLabels f φ)

@[simp]

theorem HopfAlgebras.LRootedForest.erase_graft {α : Type u} (a : α) (φ : LRootedForest α) :

(graft a φ).erase = φ.erase.graft

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_graft {α : Type u} (a : α) (φ : LRootedForest α) :

(graft a φ).treeFactorial = (1 + φ.order) * φ.treeFactorial

theorem HopfAlgebras.LRootedForest.treeFactorial_branches {α : Type u} (τ : LRootedTree α) :

τ.order * τ.branches.treeFactorial = τ.treeFactorial

@[simp]

theorem HopfAlgebras.LRootedForest.erase_branches {α : Type u} (τ : LRootedTree α) :

τ.branches.erase = τ.erase.branches

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_branches {α : Type u} {β : Type v} (f : α → β) (τ : LRootedTree α) :

mapLabels f τ.branches = (LRootedTree.map f τ).branches

@[simp]

theorem HopfAlgebras.LRootedForest.order_branches {α : Type u} (τ : LRootedTree α) :

1 + τ.branches.order = τ.order

theorem HopfAlgebras.LRootedForest.order_branches_lt {α : Type u} (τ : LRootedTree α) :

τ.branches.order < τ.order

theorem HopfAlgebras.LRootedForest.branches_eq_zero_of_order_eq_one {α : Type u} (τ : LRootedTree α) (h : τ.order = 1) :

τ.branches = 0

theorem HopfAlgebras.LRootedForest.order_eq_one_iff_branches_eq_zero {α : Type u} (τ : LRootedTree α) :

τ.order = 1 ↔ τ.branches = 0

theorem HopfAlgebras.LRootedForest.order_eq_one_iff_eq_graft_root_zero {α : Type u} (τ : LRootedTree α) :

τ.order = 1 ↔ τ = graft τ.rootLabel 0

noncomputable def HopfAlgebras.LRootedForest.butcherProduct {α : Type u} (φ : LRootedForest α) (τ : LRootedTree α) :

Graft a labelled rooted forest onto the root of a labelled rooted tree.

Equations

φ.butcherProduct τ = HopfAlgebras.LRootedForest.graft τ.rootLabel (φ + τ.branches)

Instances For

@[simp]

theorem HopfAlgebras.LRootedForest.butcherProduct_zero_left {α : Type u} (τ : LRootedTree α) :

butcherProduct 0 τ = τ

@[simp]

theorem HopfAlgebras.LRootedForest.butcherProduct_empty_left {α : Type u} (τ : LRootedTree α) :

empty.butcherProduct τ = τ

@[simp]

theorem HopfAlgebras.LRootedForest.butcherProduct_assoc {α : Type u} (φ ψ : LRootedForest α) (τ : LRootedTree α) :

φ.butcherProduct (ψ.butcherProduct τ) = (φ + ψ).butcherProduct τ

@[simp]

theorem HopfAlgebras.LRootedForest.rootLabel_butcherProduct {α : Type u} (φ : LRootedForest α) (τ : LRootedTree α) :

(φ.butcherProduct τ).rootLabel = τ.rootLabel

@[simp]

theorem HopfAlgebras.LRootedForest.branches_butcherProduct {α : Type u} (φ : LRootedForest α) (τ : LRootedTree α) :

(φ.butcherProduct τ).branches = φ + τ.branches

theorem HopfAlgebras.LRootedForest.butcherProduct_ofPLTree_list {α : Type u} (ts : List (PLTree α)) (t : PLTree α) :

LRootedTree.ofPLTree (PLTree.butcherProduct ts t) = butcherProduct (↑(List.map LRootedTree.ofPLTree ts)) (LRootedTree.ofPLTree t)

theorem HopfAlgebras.LRootedForest.butcherProduct_eq_iff_rootLabel_branches {α : Type u} (φ ψ : LRootedForest α) (τ σ : LRootedTree α) :

φ.butcherProduct τ = ψ.butcherProduct σ ↔ τ.rootLabel = σ.rootLabel ∧ φ + τ.branches = ψ + σ.branches

theorem HopfAlgebras.LRootedForest.butcherProduct_injective_left {α : Type u} (τ : LRootedTree α) :

Function.Injective fun (φ : LRootedForest α) => φ.butcherProduct τ

theorem HopfAlgebras.LRootedForest.butcherProduct_injective_right {α : Type u} (φ : LRootedForest α) :

Function.Injective φ.butcherProduct

@[simp]

theorem HopfAlgebras.LRootedForest.butcherProduct_left_eq_left_iff {α : Type u} (φ ψ : LRootedForest α) (τ : LRootedTree α) :

φ.butcherProduct τ = ψ.butcherProduct τ ↔ φ = ψ

@[simp]

theorem HopfAlgebras.LRootedForest.butcherProduct_right_eq_right_iff {α : Type u} (φ : LRootedForest α) (τ σ : LRootedTree α) :

φ.butcherProduct τ = φ.butcherProduct σ ↔ τ = σ

@[simp]

theorem HopfAlgebras.LRootedForest.order_butcherProduct {α : Type u} (φ : LRootedForest α) (τ : LRootedTree α) :

(φ.butcherProduct τ).order = φ.order + τ.order

@[simp]

theorem HopfAlgebras.LRootedForest.erase_butcherProduct {α : Type u} (φ : LRootedForest α) (τ : LRootedTree α) :

(φ.butcherProduct τ).erase = φ.erase.butcherProduct τ.erase

@[simp]

theorem HopfAlgebras.LRootedForest.mapLabels_butcherProduct {α : Type u} {β : Type v} (f : α → β) (φ : LRootedForest α) (τ : LRootedTree α) :

LRootedTree.map f (φ.butcherProduct τ) = (mapLabels f φ).butcherProduct (LRootedTree.map f τ)

@[simp]

theorem HopfAlgebras.LRootedForest.treeFactorial_butcherProduct {α : Type u} (φ : LRootedForest α) (τ : LRootedTree α) :

(φ.butcherProduct τ).treeFactorial = (φ.order + τ.order) * (φ + τ.branches).treeFactorial