Admissible Cuts of Labelled Rooted Trees

This file defines finite admissible-cut data for planar labelled rooted trees. It is the labelled analogue of HopfAlgebras.Cuts.Rooted, and provides the combinatorial input for labelled BCK-type coproducts.

Main definitions

• PLTree.RootCut - a labelled admissible cut which keeps the root component
• PLTree.Cut - a labelled admissible cut, allowing the full cut
• PLTree.cuts - finite list of labelled admissible cuts
• PLTree.coproductTerms - labelled cuts as forest-pair coproduct terms

structure HopfAlgebras.PLTree.RootCut (α : Type u) : Type u

A cut below the root, so the trunk remains a non-empty labelled tree.

• pruned : List (PLTree α)
• trunk : PLTree α

def HopfAlgebras.PLTree.instReprRootCut.repr {α✝ : Type u_1} [Repr α✝] : RootCut α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HopfAlgebras.PLTree.instReprRootCut {α✝ : Type u_1} [Repr α✝] : Repr (RootCut α✝)

Equations

• HopfAlgebras.PLTree.instReprRootCut = { reprPrec := HopfAlgebras.PLTree.instReprRootCut.repr }

structure HopfAlgebras.PLTree.ChildCut (α : Type u) : Type u

A child-level labelled cut choice. none means the edge above the child is cut.

• pruned : List (PLTree α)
• trunk? : Option (PLTree α)

@[implicit_reducible]

instance HopfAlgebras.PLTree.instReprChildCut {α✝ : Type u_1} [Repr α✝] : Repr (ChildCut α✝)

Equations

• HopfAlgebras.PLTree.instReprChildCut = { reprPrec := HopfAlgebras.PLTree.instReprChildCut.repr }

def HopfAlgebras.PLTree.instReprChildCut.repr {α✝ : Type u_1} [Repr α✝] : ChildCut α✝ → ℕ → Std.Format

Equations

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

structure HopfAlgebras.PLTree.RootCutList (α : Type u) : Type u

A root-preserving labelled cut list accumulated across a list of children.

• pruned : List (PLTree α)
• trunks : List (PLTree α)

def HopfAlgebras.PLTree.instReprRootCutList.repr {α✝ : Type u_1} [Repr α✝] : RootCutList α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HopfAlgebras.PLTree.instReprRootCutList {α✝ : Type u_1} [Repr α✝] : Repr (RootCutList α✝)

Equations

• HopfAlgebras.PLTree.instReprRootCutList = { reprPrec := HopfAlgebras.PLTree.instReprRootCutList.repr }

structure HopfAlgebras.PLTree.Cut (α : Type u) : Type u

An admissible cut of a planar labelled rooted tree. none is the full cut.

• pruned : List (PLTree α)
• trunk? : Option (PLTree α)

def HopfAlgebras.PLTree.instReprCut.repr {α✝ : Type u_1} [Repr α✝] : Cut α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HopfAlgebras.PLTree.instReprCut {α✝ : Type u_1} [Repr α✝] : Repr (Cut α✝)

Equations

• HopfAlgebras.PLTree.instReprCut = { reprPrec := HopfAlgebras.PLTree.instReprCut.repr }

def HopfAlgebras.PLTree.RootCut.erase {α : Type u} (c : RootCut α) : PTree.RootCut

Forget labels in a root-preserving labelled cut.

Equations

• c.erase = { pruned := List.map HopfAlgebras.PLTree.erase c.pruned, trunk := c.trunk.erase }

def HopfAlgebras.PLTree.RootCut.map {α : Type u} {β : Type v} (f : α → β) (c : RootCut α) : RootCut β

Relabel a root-preserving labelled cut.

Equations

• HopfAlgebras.PLTree.RootCut.map f c = { pruned := List.map (HopfAlgebras.PLTree.map f) c.pruned, trunk := HopfAlgebras.PLTree.map f c.trunk }

def HopfAlgebras.PLTree.RootCut.constLabel {α : Type u} (a : α) (c : PTree.RootCut) : RootCut α

Label every vertex in an unlabelled root-preserving cut by the same label.

Equations

• HopfAlgebras.PLTree.RootCut.constLabel a c = { pruned := List.map (HopfAlgebras.PLTree.constLabel a) c.pruned, trunk := HopfAlgebras.PLTree.constLabel a c.trunk }

@[simp]

theorem HopfAlgebras.PLTree.RootCut.erase_constLabel {α : Type u} (a : α) (c : PTree.RootCut) : (constLabel a c).erase = c

@[simp]

theorem HopfAlgebras.PLTree.RootCut.map_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (c : PTree.RootCut) : map f (constLabel a c) = constLabel (f a) c

def HopfAlgebras.PLTree.RootCut.noPrunedTrunk? {α : Type u} (c : RootCut α) : Option (PLTree α)

The trunk of a root cut, only when the cut prunes no labelled trees.

Equations

• c.noPrunedTrunk? = match c.pruned with | [] => some c.trunk | head :: tail => none

def HopfAlgebras.PLTree.ChildCut.erase {α : Type u} (c : ChildCut α) : PTree.ChildCut

Forget labels in a labelled child cut choice.

Equations

• c.erase = { pruned := List.map HopfAlgebras.PLTree.erase c.pruned, trunk? := Option.map HopfAlgebras.PLTree.erase c.trunk? }

def HopfAlgebras.PLTree.ChildCut.map {α : Type u} {β : Type v} (f : α → β) (c : ChildCut α) : ChildCut β

Relabel a labelled child cut choice.

Equations

• HopfAlgebras.PLTree.ChildCut.map f c = { pruned := List.map (HopfAlgebras.PLTree.map f) c.pruned, trunk? := Option.map (HopfAlgebras.PLTree.map f) c.trunk? }

def HopfAlgebras.PLTree.ChildCut.constLabel {α : Type u} (a : α) (c : PTree.ChildCut) : ChildCut α

Label every vertex in an unlabelled child cut by the same label.

Equations

• HopfAlgebras.PLTree.ChildCut.constLabel a c = { pruned := List.map (HopfAlgebras.PLTree.constLabel a) c.pruned, trunk? := Option.map (HopfAlgebras.PLTree.constLabel a) c.trunk? }

@[simp]

theorem HopfAlgebras.PLTree.ChildCut.erase_constLabel {α : Type u} (a : α) (c : PTree.ChildCut) : (constLabel a c).erase = c

@[simp]

theorem HopfAlgebras.PLTree.ChildCut.map_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (c : PTree.ChildCut) : map f (constLabel a c) = constLabel (f a) c

def HopfAlgebras.PLTree.ChildCut.noPrunedTrunk? {α : Type u} (c : ChildCut α) : Option (PLTree α)

The trunk of a child cut choice, only when the choice prunes no labelled trees.

Equations

• c.noPrunedTrunk? = match c.pruned with | [] => c.trunk? | head :: tail => none

def HopfAlgebras.PLTree.ChildCut.prunedForest {α : Type u} (c : ChildCut α) : LRootedForest α

The pruned forest of a labelled child cut choice.

Equations

• c.prunedForest = ↑(List.map HopfAlgebras.LRootedTree.ofPLTree c.pruned)

def HopfAlgebras.PLTree.ChildCut.trunkForest {α : Type u} (c : ChildCut α) : LRootedForest α

The trunk forest of a labelled child cut choice. Cutting the edge gives the empty trunk.

Equations

