Admissible Cuts

This file defines finite admissible-cut data for planar rooted trees. The resulting terms are the combinatorial input for the BCK/Connes-Kreimer coproduct.

The definitions here are intentionally planar. Passing to non-planar trees and building the coproduct on ForestAlgebra will require quotient-invariance proofs and coefficient multiplicities.

Main definitions

• PTree.RootCut - an admissible cut which keeps the root component
• PTree.Cut - an admissible cut, allowing the full cut
• PTree.cuts - finite list of admissible cuts
• PTree.cutTerms - admissible cuts as (pruned forest, trunk index) terms
• PTree.coproductTerms - admissible cuts as forest-pair coproduct terms

References

• Alain Connes, Dirk Kreimer, Hopf Algebras, Renormalization and Noncommutative Geometry
• Loic Foissy, An introduction to Hopf algebras of trees

structure HopfAlgebras.PTree.RootCut : Type

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

• pruned : List PTree
• trunk : PTree

def HopfAlgebras.PTree.instReprRootCut.repr : RootCut → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HopfAlgebras.PTree.instReprRootCut : Repr RootCut

Equations

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

structure HopfAlgebras.PTree.ChildCut : Type

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

• pruned : List PTree
• trunk? : Option PTree

def HopfAlgebras.PTree.instReprChildCut.repr : ChildCut → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HopfAlgebras.PTree.instReprChildCut : Repr ChildCut

Equations

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

structure HopfAlgebras.PTree.RootCutList : Type

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

• pruned : List PTree
• trunks : List PTree

def HopfAlgebras.PTree.instReprRootCutList.repr : RootCutList → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HopfAlgebras.PTree.instReprRootCutList : Repr RootCutList

Equations

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

structure HopfAlgebras.PTree.Cut : Type

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

• pruned : List PTree
• trunk? : Option PTree

@[implicit_reducible]

instance HopfAlgebras.PTree.instReprCut : Repr Cut

Equations

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

def HopfAlgebras.PTree.instReprCut.repr : Cut → ℕ → Std.Format

Equations

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

def HopfAlgebras.PTree.RootCut.Perm (c d : RootCut) : Prop

Equations

• c.Perm d = (HopfAlgebras.PTree.ForestPerm c.pruned d.pruned ∧ HopfAlgebras.RootedTree.ofPTree c.trunk = HopfAlgebras.RootedTree.ofPTree d.trunk)

theorem HopfAlgebras.PTree.RootCut.Perm.refl (c : RootCut) : c.Perm c

theorem HopfAlgebras.PTree.RootCut.Perm.trans {c d e : RootCut} (hcd : c.Perm d) (hde : d.Perm e) : c.Perm e

def HopfAlgebras.PTree.RootCut.noPrunedTrunk? (c : RootCut) : Option PTree

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

Equations

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

def HopfAlgebras.PTree.OptionPerm : Option PTree → Option PTree → Prop

Equations

• HopfAlgebras.PTree.OptionPerm none none = True
• HopfAlgebras.PTree.OptionPerm (some t) (some u) = (HopfAlgebras.RootedTree.ofPTree t = HopfAlgebras.RootedTree.ofPTree u)
• HopfAlgebras.PTree.OptionPerm x✝¹ x✝ = False

theorem HopfAlgebras.PTree.OptionPerm.refl (t : Option PTree) : OptionPerm t t

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

def HopfAlgebras.PTree.ChildCut.Perm (c d : ChildCut) : Prop

Equations

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

theorem HopfAlgebras.PTree.ChildCut.Perm.refl (c : ChildCut) : c.Perm c

theorem HopfAlgebras.PTree.ChildCut.Perm.trans {c d e : ChildCut} (hcd : c.Perm d) (hde : d.Perm e) : c.Perm e

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

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

def HopfAlgebras.PTree.ChildCut.noPrunedTrunk? (c : ChildCut) : Option PTree

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

Equations

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

def HopfAlgebras.PTree.ChildCut.prunedForest (c : ChildCut) : RootedForest

The pruned forest of a child cut choice.

Equations

• c.prunedForest = ↑(List.map HopfAlgebras.RootedTree.ofPTree c.pruned)

def HopfAlgebras.PTree.ChildCut.trunkForest (c : ChildCut) : RootedForest

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

Equations

• c.trunkForest = match c.trunk? with | none => 0 | some trunk => HopfAlgebras.RootedForest.singleton (HopfAlgebras.RootedTree.ofPTree trunk)

def HopfAlgebras.PTree.ChildCut.coproductTerm (c : ChildCut) : RootedForest × RootedForest

The coproduct term encoded by a child cut choice.

Equations

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

def HopfAlgebras.PTree.RootCutList.Perm (c d : RootCutList) : Prop

Equations

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

theorem HopfAlgebras.PTree.RootCutList.Perm.refl (c : RootCutList) : c.Perm c

theorem HopfAlgebras.PTree.RootCutList.Perm.trans {c d e : RootCutList} (hcd : c.Perm d) (hde : d.Perm e) : c.Perm e

def HopfAlgebras.PTree.RootCutList.consChild (c : ChildCut) (r : RootCutList) : RootCutList

Equations

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

theorem HopfAlgebras.PTree.RootCutList.Perm.consChild {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.PTree.RootCutList.Perm.consChild_swap (c d : ChildCut) (r : RootCutList) : (RootCutList.consChild c (RootCutList.consChild d r)).Perm (RootCutList.consChild d (RootCutList.consChild c r))

theorem HopfAlgebras.PTree.RootCutList.RootCut.Perm.of_rootCutList {c d : RootCutList} (h : c.Perm d) : { pruned := c.pruned, trunk := node c.trunks }.Perm { pruned := d.pruned, trunk := node d.trunks }

theorem HopfAlgebras.PTree.RootCutList.Perm.combine {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 }

def HopfAlgebras.PTree.RootCutList.noPrunedTrunks? (c : RootCutList) : Option (List PTree)

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

Equations

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

def HopfAlgebras.PTree.RootCutList.prunedForest (c : RootCutList) : RootedForest

The pruned forest of a root-preserving cut list.

Equations

• c.prunedForest = ↑(List.map HopfAlgebras.RootedTree.ofPTree c.pruned)

def HopfAlgebras.PTree.RootCutList.trunkForest (c : RootCutList) : RootedForest

The trunk forest of a root-preserving cut list.

Equations

• c.trunkForest = ↑(List.map HopfAlgebras.RootedTree.ofPTree c.trunks)

def HopfAlgebras.PTree.RootCutList.coproductTerm (c : RootCutList) : RootedForest × RootedForest

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

Equations

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

@[simp]

theorem HopfAlgebras.PTree.RootCutList.prunedForest_consChild (c : ChildCut) (r : RootCutList) : (consChild c r).prunedForest = c.prunedForest + r.prunedForest

@[simp]

theorem HopfAlgebras.PTree.RootCutList.trunkForest_consChild (c : ChildCut) (r : RootCutList) : (consChild c r).trunkForest = c.trunkForest + r.trunkForest

@[simp]

theorem HopfAlgebras.PTree.RootCutList.coproductTerm_consChild (c : ChildCut) (r : RootCutList) : (consChild c r).coproductTerm = c.coproductTerm + r.coproductTerm

theorem HopfAlgebras.PTree.rootCut_perm_of_rootCutList_perm {c d : RootCutList} (h : c.Perm d) : { pruned := c.pruned, trunk := node c.trunks }.Perm { pruned := d.pruned, trunk := node d.trunks }

def HopfAlgebras.PTree.Cut.Perm (c d : Cut) : Prop

Equations

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

theorem HopfAlgebras.PTree.Cut.Perm.refl (c : Cut) : c.Perm c

theorem HopfAlgebras.PTree.Cut.Perm.trans {c d e : Cut} (hcd : c.Perm d) (hde : d.Perm e) : c.Perm e

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

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

theorem HopfAlgebras.PTree.ListRelPerm.of_forestPerm {ts us : List PTree} (h : ForestPerm ts us) : ListRelPerm Perm ts us

@[irreducible]

def HopfAlgebras.PTree.rootCuts : PTree → List RootCut

Admissible cuts which keep the root component.

Equations

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

@[irreducible]

def HopfAlgebras.PTree.childCuts (t : PTree) : List ChildCut

Choices for a 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.PTree.RootCut) => { pruned := c.pruned, trunk? := some c.trunk }) t.rootCuts

@[irreducible]