• c.trunkForest = match c.trunk? with | none => 0 | some trunk => HopfAlgebras.LRootedForest.singleton (HopfAlgebras.LRootedTree.ofPLTree trunk)

def HopfAlgebras.PLTree.ChildCut.coproductTerm {α : Type u} (c : ChildCut α) : LRootedForest α × LRootedForest α

The labelled coproduct term encoded by a child cut choice.

Equations

• c.coproductTerm = (c.prunedForest, c.trunkForest)

def HopfAlgebras.PLTree.RootCutList.erase {α : Type u} (c : RootCutList α) : PTree.RootCutList

Forget labels in a root-preserving labelled cut list.

Equations

• c.erase = { pruned := List.map HopfAlgebras.PLTree.erase c.pruned, trunks := List.map HopfAlgebras.PLTree.erase c.trunks }

def HopfAlgebras.PLTree.RootCutList.map {α : Type u} {β : Type v} (f : α → β) (c : RootCutList α) : RootCutList β

Relabel a root-preserving labelled cut list.

Equations

• HopfAlgebras.PLTree.RootCutList.map f c = { pruned := List.map (HopfAlgebras.PLTree.map f) c.pruned, trunks := List.map (HopfAlgebras.PLTree.map f) c.trunks }

def HopfAlgebras.PLTree.RootCutList.constLabel {α : Type u} (a : α) (c : PTree.RootCutList) : RootCutList α

Label every vertex in an unlabelled root-preserving cut list by the same label.

Equations

• HopfAlgebras.PLTree.RootCutList.constLabel a c = { pruned := List.map (HopfAlgebras.PLTree.constLabel a) c.pruned, trunks := List.map (HopfAlgebras.PLTree.constLabel a) c.trunks }

@[simp]

theorem HopfAlgebras.PLTree.RootCutList.erase_constLabel {α : Type u} (a : α) (c : PTree.RootCutList) : (constLabel a c).erase = c

@[simp]

theorem HopfAlgebras.PLTree.RootCutList.map_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (c : PTree.RootCutList) : map f (constLabel a c) = constLabel (f a) c

def HopfAlgebras.PLTree.RootCutList.noPrunedTrunks? {α : Type u} (c : RootCutList α) : Option (List (PLTree α))

The trunks of a root-preserving cut list, only when the cut prunes no labelled trees.

Equations

• c.noPrunedTrunks? = match c.pruned with | [] => some c.trunks | head :: tail => none

def HopfAlgebras.PLTree.RootCutList.prunedForest {α : Type u} (c : RootCutList α) : LRootedForest α

The pruned forest of a labelled root-preserving cut list.

Equations

• c.prunedForest = ↑(List.map HopfAlgebras.LRootedTree.ofPLTree c.pruned)

def HopfAlgebras.PLTree.RootCutList.trunkForest {α : Type u} (c : RootCutList α) : LRootedForest α

The trunk forest of a labelled root-preserving cut list.

Equations

• c.trunkForest = ↑(List.map HopfAlgebras.LRootedTree.ofPLTree c.trunks)

def HopfAlgebras.PLTree.RootCutList.coproductTerm {α : Type u} (c : RootCutList α) : LRootedForest α × LRootedForest α

The labelled coproduct term encoded by a root-preserving cut list.

Equations

• c.coproductTerm = (c.prunedForest, c.trunkForest)

def HopfAlgebras.PLTree.Cut.erase {α : Type u} (c : Cut α) : PTree.Cut

Forget labels in a labelled admissible cut.

Equations

• c.erase = { pruned := List.map HopfAlgebras.PLTree.erase c.pruned, trunk? := Option.map HopfAlgebras.PLTree.erase c.trunk? }

def HopfAlgebras.PLTree.Cut.map {α : Type u} {β : Type v} (f : α → β) (c : Cut α) : Cut β

Relabel a labelled admissible cut.

Equations

• HopfAlgebras.PLTree.Cut.map f c = { pruned := List.map (HopfAlgebras.PLTree.map f) c.pruned, trunk? := Option.map (HopfAlgebras.PLTree.map f) c.trunk? }

def HopfAlgebras.PLTree.Cut.constLabel {α : Type u} (a : α) (c : PTree.Cut) : Cut α

Label every vertex in an unlabelled admissible cut by the same label.

Equations

• HopfAlgebras.PLTree.Cut.constLabel a c = { pruned := List.map (HopfAlgebras.PLTree.constLabel a) c.pruned, trunk? := Option.map (HopfAlgebras.PLTree.constLabel a) c.trunk? }

@[simp]

theorem HopfAlgebras.PLTree.Cut.erase_constLabel {α : Type u} (a : α) (c : PTree.Cut) : (constLabel a c).erase = c

@[simp]

theorem HopfAlgebras.PLTree.Cut.map_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (c : PTree.Cut) : map f (constLabel a c) = constLabel (f a) c

def HopfAlgebras.PLTree.RootCut.Perm {α : Type u} (c d : RootCut α) : Prop

Equations

• c.Perm d = (HopfAlgebras.PLTree.ForestPerm c.pruned d.pruned ∧ HopfAlgebras.LRootedTree.ofPLTree c.trunk = HopfAlgebras.LRootedTree.ofPLTree d.trunk)

theorem HopfAlgebras.PLTree.RootCut.Perm.refl {α : Type u} (c : RootCut α) : c.Perm c

theorem HopfAlgebras.PLTree.RootCut.Perm.trans {α : Type u} {c d e : RootCut α} (hcd : c.Perm d) (hde : d.Perm e) : c.Perm e

def HopfAlgebras.PLTree.OptionPerm {α : Type u} : Option (PLTree α) → Option (PLTree α) → Prop

Equations

• HopfAlgebras.PLTree.OptionPerm none none = True
• HopfAlgebras.PLTree.OptionPerm (some t) (some u) = (HopfAlgebras.LRootedTree.ofPLTree t = HopfAlgebras.LRootedTree.ofPLTree u)
• HopfAlgebras.PLTree.OptionPerm x✝¹ x✝ = False

theorem HopfAlgebras.PLTree.OptionPerm.refl {α : Type u} (t : Option (PLTree α)) : OptionPerm t t

theorem HopfAlgebras.PLTree.OptionPerm.trans {α : Type u} {t u v : Option (PLTree α)} (htu : OptionPerm t u) (huv : OptionPerm u v) : OptionPerm t v

def HopfAlgebras.PLTree.ChildCut.Perm {α : Type u} (c d : ChildCut α) : Prop

Equations

• c.Perm d = (HopfAlgebras.PLTree.ForestPerm c.pruned d.pruned ∧ HopfAlgebras.PLTree.OptionPerm c.trunk? d.trunk?)

theorem HopfAlgebras.PLTree.ChildCut.Perm.refl {α : Type u} (c : ChildCut α) : c.Perm c

theorem HopfAlgebras.PLTree.ChildCut.Perm.trans {α : Type u} {c d e : ChildCut α} (hcd : c.Perm d) (hde : d.Perm e) : c.Perm e

theorem HopfAlgebras.PLTree.ChildCut.Perm.cutEdge {α : Type u} {t u : PLTree α} (h : t.Perm u) : { pruned := [t], trunk? := none }.Perm { pruned := [u], trunk? := none }

theorem HopfAlgebras.PLTree.ChildCut.Perm.of_rootCut {α : Type u} {c d : RootCut α} (h : c.Perm d) : { pruned := c.pruned, trunk? := some c.trunk }.Perm { pruned := d.pruned, trunk? := some d.trunk }