def HopfAlgebras.PTree.rootCutsList : List PTree → List RootCutList

Combine child cut choices into root-preserving cuts.

Equations

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

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

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

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

theorem HopfAlgebras.PTree.rootCutsList_cons_cons_listRelPerm_swap (t u : PTree) (ts : List PTree) : ListRelPerm RootCutList.Perm (rootCutsList (t :: u :: ts)) (rootCutsList (u :: t :: ts))

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

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

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

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

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

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

theorem HopfAlgebras.PTree.rootCuts_pruned_eq_nil {t : PTree} {c : RootCut} : c ∈ t.rootCuts → c.pruned = [] → c.trunk = t

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

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

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

theorem HopfAlgebras.PTree.rootCutsList_pruned_eq_nil {ts : List PTree} {c : RootCutList} : c ∈ rootCutsList ts → c.pruned = [] → c.trunks = ts

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

theorem HopfAlgebras.PTree.rootCuts_noPrunedTrunks (t : PTree) : List.filterMap RootCut.noPrunedTrunk? t.rootCuts = [t]

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

theorem HopfAlgebras.PTree.childCuts_noPrunedTrunks (t : PTree) : List.filterMap ChildCut.noPrunedTrunk? t.childCuts = [t]

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

theorem HopfAlgebras.PTree.rootCutsList_noPrunedTrunks (ts : List PTree) : List.filterMap RootCutList.noPrunedTrunks? (rootCutsList ts) = [ts]

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

theorem HopfAlgebras.PTree.rootCuts_order {t : PTree} {c : RootCut} : c ∈ t.rootCuts → orderList c.pruned + c.trunk.order = t.order

Root-preserving cuts conserve the order of a tree.

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

Child cut choices conserve the order of the child tree.

theorem HopfAlgebras.PTree.rootCutsList_order {ts : List PTree} {c : RootCutList} : c ∈ rootCutsList ts → orderList c.pruned + orderList c.trunks = orderList ts

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

def HopfAlgebras.PTree.cuts (t : PTree) : List Cut

All admissible cuts, including the full cut.

Equations

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

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

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

def HopfAlgebras.PTree.Cut.prunedForest (c : Cut) : RootedForest

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

Equations

• c.prunedForest = ↑(List.map HopfAlgebras.RootedTree.ofPTree c.pruned)

def HopfAlgebras.PTree.Cut.trunkIndex (c : Cut) : TreeIndex

The trunk of a cut, using the adjoined empty tree for the full cut.

Equations

• c.trunkIndex = match c.trunk? with | none => HopfAlgebras.TreeIndex.empty | some t => HopfAlgebras.TreeIndex.tree (HopfAlgebras.RootedTree.ofPTree t)

def HopfAlgebras.PTree.Cut.trunkForest (c : Cut) : RootedForest

The trunk of a cut, as a rooted forest. The full cut has empty trunk forest.

Equations

• c.trunkForest = match c.trunk? with | none => 0 | some t => HopfAlgebras.RootedForest.singleton (HopfAlgebras.RootedTree.ofPTree t)

theorem HopfAlgebras.PTree.Cut.Perm.prunedForest_eq {c d : Cut} (h : c.Perm d) : c.prunedForest = d.prunedForest

theorem HopfAlgebras.PTree.Cut.Perm.trunkForest_eq {c d : Cut} (h : c.Perm d) : c.trunkForest = d.trunkForest

theorem HopfAlgebras.PTree.Cut.Perm.coproductTerm_eq {c d : Cut} (h : c.Perm d) : (c.prunedForest, c.trunkForest) = (d.prunedForest, d.trunkForest)

@[simp]

theorem HopfAlgebras.PTree.Cut.order_trunkForest (c : Cut) : c.trunkForest.order = c.trunkIndex.order

theorem HopfAlgebras.PTree.cuts_order {t : PTree} {c : Cut} (hc : c ∈ t.cuts) : c.prunedForest.order + c.trunkIndex.order = t.order

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

def HopfAlgebras.PTree.cutTerms (t : PTree) : List (RootedForest × TreeIndex)

The terms (P^c(t), R^c(t)) appearing in the BCK coproduct of a planar tree.

Equations

• t.cutTerms = List.map (fun (c : HopfAlgebras.PTree.Cut) => (c.prunedForest, c.trunkIndex)) t.cuts

def HopfAlgebras.PTree.coproductTerms (t : PTree) : List (RootedForest × RootedForest)

The terms P^c(t) ⊗ R^c(t) appearing in the BCK coproduct of a planar tree.

Equations

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

def HopfAlgebras.PTree.leftBoundaryCoproductTerm? (term : RootedForest × RootedForest) : Option (RootedForest × RootedForest)

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

Equations

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

def HopfAlgebras.PTree.rightBoundaryCoproductTerm? (term : RootedForest × RootedForest) : Option (RootedForest × RootedForest)

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

Equations

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

theorem HopfAlgebras.PTree.cutTerms_order {t : PTree} {term : RootedForest × TreeIndex} (hterm : term ∈ t.cutTerms) : term.1.order + term.2.order = t.order

Every cut term conserves total order between the pruned forest and trunk.

theorem HopfAlgebras.PTree.coproductTerms_order {t : PTree} {term : RootedForest × RootedForest} (hterm : term ∈ t.coproductTerms) : term.1.order + term.2.order = t.order

Every coproduct term conserves total order between the two tensor factors.

theorem HopfAlgebras.PTree.coproductTerms_left_eq_zero {t : PTree} {term : RootedForest × RootedForest} (hterm : term ∈ t.coproductTerms) (hleft : term.1 = 0) : term.2 = RootedForest.singleton (RootedTree.ofPTree t)

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

theorem HopfAlgebras.PTree.coproductTerms_right_eq_zero {t : PTree} {term : RootedForest × RootedForest} (hterm : term ∈ t.coproductTerms) (hright : term.2 = 0) : term.1 = RootedForest.singleton (RootedTree.ofPTree t)

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

theorem HopfAlgebras.PTree.coproductTerms_leftBoundaryCoproductTerm (t : PTree) : List.filterMap leftBoundaryCoproductTerm? t.coproductTerms = [(0, RootedForest.singleton (RootedTree.ofPTree t))]

A tree coproduct has exactly one term with empty left factor, namely 1 ⊗ t.

theorem HopfAlgebras.PTree.coproductTerms_rightBoundaryCoproductTerm (t : PTree) : List.filterMap rightBoundaryCoproductTerm? t.coproductTerms = [(RootedForest.singleton (RootedTree.ofPTree t), 0)]

A tree coproduct has exactly one term with empty right factor, namely t ⊗ 1.

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

theorem HopfAlgebras.PTree.coproductTerms_perm {t u : PTree} (h : t.Perm u) : t.coproductTerms.Perm u.coproductTerms

theorem HopfAlgebras.PTree.childCuts_coproductTerms_perm (t : PTree) : (List.map ChildCut.coproductTerm t.childCuts).Perm t.coproductTerms

def HopfAlgebras.PTree.properCoproductTerms (t : PTree) : List (RootedForest × RootedForest)

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

Equations

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

theorem HopfAlgebras.PTree.properCoproductTerms_perm {t u : PTree} (h : t.Perm u) : t.properCoproductTerms.Perm u.properCoproductTerms

theorem HopfAlgebras.PTree.properCoproductTerms_mem_coproductTerms {t : PTree} {term : RootedForest × RootedForest} (hterm : term ∈ t.properCoproductTerms) : term ∈ t.coproductTerms

theorem HopfAlgebras.PTree.properCoproductTerms_order {t : PTree} {term : RootedForest × RootedForest} (hterm : term ∈ t.properCoproductTerms) : term.1.order + term.2.order = t.order

theorem HopfAlgebras.PTree.properCoproductTerms_left_order_lt {t : PTree} {term : RootedForest × RootedForest} (hterm : term ∈ t.properCoproductTerms) : term.1.order < t.order

theorem HopfAlgebras.PTree.properCoproductTerms_right_order_lt {t : PTree} {term : RootedForest × RootedForest} (hterm : term ∈ t.properCoproductTerms) : term.2.order < t.order

def HopfAlgebras.PTree.multiplyCoproductTerms (xs ys : List (RootedForest × RootedForest)) : List (RootedForest × RootedForest)

Multiply two finite lists of coproduct basis terms.

Equations

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

def HopfAlgebras.PTree.coproductTermsList : List PTree → List (RootedForest × RootedForest)