def HopfAlgebras.PLTree.RootCutList.Perm {α : Type u} (c d : RootCutList α) : Prop

Equations

• c.Perm d = (HopfAlgebras.PLTree.ForestPerm c.pruned d.pruned ∧ HopfAlgebras.PLTree.ForestPerm c.trunks d.trunks)

theorem HopfAlgebras.PLTree.RootCutList.Perm.refl {α : Type u} (c : RootCutList α) : c.Perm c

theorem HopfAlgebras.PLTree.RootCutList.Perm.trans {α : Type u} {c d e : RootCutList α} (hcd : c.Perm d) (hde : d.Perm e) : c.Perm e

def HopfAlgebras.PLTree.RootCutList.consChild {α : Type u} (c : ChildCut α) (r : RootCutList α) : RootCutList α

Equations

• HopfAlgebras.PLTree.RootCutList.consChild c r = { pruned := c.pruned ++ r.pruned, trunks := match c.trunk? with | none => r.trunks | some trunk => trunk :: r.trunks }

@[simp]

theorem HopfAlgebras.PLTree.RootCutList.prunedForest_consChild {α : Type u} (c : ChildCut α) (r : RootCutList α) : (consChild c r).prunedForest = c.prunedForest + r.prunedForest

@[simp]

theorem HopfAlgebras.PLTree.RootCutList.trunkForest_consChild {α : Type u} (c : ChildCut α) (r : RootCutList α) : (consChild c r).trunkForest = c.trunkForest + r.trunkForest

@[simp]

theorem HopfAlgebras.PLTree.RootCutList.coproductTerm_consChild {α : Type u} (c : ChildCut α) (r : RootCutList α) : (consChild c r).coproductTerm = c.coproductTerm + r.coproductTerm

@[simp]

theorem HopfAlgebras.PLTree.RootCutList.coproductTerm_mk_consChild {α : Type u} (c : ChildCut α) (r : RootCutList α) : { pruned := c.pruned ++ r.pruned, trunks := match c.trunk? with | none => r.trunks | some trunk => trunk :: r.trunks }.coproductTerm = c.coproductTerm + r.coproductTerm

@[simp]

theorem HopfAlgebras.PLTree.RootCutList.map_consChild {α : Type u} {β : Type v} (f : α → β) (c : ChildCut α) (r : RootCutList α) : map f (consChild c r) = consChild (ChildCut.map f c) (map f r)

@[simp]

theorem HopfAlgebras.PLTree.RootCutList.constLabel_consChild {α : Type u} (a : α) (c : PTree.ChildCut) (r : PTree.RootCutList) : constLabel a (PTree.RootCutList.consChild c r) = consChild (ChildCut.constLabel a c) (constLabel a r)

theorem HopfAlgebras.PLTree.RootCutList.Perm.consChild {α : Type u} {c d : ChildCut α} {r s : RootCutList α} (hc : c.Perm d) (hr : r.Perm s) : (RootCutList.consChild c r).Perm (RootCutList.consChild d s)

theorem HopfAlgebras.PLTree.RootCutList.Perm.consChild_swap {α : Type u} (c d : ChildCut α) (r : RootCutList α) : (RootCutList.consChild c (RootCutList.consChild d r)).Perm (RootCutList.consChild d (RootCutList.consChild c r))

theorem HopfAlgebras.PLTree.RootCutList.Perm.combine {α : Type u} {c d : ChildCut α} {r s : RootCutList α} (hc : c.Perm d) (hr : r.Perm s) : { pruned := c.pruned ++ r.pruned, trunks := match c.trunk? with | none => r.trunks | some trunk => trunk :: r.trunks }.Perm { pruned := d.pruned ++ s.pruned, trunks := match d.trunk? with | none => s.trunks | some trunk => trunk :: s.trunks }

theorem HopfAlgebras.PLTree.rootCut_perm_of_rootCutList_perm {α : Type u} (a : α) {c d : RootCutList α} (h : c.Perm d) : { pruned := c.pruned, trunk := node a c.trunks }.Perm { pruned := d.pruned, trunk := node a d.trunks }

def HopfAlgebras.PLTree.Cut.Perm {α : Type u} (c d : Cut α) : Prop

Equations

• c.Perm d = (HopfAlgebras.PLTree.ForestPerm c.pruned d.pruned ∧ HopfAlgebras.PLTree.OptionPerm c.trunk? d.trunk?)

theorem HopfAlgebras.PLTree.Cut.Perm.refl {α : Type u} (c : Cut α) : c.Perm c

theorem HopfAlgebras.PLTree.Cut.Perm.trans {α : Type u} {c d e : Cut α} (hcd : c.Perm d) (hde : d.Perm e) : c.Perm e

theorem HopfAlgebras.PLTree.Cut.Perm.full {α : Type u} {t u : PLTree α} (h : t.Perm u) : { pruned := [t], trunk? := none }.Perm { pruned := [u], trunk? := none }

theorem HopfAlgebras.PLTree.Cut.Perm.of_rootCut {α : Type u} {c d : RootCut α} (h : c.Perm d) : { pruned := c.pruned, trunk? := some c.trunk }.Perm { pruned := d.pruned, trunk? := some d.trunk }

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

@[irreducible]

def HopfAlgebras.PLTree.rootCuts {α : Type u} : PLTree α → List (RootCut α)

Labelled admissible cuts which keep the root component.

Equations

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

@[irreducible]

def HopfAlgebras.PLTree.childCuts {α : Type u} (t : PLTree α) : List (ChildCut α)

Choices for a labelled child: cut the edge above it, or keep it with a root-preserving cut.

Equations

• t.childCuts = { pruned := [t], trunk? := none } :: List.map (fun (c : HopfAlgebras.PLTree.RootCut α) => { pruned := c.pruned, trunk? := some c.trunk }) t.rootCuts

@[irreducible]

def HopfAlgebras.PLTree.rootCutsList {α : Type u} : List (PLTree α) → List (RootCutList α)

Combine labelled child cut choices into root-preserving cuts.

Equations

• One or more equations did not get rendered due to their size.
• HopfAlgebras.PLTree.rootCutsList [] = [{ pruned := [], trunks := [] }]

theorem HopfAlgebras.PLTree.rootCuts_erase {α : Type u} (t : PLTree α) : List.map RootCut.erase t.rootCuts = t.erase.rootCuts

Labelled root-preserving cuts erase to the corresponding unlabelled cuts.

theorem HopfAlgebras.PLTree.childCuts_erase {α : Type u} (t : PLTree α) : List.map ChildCut.erase t.childCuts = t.erase.childCuts

Labelled child cut choices erase to the corresponding unlabelled choices.

theorem HopfAlgebras.PLTree.rootCutsList_erase {α : Type u} (ts : List (PLTree α)) : List.map RootCutList.erase (rootCutsList ts) = PTree.rootCutsList (List.map erase ts)

Labelled root-preserving cut lists erase to the corresponding unlabelled cut lists.

theorem HopfAlgebras.PLTree.rootCuts_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).rootCuts = List.map (RootCut.map f) t.rootCuts

Root-preserving cuts commute with relabelling.

theorem HopfAlgebras.PLTree.childCuts_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).childCuts = List.map (ChildCut.map f) t.childCuts

Child cut choices commute with relabelling.

theorem HopfAlgebras.PLTree.rootCutsList_map {α : Type u} {β : Type v} (f : α → β) (ts : List (PLTree α)) : rootCutsList (List.map (map f) ts) = List.map (RootCutList.map f) (rootCutsList ts)