Multiplicative extension of coproduct terms to planar forests.

Equations

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

theorem HopfAlgebras.PTree.multiplyCoproductTerms_perm_left {xs ys zs : List (RootedForest × RootedForest)} (h : xs.Perm ys) : (multiplyCoproductTerms xs zs).Perm (multiplyCoproductTerms ys zs)

theorem HopfAlgebras.PTree.multiplyCoproductTerms_perm_right {xs ys zs : List (RootedForest × RootedForest)} (h : ys.Perm zs) : (multiplyCoproductTerms xs ys).Perm (multiplyCoproductTerms xs zs)

theorem HopfAlgebras.PTree.multiplyCoproductTerms_perm {xs xs' ys ys' : List (RootedForest × RootedForest)} (hxs : xs.Perm xs') (hys : ys.Perm ys') : (multiplyCoproductTerms xs ys).Perm (multiplyCoproductTerms xs' ys')

theorem HopfAlgebras.PTree.coproductTermsList_perm_rootCutsList (ts : List PTree) : (coproductTermsList ts).Perm (List.map RootCutList.coproductTerm (rootCutsList ts))

theorem HopfAlgebras.PTree.coproductTerms_node_perm (ts : List PTree) : (node ts).coproductTerms.Perm (List.map (fun (term : RootedForest × RootedForest) => (term.1, RootedForest.singleton term.2.graft)) (coproductTermsList ts) ++ [(RootedForest.singleton (RootedTree.ofPTree (node ts)), 0)])

theorem HopfAlgebras.PTree.multiplyCoproductTerms_comm {xs ys : List (RootedForest × RootedForest)} : (multiplyCoproductTerms xs ys).Perm (multiplyCoproductTerms ys xs)

theorem HopfAlgebras.PTree.multiplyCoproductTerms_assoc {xs ys zs : List (RootedForest × RootedForest)} : (multiplyCoproductTerms xs (multiplyCoproductTerms ys zs)).Perm (multiplyCoproductTerms (multiplyCoproductTerms xs ys) zs)

theorem HopfAlgebras.PTree.coproductTermsList_append_perm (ts us : List PTree) : (coproductTermsList (ts ++ us)).Perm (multiplyCoproductTerms (coproductTermsList ts) (coproductTermsList us))

theorem HopfAlgebras.PTree.coproductTermsList_perm_of_list_perm {ts us : List PTree} (h : ts.Perm us) : (coproductTermsList ts).Perm (coproductTermsList us)

theorem HopfAlgebras.PTree.coproductTermsList_forall₂_perm {ts us : List PTree} : List.Forall₂ Perm ts us → (coproductTermsList ts).Perm (coproductTermsList us)

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

theorem HopfAlgebras.PTree.coproductTermsList_forestPerm {ts us : List PTree} (h : ForestPerm ts us) : (coproductTermsList ts).Perm (coproductTermsList us)

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

theorem HopfAlgebras.PTree.coproductTermsList_order {ts : List PTree} {term : RootedForest × RootedForest} : term ∈ coproductTermsList ts → term.1.order + term.2.order = orderList ts

Every planar-forest coproduct term conserves total order.

theorem HopfAlgebras.PTree.coproductTermsList_left_eq_zero {ts : List PTree} {term : RootedForest × RootedForest} : term ∈ coproductTermsList ts → term.1 = 0 → term.2 = ↑(List.map RootedTree.ofPTree ts)

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

theorem HopfAlgebras.PTree.coproductTermsList_right_eq_zero {ts : List PTree} {term : RootedForest × RootedForest} : term ∈ coproductTermsList ts → term.2 = 0 → term.1 = ↑(List.map RootedTree.ofPTree ts)

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

theorem HopfAlgebras.PTree.coproductTermsList_leftBoundaryCoproductTerm (ts : List PTree) : List.filterMap leftBoundaryCoproductTerm? (coproductTermsList ts) = [(0, ↑(List.map RootedTree.ofPTree ts))]

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

theorem HopfAlgebras.PTree.coproductTermsList_rightBoundaryCoproductTerm (ts : List PTree) : List.filterMap rightBoundaryCoproductTerm? (coproductTermsList ts) = [(↑(List.map RootedTree.ofPTree ts), 0)]

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

def HopfAlgebras.PTree.properCoproductTermsList (ts : List PTree) : List (RootedForest × RootedForest)

The proper BCK coproduct terms for a planar forest.

Equations

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

theorem HopfAlgebras.PTree.properCoproductTermsList_forall₂_perm {ts us : List PTree} (h : List.Forall₂ Perm ts us) : (properCoproductTermsList ts).Perm (properCoproductTermsList us)

theorem HopfAlgebras.PTree.properCoproductTermsList_mem_coproductTermsList {ts : List PTree} {term : RootedForest × RootedForest} (hterm : term ∈ properCoproductTermsList ts) : term ∈ coproductTermsList ts

theorem HopfAlgebras.PTree.properCoproductTermsList_order {ts : List PTree} {term : RootedForest × RootedForest} (hterm : term ∈ properCoproductTermsList ts) : term.1.order + term.2.order = orderList ts

theorem HopfAlgebras.PTree.properCoproductTermsList_left_order_lt {ts : List PTree} {term : RootedForest × RootedForest} (hterm : term ∈ properCoproductTermsList ts) : term.1.order < orderList ts

theorem HopfAlgebras.PTree.properCoproductTermsList_right_order_lt {ts : List PTree} {term : RootedForest × RootedForest} (hterm : term ∈ properCoproductTermsList ts) : term.2.order < orderList ts

def HopfAlgebras.PTree.Cut.trunkCoproductTerms (c : Cut) : List (RootedForest × RootedForest)

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

Equations

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

theorem HopfAlgebras.PTree.Cut.trunkCoproductTerms_order {c : Cut} {term : RootedForest × RootedForest} (hterm : term ∈ c.trunkCoproductTerms) : term.1.order + term.2.order = c.trunkForest.order

theorem HopfAlgebras.PTree.Cut.trunkCoproductTerms_perm {c d : Cut} (h : c.Perm d) : c.trunkCoproductTerms.Perm d.trunkCoproductTerms

def HopfAlgebras.PTree.nestedCoproductLeftTerms (t : PTree) : List (RootedForest × RootedForest × RootedForest)

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

Equations

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

def HopfAlgebras.PTree.nestedCoproductRightTerms (t : PTree) : List (RootedForest × RootedForest × RootedForest)

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

Equations

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

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

theorem HopfAlgebras.PTree.nestedCoproductLeftCut_perm {c d : Cut} (h : c.Perm d) : (List.map (fun (left : RootedForest × RootedForest) => (left.1, left.2, c.trunkForest)) (coproductTermsList c.pruned)).Perm (List.map (fun (left : RootedForest × RootedForest) => (left.1, left.2, d.trunkForest)) (coproductTermsList d.pruned))

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

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

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

theorem HopfAlgebras.PTree.nestedCoproductLeftTerms_perm {t u : PTree} (h : t.Perm u) : t.nestedCoproductLeftTerms.Perm u.nestedCoproductLeftTerms

theorem HopfAlgebras.PTree.nestedCoproductRightCut_perm {c d : Cut} (h : c.Perm d) : (List.map (fun (right : RootedForest × RootedForest) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms).Perm (List.map (fun (right : RootedForest × RootedForest) => (d.prunedForest, right.1, right.2)) d.trunkCoproductTerms)

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

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

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

theorem HopfAlgebras.PTree.nestedCoproductRightTerms_perm {t u : PTree} (h : t.Perm u) : t.nestedCoproductRightTerms.Perm u.nestedCoproductRightTerms

theorem HopfAlgebras.PTree.nestedCoproductLeftTerms_order {t : PTree} {term : RootedForest × RootedForest × RootedForest} (hterm : term ∈ t.nestedCoproductLeftTerms) : term.1.order + term.2.1.order + term.2.2.order = t.order

theorem HopfAlgebras.PTree.nestedCoproductRightTerms_order {t : PTree} {term : RootedForest × RootedForest × RootedForest} (hterm : term ∈ t.nestedCoproductRightTerms) : term.1.order + term.2.1.order + term.2.2.order = t.order

@[simp]

theorem HopfAlgebras.PTree.rootCutsList_nil : rootCutsList [] = [{ pruned := [], trunks := [] }]

@[simp]

theorem HopfAlgebras.PTree.rootCuts_bullet : bullet.rootCuts = [{ pruned := [], trunk := bullet }]