Root-preserving cut lists commute with relabelling.

theorem HopfAlgebras.PLTree.rootCuts_constLabel {α : Type u} (a : α) (t : PTree) : (constLabel a t).rootCuts = List.map (RootCut.constLabel a) t.rootCuts

Root-preserving cuts of a constantly labelled tree are constantly labelled cuts.

theorem HopfAlgebras.PLTree.childCuts_constLabel {α : Type u} (a : α) (t : PTree) : (constLabel a t).childCuts = List.map (ChildCut.constLabel a) t.childCuts

Child cuts of a constantly labelled tree are constantly labelled cuts.

theorem HopfAlgebras.PLTree.rootCutsList_constLabel {α : Type u} (a : α) (ts : List PTree) : rootCutsList (List.map (constLabel a) ts) = List.map (RootCutList.constLabel a) (PTree.rootCutsList ts)

Root-preserving cut lists of constantly labelled trees are constantly labelled cut lists.

theorem HopfAlgebras.PLTree.rootCuts_node_listRelPerm_of_rootCutsList {α : Type u} {a : α} {ts us : List (PLTree α)} (h : PTree.ListRelPerm RootCutList.Perm (rootCutsList ts) (rootCutsList us)) : PTree.ListRelPerm RootCut.Perm (node a ts).rootCuts (node a us).rootCuts

theorem HopfAlgebras.PLTree.childCuts_listRelPerm_of_perm {α : Type u} {t u : PLTree α} (htu : t.Perm u) (hroot : PTree.ListRelPerm RootCut.Perm t.rootCuts u.rootCuts) : PTree.ListRelPerm ChildCut.Perm t.childCuts u.childCuts

theorem HopfAlgebras.PLTree.rootCutsList_cons_listRelPerm {α : Type u} {t u : PLTree α} {ts us : List (PLTree α)} (hchild : PTree.ListRelPerm ChildCut.Perm t.childCuts u.childCuts) (htail : PTree.ListRelPerm RootCutList.Perm (rootCutsList ts) (rootCutsList us)) : PTree.ListRelPerm RootCutList.Perm (rootCutsList (t :: ts)) (rootCutsList (u :: us))

theorem HopfAlgebras.PLTree.rootCutsList_cons_cons_listRelPerm_swap {α : Type u} (t u : PLTree α) (ts : List (PLTree α)) : PTree.ListRelPerm RootCutList.Perm (rootCutsList (t :: u :: ts)) (rootCutsList (u :: t :: ts))

theorem HopfAlgebras.PLTree.rootCutsList_listRelPerm_of_perm {α : Type u} {ts us : List (PLTree α)} (h : ts.Perm us) : PTree.ListRelPerm RootCutList.Perm (rootCutsList ts) (rootCutsList us)

theorem HopfAlgebras.PLTree.rootCutsList_listRelPerm_of_forall₂_childCuts {α : Type u} {ts us : List (PLTree α)} : List.Forall₂ (fun (t u : PLTree α) => PTree.ListRelPerm ChildCut.Perm t.childCuts u.childCuts) ts us → PTree.ListRelPerm RootCutList.Perm (rootCutsList ts) (rootCutsList us)

theorem HopfAlgebras.PLTree.rootCutsList_listRelPerm_of_forall₂_perm_rootCuts {α : Type u} {ts us : List (PLTree α)} : List.Forall₂ (fun (t u : PLTree α) => t.Perm u ∧ PTree.ListRelPerm RootCut.Perm t.rootCuts u.rootCuts) ts us → PTree.ListRelPerm RootCutList.Perm (rootCutsList ts) (rootCutsList us)

theorem HopfAlgebras.PLTree.rootCuts_node_listRelPerm_of_forall₂_perm_rootCuts {α : Type u} {a : α} {ts us : List (PLTree α)} (h : List.Forall₂ (fun (t u : PLTree α) => t.Perm u ∧ PTree.ListRelPerm RootCut.Perm t.rootCuts u.rootCuts) ts us) : PTree.ListRelPerm RootCut.Perm (node a ts).rootCuts (node a us).rootCuts

theorem HopfAlgebras.PLTree.rootCuts_listRelPerm_of_perm {α : Type u} {t u : PLTree α} : t.Perm u → PTree.ListRelPerm RootCut.Perm t.rootCuts u.rootCuts

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

theorem HopfAlgebras.PLTree.rootCuts_noPrunedTrunks {α : Type u} (t : PLTree α) : List.filterMap RootCut.noPrunedTrunk? t.rootCuts = [t]

Exactly one root-preserving labelled cut of a tree prunes no trees: the no-cut cut.

theorem HopfAlgebras.PLTree.childCuts_noPrunedTrunks {α : Type u} (t : PLTree α) : List.filterMap ChildCut.noPrunedTrunk? t.childCuts = [t]

Exactly one labelled child cut choice prunes no trees: the choice keeping the whole child.

theorem HopfAlgebras.PLTree.rootCutsList_noPrunedTrunks {α : Type u} (ts : List (PLTree α)) : List.filterMap RootCutList.noPrunedTrunks? (rootCutsList ts) = [ts]

Exactly one root-preserving labelled cut list prunes no trees: the no-cut list.

theorem HopfAlgebras.PLTree.rootCuts_order {α : Type u} {t : PLTree α} {c : RootCut α} : c ∈ t.rootCuts → orderList c.pruned + c.trunk.order = t.order

Root-preserving labelled cuts conserve the order of a tree.

theorem HopfAlgebras.PLTree.childCuts_order {α : Type u} {t : PLTree α} {c : ChildCut α} : c ∈ t.childCuts → (orderList c.pruned + match c.trunk? with | none => 0 | some trunk => trunk.order) = t.order

Labelled child cut choices conserve the order of the child tree.

theorem HopfAlgebras.PLTree.rootCutsList_order {α : Type u} {ts : List (PLTree α)} {c : RootCutList α} : c ∈ rootCutsList ts → orderList c.pruned + orderList c.trunks = orderList ts

Combined labelled child cuts conserve the total order of a list of children.

theorem HopfAlgebras.PLTree.rootCuts_pruned_eq_nil {α : Type u} {t : PLTree α} {c : RootCut α} : c ∈ t.rootCuts → c.pruned = [] → c.trunk = t

A labelled root-preserving cut with no pruned trees is the no-cut root cut.

theorem HopfAlgebras.PLTree.childCuts_pruned_eq_nil {α : Type u} {t : PLTree α} {c : ChildCut α} : c ∈ t.childCuts → c.pruned = [] → c.trunk? = some t

A labelled child cut choice with no pruned trees keeps the whole child tree.

theorem HopfAlgebras.PLTree.rootCutsList_pruned_eq_nil {α : Type u} {ts : List (PLTree α)} {c : RootCutList α} : c ∈ rootCutsList ts → c.pruned = [] → c.trunks = ts

A labelled root-preserving cut list with no pruned trees keeps every child tree.

def HopfAlgebras.PLTree.cuts {α : Type u} (t : PLTree α) : List (Cut α)

All labelled admissible cuts, including the full cut.

Equations

• t.cuts = List.map (fun (c : HopfAlgebras.PLTree.RootCut α) => { pruned := c.pruned, trunk? := some c.trunk }) t.rootCuts ++ [{ pruned := [t], trunk? := none }]

theorem HopfAlgebras.PLTree.cuts_listRelPerm_of_rootCuts {α : Type u} {t u : PLTree α} (htu : t.Perm u) (hroot : PTree.ListRelPerm RootCut.Perm t.rootCuts u.rootCuts) : PTree.ListRelPerm Cut.Perm t.cuts u.cuts

theorem HopfAlgebras.PLTree.cuts_listRelPerm_of_perm {α : Type u} {t u : PLTree α} (h : t.Perm u) : PTree.ListRelPerm Cut.Perm t.cuts u.cuts

theorem HopfAlgebras.PLTree.cuts_erase {α : Type u} (t : PLTree α) : List.map Cut.erase t.cuts = t.erase.cuts

Labelled admissible cuts erase to the corresponding unlabelled cuts.

theorem HopfAlgebras.PLTree.cuts_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).cuts = List.map (Cut.map f) t.cuts

theorem HopfAlgebras.PLTree.cuts_constLabel {α : Type u} (a : α) (t : PTree) : (constLabel a t).cuts = List.map (Cut.constLabel a) t.cuts

def HopfAlgebras.PLTree.Cut.prunedForest {α : Type u} (c : Cut α) : LRootedForest α

The pruned branches of a labelled cut, as a non-planar labelled rooted forest.

Equations

• c.prunedForest = ↑(List.map HopfAlgebras.LRootedTree.ofPLTree c.pruned)

def HopfAlgebras.PLTree.Cut.trunkForest {α : Type u} (c : Cut α) : LRootedForest α

The trunk of a labelled cut. The full cut has empty trunk forest.

Equations

• c.trunkForest = match c.trunk? with | none => 0 | some t => HopfAlgebras.LRootedForest.singleton (HopfAlgebras.LRootedTree.ofPLTree t)

@[simp]

theorem HopfAlgebras.PLTree.Cut.map_prunedForest {α : Type u} {β : Type v} (f : α → β) (c : Cut α) : LRootedForest.mapLabels f c.prunedForest = (map f c).prunedForest

@[simp]

theorem HopfAlgebras.PLTree.Cut.map_trunkForest {α : Type u} {β : Type v} (f : α → β) (c : Cut α) : LRootedForest.mapLabels f c.trunkForest = (map f c).trunkForest

theorem HopfAlgebras.PLTree.Cut.Perm.prunedForest_eq {α : Type u} {c d : Cut α} (h : c.Perm d) : c.prunedForest = d.prunedForest

theorem HopfAlgebras.PLTree.Cut.Perm.trunkForest_eq {α : Type u} {c d : Cut α} (h : c.Perm d) : c.trunkForest = d.trunkForest

theorem HopfAlgebras.PLTree.Cut.Perm.coproductTerm_eq {α : Type u} {c d : Cut α} (h : c.Perm d) : (c.prunedForest, c.trunkForest) = (d.prunedForest, d.trunkForest)

@[simp]

theorem HopfAlgebras.PLTree.Cut.constLabel_prunedForest {α : Type u} (a : α) (c : PTree.Cut) : (constLabel a c).prunedForest = LRootedForest.constLabel a c.prunedForest

@[simp]

theorem HopfAlgebras.PLTree.Cut.constLabel_trunkForest {α : Type u} (a : α) (c : PTree.Cut) : (constLabel a c).trunkForest = LRootedForest.constLabel a c.trunkForest

@[simp]

theorem HopfAlgebras.PLTree.Cut.erase_prunedForest {α : Type u} (c : Cut α) : c.prunedForest.erase = c.erase.prunedForest

@[simp]

theorem HopfAlgebras.PLTree.Cut.erase_trunkForest {α : Type u} (c : Cut α) : c.trunkForest.erase = c.erase.trunkForest

@[simp]

theorem HopfAlgebras.PLTree.Cut.order_trunkForest {α : Type u} (c : Cut α) : c.trunkForest.order = match c.trunk? with | none => 0 | some trunk => trunk.order

theorem HopfAlgebras.PLTree.cuts_order {α : Type u} {t : PLTree α} {c : Cut α} (hc : c ∈ t.cuts) : c.prunedForest.order + c.trunkForest.order = t.order

Every labelled admissible cut conserves total order between pruned forest and trunk.

def HopfAlgebras.PLTree.coproductTerms {α : Type u} (t : PLTree α) : List (LRootedForest α × LRootedForest α)

The terms P^c(t) ⊗ R^c(t) appearing in the labelled BCK coproduct.

Equations

• t.coproductTerms = List.map (fun (c : HopfAlgebras.PLTree.Cut α) => (c.prunedForest, c.trunkForest)) t.cuts

def HopfAlgebras.PLTree.leftBoundaryCoproductTerm? {α : Type u} (term : LRootedForest α × LRootedForest α) : Option (LRootedForest α × LRootedForest α)

Keep exactly the labelled coproduct terms whose left tensor factor is empty.

Equations

• HopfAlgebras.PLTree.leftBoundaryCoproductTerm? term = if term.1.order = 0 then some term else none

def HopfAlgebras.PLTree.rightBoundaryCoproductTerm? {α : Type u} (term : LRootedForest α × LRootedForest α) : Option (LRootedForest α × LRootedForest α)

Keep exactly the labelled coproduct terms whose right tensor factor is empty.

Equations

• HopfAlgebras.PLTree.rightBoundaryCoproductTerm? term = if term.2.order = 0 then some term else none

def HopfAlgebras.PLTree.eraseCoproductTerm {α : Type u} (term : LRootedForest α × LRootedForest α) : RootedForest × RootedForest

Forget labels in a labelled coproduct basis term.

Equations

• HopfAlgebras.PLTree.eraseCoproductTerm term = (term.1.erase, term.2.erase)

def HopfAlgebras.PLTree.mapCoproductTerm {α : Type u} {β : Type v} (f : α → β) (term : LRootedForest α × LRootedForest α) : LRootedForest β × LRootedForest β

Relabel a labelled coproduct basis term.

Equations

• HopfAlgebras.PLTree.mapCoproductTerm f term = (HopfAlgebras.LRootedForest.mapLabels f term.1, HopfAlgebras.LRootedForest.mapLabels f term.2)

def HopfAlgebras.PLTree.constLabelCoproductTerm {α : Type u} (a : α) (term : RootedForest × RootedForest) : LRootedForest α × LRootedForest α

Label every vertex in an unlabelled coproduct basis term by the same label.

Equations

• HopfAlgebras.PLTree.constLabelCoproductTerm a term = (HopfAlgebras.LRootedForest.constLabel a term.1, HopfAlgebras.LRootedForest.constLabel a term.2)

@[simp]

theorem HopfAlgebras.PLTree.eraseCoproductTerm_constLabel {α : Type u} (a : α) (term : RootedForest × RootedForest) : eraseCoproductTerm (constLabelCoproductTerm a term) = term

@[simp]

theorem HopfAlgebras.PLTree.mapCoproductTerm_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (term : RootedForest × RootedForest) : mapCoproductTerm f (constLabelCoproductTerm a term) = constLabelCoproductTerm (f a) term

@[simp]

theorem HopfAlgebras.PLTree.mapCoproductTerm_add {α : Type u} {β : Type v} (f : α → β) (x y : LRootedForest α × LRootedForest α) : mapCoproductTerm f (x + y) = mapCoproductTerm f x + mapCoproductTerm f y

@[simp]

theorem HopfAlgebras.PLTree.constLabelCoproductTerm_add {α : Type u} (a : α) (x y : RootedForest × RootedForest) : constLabelCoproductTerm a (x + y) = constLabelCoproductTerm a x + constLabelCoproductTerm a y

def HopfAlgebras.PLTree.eraseTripleCoproductTerm {α : Type u} (term : LRootedForest α × LRootedForest α × LRootedForest α) : RootedForest × RootedForest × RootedForest

Forget labels in a labelled triple coproduct term.

Equations

• HopfAlgebras.PLTree.eraseTripleCoproductTerm term = (term.1.erase, term.2.1.erase, term.2.2.erase)

def HopfAlgebras.PLTree.mapTripleCoproductTerm {α : Type u} {β : Type v} (f : α → β) (term : LRootedForest α × LRootedForest α × LRootedForest α) : LRootedForest β × LRootedForest β × LRootedForest β

Relabel a labelled triple coproduct term.

Equations

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

def HopfAlgebras.PLTree.constLabelTripleCoproductTerm {α : Type u} (a : α) (term : RootedForest × RootedForest × RootedForest) : LRootedForest α × LRootedForest α × LRootedForest α

Label every vertex in an unlabelled triple coproduct term by the same label.

Equations

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

@[simp]

theorem HopfAlgebras.PLTree.eraseTripleCoproductTerm_constLabel {α : Type u} (a : α) (term : RootedForest × RootedForest × RootedForest) : eraseTripleCoproductTerm (constLabelTripleCoproductTerm a term) = term

@[simp]

theorem HopfAlgebras.PLTree.mapTripleCoproductTerm_constLabel {α : Type u} {β : Type v} (f : α → β) (a : α) (term : RootedForest × RootedForest × RootedForest) : mapTripleCoproductTerm f (constLabelTripleCoproductTerm a term) = constLabelTripleCoproductTerm (f a) term

theorem HopfAlgebras.PLTree.coproductTerms_erase {α : Type u} (t : PLTree α) : List.map eraseCoproductTerm t.coproductTerms = t.erase.coproductTerms

Labelled tree coproduct terms erase to the corresponding unlabelled terms.

theorem HopfAlgebras.PLTree.coproductTerms_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).coproductTerms = List.map (mapCoproductTerm f) t.coproductTerms

theorem HopfAlgebras.PLTree.coproductTerms_constLabel {α : Type u} (a : α) (t : PTree) : (constLabel a t).coproductTerms = List.map (constLabelCoproductTerm a) t.coproductTerms

theorem HopfAlgebras.PLTree.coproductTerms_order {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ t.coproductTerms) : term.1.order + term.2.order = t.order

Every labelled coproduct term conserves total order between tensor factors.

theorem HopfAlgebras.PLTree.coproductTerms_left_eq_zero {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ t.coproductTerms) (hleft : term.1 = 0) : term.2 = LRootedForest.singleton (LRootedTree.ofPLTree t)

The only labelled tree coproduct term with empty left factor is 1 ⊗ t.

theorem HopfAlgebras.PLTree.coproductTerms_right_eq_zero {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ t.coproductTerms) (hright : term.2 = 0) : term.1 = LRootedForest.singleton (LRootedTree.ofPLTree t)

The only labelled tree coproduct term with empty right factor is t ⊗ 1.

theorem HopfAlgebras.PLTree.coproductTerms_leftBoundaryCoproductTerm {α : Type u} (t : PLTree α) : List.filterMap leftBoundaryCoproductTerm? t.coproductTerms = [(0, LRootedForest.singleton (LRootedTree.ofPLTree t))]

A labelled tree coproduct has exactly one term with empty left factor.

theorem HopfAlgebras.PLTree.coproductTerms_rightBoundaryCoproductTerm {α : Type u} (t : PLTree α) : List.filterMap rightBoundaryCoproductTerm? t.coproductTerms = [(LRootedForest.singleton (LRootedTree.ofPLTree t), 0)]

A labelled tree coproduct has exactly one term with empty right factor.

theorem HopfAlgebras.PLTree.coproductTerms_perm_of_cuts_listRelPerm {α : Type u} {t u : PLTree α} (h : PTree.ListRelPerm Cut.Perm t.cuts u.cuts) : t.coproductTerms.Perm u.coproductTerms

theorem HopfAlgebras.PLTree.coproductTerms_perm {α : Type u} {t u : PLTree α} (h : t.Perm u) : t.coproductTerms.Perm u.coproductTerms

theorem HopfAlgebras.PLTree.childCuts_coproductTerms_perm {α : Type u} (t : PLTree α) : (List.map ChildCut.coproductTerm t.childCuts).Perm t.coproductTerms

def HopfAlgebras.PLTree.properCoproductTerms {α : Type u} (t : PLTree α) : List (LRootedForest α × LRootedForest α)

The proper labelled BCK coproduct terms, excluding the two counit terms.

Equations

• t.properCoproductTerms = List.filter (fun (term : HopfAlgebras.LRootedForest α × HopfAlgebras.LRootedForest α) => decide (0 < term.1.order ∧ 0 < term.2.order)) t.coproductTerms

theorem HopfAlgebras.PLTree.properCoproductTerms_perm {α : Type u} {t u : PLTree α} (h : t.Perm u) : t.properCoproductTerms.Perm u.properCoproductTerms

theorem HopfAlgebras.PLTree.properCoproductTerms_erase {α : Type u} (t : PLTree α) : List.map eraseCoproductTerm t.properCoproductTerms = t.erase.properCoproductTerms

theorem HopfAlgebras.PLTree.properCoproductTerms_map {α : Type u} {β : Type v} (f : α → β) (t : PLTree α) : (map f t).properCoproductTerms = List.map (mapCoproductTerm f) t.properCoproductTerms

theorem HopfAlgebras.PLTree.properCoproductTerms_constLabel {α : Type u} (a : α) (t : PTree) : (constLabel a t).properCoproductTerms = List.map (constLabelCoproductTerm a) t.properCoproductTerms

theorem HopfAlgebras.PLTree.properCoproductTerms_mem_coproductTerms {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ t.properCoproductTerms) : term ∈ t.coproductTerms

theorem HopfAlgebras.PLTree.properCoproductTerms_order {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ t.properCoproductTerms) : term.1.order + term.2.order = t.order

theorem HopfAlgebras.PLTree.properCoproductTerms_left_order_lt {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ t.properCoproductTerms) : term.1.order < t.order

theorem HopfAlgebras.PLTree.properCoproductTerms_right_order_lt {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ t.properCoproductTerms) : term.2.order < t.order

def HopfAlgebras.PLTree.multiplyCoproductTerms {α : Type u} (xs ys : List (LRootedForest α × LRootedForest α)) : List (LRootedForest α × LRootedForest α)

Multiply two finite lists of labelled coproduct basis terms.

Equations

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

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_erase {α : Type u} (xs ys : List (LRootedForest α × LRootedForest α)) : List.map eraseCoproductTerm (multiplyCoproductTerms xs ys) = PTree.multiplyCoproductTerms (List.map eraseCoproductTerm xs) (List.map eraseCoproductTerm ys)

Multiplication of labelled coproduct terms commutes with erasing labels.

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_map {α : Type u} {β : Type v} (f : α → β) (xs ys : List (LRootedForest α × LRootedForest α)) : multiplyCoproductTerms (List.map (mapCoproductTerm f) xs) (List.map (mapCoproductTerm f) ys) = List.map (mapCoproductTerm f) (multiplyCoproductTerms xs ys)

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_constLabel {α : Type u} (a : α) (xs ys : List (RootedForest × RootedForest)) : multiplyCoproductTerms (List.map (constLabelCoproductTerm a) xs) (List.map (constLabelCoproductTerm a) ys) = List.map (constLabelCoproductTerm a) (PTree.multiplyCoproductTerms xs ys)

def HopfAlgebras.PLTree.coproductTermsList {α : Type u} : List (PLTree α) → List (LRootedForest α × LRootedForest α)

Multiplicative extension of labelled coproduct terms to planar labelled forests.

Equations

• HopfAlgebras.PLTree.coproductTermsList [] = [(0, 0)]
• HopfAlgebras.PLTree.coproductTermsList (head :: tail) = HopfAlgebras.PLTree.multiplyCoproductTerms head.coproductTerms (HopfAlgebras.PLTree.coproductTermsList tail)

theorem HopfAlgebras.PLTree.coproductTermsList_erase {α : Type u} (ts : List (PLTree α)) : List.map eraseCoproductTerm (coproductTermsList ts) = PTree.coproductTermsList (List.map erase ts)

Labelled forest coproduct terms erase to the corresponding unlabelled terms.

theorem HopfAlgebras.PLTree.coproductTermsList_map {α : Type u} {β : Type v} (f : α → β) (ts : List (PLTree α)) : coproductTermsList (List.map (map f) ts) = List.map (mapCoproductTerm f) (coproductTermsList ts)

theorem HopfAlgebras.PLTree.coproductTermsList_constLabel {α : Type u} (a : α) (ts : List PTree) : coproductTermsList (List.map (constLabel a) ts) = List.map (constLabelCoproductTerm a) (PTree.coproductTermsList ts)

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_perm_left {α : Type u} {xs ys zs : List (LRootedForest α × LRootedForest α)} (h : xs.Perm ys) : (multiplyCoproductTerms xs zs).Perm (multiplyCoproductTerms ys zs)

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_perm_right {α : Type u} {xs ys zs : List (LRootedForest α × LRootedForest α)} (h : ys.Perm zs) : (multiplyCoproductTerms xs ys).Perm (multiplyCoproductTerms xs zs)

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_perm {α : Type u} {xs xs' ys ys' : List (LRootedForest α × LRootedForest α)} (hxs : xs.Perm xs') (hys : ys.Perm ys') : (multiplyCoproductTerms xs ys).Perm (multiplyCoproductTerms xs' ys')

theorem HopfAlgebras.PLTree.coproductTermsList_perm_rootCutsList {α : Type u} (ts : List (PLTree α)) : (coproductTermsList ts).Perm (List.map RootCutList.coproductTerm (rootCutsList ts))

theorem HopfAlgebras.PLTree.coproductTerms_node_perm {α : Type u} (a : α) (ts : List (PLTree α)) : (node a ts).coproductTerms.Perm (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, LRootedForest.singleton (LRootedForest.graft a term.2))) (coproductTermsList ts) ++ [(LRootedForest.singleton (LRootedTree.ofPLTree (node a ts)), 0)])

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_comm {α : Type u} {xs ys : List (LRootedForest α × LRootedForest α)} : (multiplyCoproductTerms xs ys).Perm (multiplyCoproductTerms ys xs)

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_assoc {α : Type u} {xs ys zs : List (LRootedForest α × LRootedForest α)} : (multiplyCoproductTerms xs (multiplyCoproductTerms ys zs)).Perm (multiplyCoproductTerms (multiplyCoproductTerms xs ys) zs)

theorem HopfAlgebras.PLTree.coproductTermsList_append_perm {α : Type u} (ts us : List (PLTree α)) : (coproductTermsList (ts ++ us)).Perm (multiplyCoproductTerms (coproductTermsList ts) (coproductTermsList us))

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

theorem HopfAlgebras.PLTree.coproductTermsList_forall₂_perm {α : Type u} {ts us : List (PLTree α)} : List.Forall₂ Perm ts us → (coproductTermsList ts).Perm (coproductTermsList us)

theorem HopfAlgebras.PLTree.coproductTermsList_listRelPerm {α : Type u} {ts us : List (PLTree α)} (h : PTree.ListRelPerm Perm ts us) : (coproductTermsList ts).Perm (coproductTermsList us)

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

theorem HopfAlgebras.PLTree.multiplyCoproductTerms_order {α : Type u} {xs ys : List (LRootedForest α × LRootedForest α)} {m n : ℕ} (hxs : ∀ term ∈ xs, term.1.order + term.2.order = m) (hys : ∀ term ∈ ys, term.1.order + term.2.order = n) {term : LRootedForest α × LRootedForest α} (hterm : term ∈ multiplyCoproductTerms xs ys) : term.1.order + term.2.order = m + n

theorem HopfAlgebras.PLTree.coproductTermsList_order {α : Type u} {ts : List (PLTree α)} {term : LRootedForest α × LRootedForest α} : term ∈ coproductTermsList ts → term.1.order + term.2.order = orderList ts

Every labelled planar-forest coproduct term conserves total order.

theorem HopfAlgebras.PLTree.coproductTermsList_left_eq_zero {α : Type u} {ts : List (PLTree α)} {term : LRootedForest α × LRootedForest α} : term ∈ coproductTermsList ts → term.1 = 0 → term.2 = ↑(List.map LRootedTree.ofPLTree ts)

The only labelled planar-forest coproduct terms with empty left factor are 1 ⊗ φ.

theorem HopfAlgebras.PLTree.coproductTermsList_right_eq_zero {α : Type u} {ts : List (PLTree α)} {term : LRootedForest α × LRootedForest α} : term ∈ coproductTermsList ts → term.2 = 0 → term.1 = ↑(List.map LRootedTree.ofPLTree ts)

The only labelled planar-forest coproduct terms with empty right factor are φ ⊗ 1.

theorem HopfAlgebras.PLTree.coproductTermsList_leftBoundaryCoproductTerm {α : Type u} (ts : List (PLTree α)) : List.filterMap leftBoundaryCoproductTerm? (coproductTermsList ts) = [(0, ↑(List.map LRootedTree.ofPLTree ts))]

A labelled planar-forest coproduct has exactly one term with empty left factor.

theorem HopfAlgebras.PLTree.coproductTermsList_rightBoundaryCoproductTerm {α : Type u} (ts : List (PLTree α)) : List.filterMap rightBoundaryCoproductTerm? (coproductTermsList ts) = [(↑(List.map LRootedTree.ofPLTree ts), 0)]

A labelled planar-forest coproduct has exactly one term with empty right factor.

def HopfAlgebras.PLTree.properCoproductTermsList {α : Type u} (ts : List (PLTree α)) : List (LRootedForest α × LRootedForest α)

The proper BCK coproduct terms for a planar labelled forest.

Equations

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

theorem HopfAlgebras.PLTree.properCoproductTermsList_erase {α : Type u} (ts : List (PLTree α)) : List.map eraseCoproductTerm (properCoproductTermsList ts) = PTree.properCoproductTermsList (List.map erase ts)

theorem HopfAlgebras.PLTree.properCoproductTermsList_map {α : Type u} {β : Type v} (f : α → β) (ts : List (PLTree α)) : properCoproductTermsList (List.map (map f) ts) = List.map (mapCoproductTerm f) (properCoproductTermsList ts)

theorem HopfAlgebras.PLTree.properCoproductTermsList_constLabel {α : Type u} (a : α) (ts : List PTree) : properCoproductTermsList (List.map (constLabel a) ts) = List.map (constLabelCoproductTerm a) (PTree.properCoproductTermsList ts)

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

theorem HopfAlgebras.PLTree.properCoproductTermsList_mem_coproductTermsList {α : Type u} {ts : List (PLTree α)} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ properCoproductTermsList ts) : term ∈ coproductTermsList ts

theorem HopfAlgebras.PLTree.properCoproductTermsList_order {α : Type u} {ts : List (PLTree α)} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ properCoproductTermsList ts) : term.1.order + term.2.order = orderList ts

theorem HopfAlgebras.PLTree.properCoproductTermsList_left_order_lt {α : Type u} {ts : List (PLTree α)} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ properCoproductTermsList ts) : term.1.order < orderList ts

theorem HopfAlgebras.PLTree.properCoproductTermsList_right_order_lt {α : Type u} {ts : List (PLTree α)} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ properCoproductTermsList ts) : term.2.order < orderList ts

def HopfAlgebras.PLTree.Cut.trunkCoproductTerms {α : Type u} (c : Cut α) : List (LRootedForest α × LRootedForest α)

Coproduct terms of the trunk of a labelled cut, using [(0, 0)] for the full cut.

Equations

• c.trunkCoproductTerms = match c.trunk? with | none => [(0, 0)] | some trunk => trunk.coproductTerms

theorem HopfAlgebras.PLTree.Cut.trunkCoproductTerms_order {α : Type u} {c : Cut α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ c.trunkCoproductTerms) : term.1.order + term.2.order = c.trunkForest.order

theorem HopfAlgebras.PLTree.Cut.trunkCoproductTerms_perm {α : Type u} {c d : Cut α} (h : c.Perm d) : c.trunkCoproductTerms.Perm d.trunkCoproductTerms

theorem HopfAlgebras.PLTree.Cut.trunkCoproductTerms_erase {α : Type u} (c : Cut α) : List.map eraseCoproductTerm c.trunkCoproductTerms = c.erase.trunkCoproductTerms

def HopfAlgebras.PLTree.nestedCoproductLeftTerms {α : Type u} (t : PLTree α) : List (LRootedForest α × LRootedForest α × LRootedForest α)

Planar terms for (Δ ⊗ id)Δ(t), keeping the original labelled cut representatives.

Equations

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

def HopfAlgebras.PLTree.nestedCoproductRightTerms {α : Type u} (t : PLTree α) : List (LRootedForest α × LRootedForest α × LRootedForest α)

Planar terms for (id ⊗ Δ)Δ(t), keeping the original labelled cut representatives.

Equations

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

theorem HopfAlgebras.PLTree.nestedCoproductLeftTerms_erase {α : Type u} (t : PLTree α) : List.map eraseTripleCoproductTerm t.nestedCoproductLeftTerms = t.erase.nestedCoproductLeftTerms

theorem HopfAlgebras.PLTree.nestedCoproductRightTerms_erase {α : Type u} (t : PLTree α) : List.map eraseTripleCoproductTerm t.nestedCoproductRightTerms = t.erase.nestedCoproductRightTerms

theorem HopfAlgebras.PLTree.nestedCoproductLeftCut_forall₂_perm {α : Type u} {c d : Cut α} (hpruned : List.Forall₂ Perm c.pruned d.pruned) (htrunk : c.trunkForest = d.trunkForest) : (List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (coproductTermsList c.pruned)).Perm (List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, d.trunkForest)) (coproductTermsList d.pruned))

theorem HopfAlgebras.PLTree.nestedCoproductLeftCut_perm {α : Type u} {c d : Cut α} (h : c.Perm d) : (List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (coproductTermsList c.pruned)).Perm (List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, d.trunkForest)) (coproductTermsList d.pruned))

theorem HopfAlgebras.PLTree.nestedCoproductLeftCuts_forall₂_perm {α : Type u} {cs ds : List (Cut α)} : List.Forall₂ Cut.Perm cs ds → (List.flatMap (fun (c : Cut α) => List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (coproductTermsList c.pruned)) cs).Perm (List.flatMap (fun (d : Cut α) => List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, d.trunkForest)) (coproductTermsList d.pruned)) ds)

theorem HopfAlgebras.PLTree.nestedCoproductLeftCuts_listRelPerm {α : Type u} {cs ds : List (Cut α)} (h : PTree.ListRelPerm Cut.Perm cs ds) : (List.flatMap (fun (c : Cut α) => List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (coproductTermsList c.pruned)) cs).Perm (List.flatMap (fun (d : Cut α) => List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, d.trunkForest)) (coproductTermsList d.pruned)) ds)

theorem HopfAlgebras.PLTree.nestedCoproductLeftTerms_listRelPerm {α : Type u} {t u : PLTree α} (h : PTree.ListRelPerm Cut.Perm t.cuts u.cuts) : t.nestedCoproductLeftTerms.Perm u.nestedCoproductLeftTerms

theorem HopfAlgebras.PLTree.nestedCoproductLeftTerms_perm {α : Type u} {t u : PLTree α} (h : t.Perm u) : t.nestedCoproductLeftTerms.Perm u.nestedCoproductLeftTerms

theorem HopfAlgebras.PLTree.nestedCoproductRightCut_perm {α : Type u} {c d : Cut α} (h : c.Perm d) : (List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms).Perm (List.map (fun (right : LRootedForest α × LRootedForest α) => (d.prunedForest, right.1, right.2)) d.trunkCoproductTerms)

theorem HopfAlgebras.PLTree.nestedCoproductRightCuts_forall₂_perm {α : Type u} {cs ds : List (Cut α)} : List.Forall₂ Cut.Perm cs ds → (List.flatMap (fun (c : Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) cs).Perm (List.flatMap (fun (d : Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (d.prunedForest, right.1, right.2)) d.trunkCoproductTerms) ds)

theorem HopfAlgebras.PLTree.nestedCoproductRightCuts_listRelPerm {α : Type u} {cs ds : List (Cut α)} (h : PTree.ListRelPerm Cut.Perm cs ds) : (List.flatMap (fun (c : Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) cs).Perm (List.flatMap (fun (d : Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (d.prunedForest, right.1, right.2)) d.trunkCoproductTerms) ds)

theorem HopfAlgebras.PLTree.nestedCoproductRightTerms_listRelPerm {α : Type u} {t u : PLTree α} (h : PTree.ListRelPerm Cut.Perm t.cuts u.cuts) : t.nestedCoproductRightTerms.Perm u.nestedCoproductRightTerms

theorem HopfAlgebras.PLTree.nestedCoproductRightTerms_perm {α : Type u} {t u : PLTree α} (h : t.Perm u) : t.nestedCoproductRightTerms.Perm u.nestedCoproductRightTerms

theorem HopfAlgebras.PLTree.nestedCoproductLeftTerms_order {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α × LRootedForest α} (hterm : term ∈ t.nestedCoproductLeftTerms) : term.1.order + term.2.1.order + term.2.2.order = t.order

theorem HopfAlgebras.PLTree.nestedCoproductRightTerms_order {α : Type u} {t : PLTree α} {term : LRootedForest α × LRootedForest α × LRootedForest α} (hterm : term ∈ t.nestedCoproductRightTerms) : term.1.order + term.2.1.order + term.2.2.order = t.order

@[simp]

theorem HopfAlgebras.PLTree.rootCutsList_nil {α : Type u} : rootCutsList [] = [{ pruned := [], trunks := [] }]

@[simp]

theorem HopfAlgebras.PLTree.rootCuts_node_nil {α : Type u} (a : α) : (node a []).rootCuts = [{ pruned := [], trunk := node a [] }]