Labelled Coproduct Terms in the Forest Algebra

This file turns the finite labelled cut-term lists from HopfAlgebras.Cuts.Labelled into elements of the monoid algebra on pairs of labelled rooted forests. A pair (φ, ψ) represents the basis tensor φ ⊗ ψ.

Planar labelled cut terms are extended to non-planar labelled forests through the forest quotient.

@[reducible, inline]

abbrev HopfAlgebras.LForestTensorAlgebra (α : Type u) (R : Type v) [Semiring R] : Type (max u v)

Tensor-coded labelled forest algebra: (φ, ψ) represents the basis tensor φ ⊗ ψ.

Equations

• HopfAlgebras.LForestTensorAlgebra α R = AddMonoidAlgebra R (HopfAlgebras.LRootedForest α × HopfAlgebras.LRootedForest α)

noncomputable def HopfAlgebras.LForestTensorAlgebra.ofPair {α : Type u} {R : Type v} [Semiring R] (term : LRootedForest α × LRootedForest α) : LForestTensorAlgebra α R

The basis tensor represented by a pair of labelled rooted forests.

Equations

• HopfAlgebras.LForestTensorAlgebra.ofPair term = AddMonoidAlgebra.single term 1

noncomputable def HopfAlgebras.LForestTensorAlgebra.ofForests {α : Type u} {R : Type v} [Semiring R] (φ ψ : LRootedForest α) : LForestTensorAlgebra α R

The basis tensor φ ⊗ ψ.

Equations

• HopfAlgebras.LForestTensorAlgebra.ofForests φ ψ = HopfAlgebras.LForestTensorAlgebra.ofPair (φ, ψ)

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.ofPair_zero {α : Type u} {R : Type v} [Semiring R] : ofPair 0 = 1

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.ofForests_zero_zero {α : Type u} {R : Type v} [Semiring R] : ofForests 0 0 = 1

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.ofPair_add {α : Type u} {R : Type v} [Semiring R] (x y : LRootedForest α × LRootedForest α) : ofPair (x + y) = ofPair x * ofPair y

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.ofForests_add {α : Type u} {R : Type v} [Semiring R] (φ₁ φ₂ ψ₁ ψ₂ : LRootedForest α) : ofForests (φ₁ + φ₂) (ψ₁ + ψ₂) = ofForests φ₁ ψ₁ * ofForests φ₂ ψ₂

noncomputable def HopfAlgebras.LForestTensorAlgebra.sumTerms {α : Type u} {R : Type v} [Semiring R] (terms : List (LRootedForest α × LRootedForest α)) : LForestTensorAlgebra α R

Sum a finite list of labelled basis tensors. Duplicates contribute multiplicity.

Equations

• HopfAlgebras.LForestTensorAlgebra.sumTerms terms = (List.map HopfAlgebras.LForestTensorAlgebra.ofPair terms).sum

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_nil {α : Type u} {R : Type v} [Semiring R] : sumTerms [] = 0

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_cons {α : Type u} {R : Type v} [Semiring R] (term : LRootedForest α × LRootedForest α) (terms : List (LRootedForest α × LRootedForest α)) : sumTerms (term :: terms) = ofPair term + sumTerms terms

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_singleton {α : Type u} {R : Type v} [Semiring R] (term : LRootedForest α × LRootedForest α) : sumTerms [term] = ofPair term

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_append {α : Type u} {R : Type v} [Semiring R] (xs ys : List (LRootedForest α × LRootedForest α)) : sumTerms (xs ++ ys) = sumTerms xs + sumTerms ys

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_perm {α : Type u} {R : Type v} [Semiring R] {xs ys : List (LRootedForest α × LRootedForest α)} (h : xs.Perm ys) : sumTerms xs = sumTerms ys

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_cut_forall₂_perm {α : Type u} {R : Type v} [Semiring R] {cs ds : List (PLTree.Cut α)} : List.Forall₂ PLTree.Cut.Perm cs ds → sumTerms (List.map (fun (c : PLTree.Cut α) => (c.prunedForest, c.trunkForest)) cs) = sumTerms (List.map (fun (d : PLTree.Cut α) => (d.prunedForest, d.trunkForest)) ds)

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_cut_listRelPerm {α : Type u} {R : Type v} [Semiring R] {cs ds : List (PLTree.Cut α)} (h : PTree.ListRelPerm PLTree.Cut.Perm cs ds) : sumTerms (List.map (fun (c : PLTree.Cut α) => (c.prunedForest, c.trunkForest)) cs) = sumTerms (List.map (fun (d : PLTree.Cut α) => (d.prunedForest, d.trunkForest)) ds)

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_map_add_left {α : Type u} {R : Type v} [Semiring R] (x : LRootedForest α × LRootedForest α) (ys : List (LRootedForest α × LRootedForest α)) : sumTerms (List.map (fun (y : LRootedForest α × LRootedForest α) => x + y) ys) = ofPair x * sumTerms ys

theorem HopfAlgebras.LForestTensorAlgebra.sumTerms_multiply {α : Type u} {R : Type v} [Semiring R] (xs ys : List (LRootedForest α × LRootedForest α)) : sumTerms (PLTree.multiplyCoproductTerms xs ys) = sumTerms xs * sumTerms ys

def HopfAlgebras.LForestTensorAlgebra.eraseTermAddHom {α : Type u} : LRootedForest α × LRootedForest α →+ RootedForest × RootedForest

Forget labels in a coproduct basis term, as an additive homomorphism.

Equations

• HopfAlgebras.LForestTensorAlgebra.eraseTermAddHom = { toFun := HopfAlgebras.PLTree.eraseCoproductTerm, map_zero' := HopfAlgebras.LForestTensorAlgebra.eraseTermAddHom._proof_1, map_add' := ⋯ }

noncomputable def HopfAlgebras.LForestTensorAlgebra.erase {α : Type u} {R : Type v} [Semiring R] (x : LForestTensorAlgebra α R) : ForestTensorAlgebra R

Forget labels in the tensor-coded labelled forest algebra.

Equations

• x.erase = AddMonoidAlgebra.mapDomain (⇑HopfAlgebras.LForestTensorAlgebra.eraseTermAddHom) x

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.erase_zero {α : Type u} {R : Type v} [Semiring R] : erase 0 = 0

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.erase_add {α : Type u} {R : Type v} [Semiring R] (x y : LForestTensorAlgebra α R) : (x + y).erase = x.erase + y.erase

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.erase_one {α : Type u} {R : Type v} [Semiring R] : erase 1 = 1

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.erase_mul {α : Type u} {R : Type v} [Semiring R] (x y : LForestTensorAlgebra α R) : (x * y).erase = x.erase * y.erase

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.erase_ofPair {α : Type u} {R : Type v} [Semiring R] (term : LRootedForest α × LRootedForest α) : (ofPair term).erase = ForestTensorAlgebra.ofPair (PLTree.eraseCoproductTerm term)

theorem HopfAlgebras.LForestTensorAlgebra.erase_sumTerms {α : Type u} {R : Type v} [Semiring R] (terms : List (LRootedForest α × LRootedForest α)) : (sumTerms terms).erase = ForestTensorAlgebra.sumTerms (List.map PLTree.eraseCoproductTerm terms)

Erasing labels commutes with summing finite tensor basis terms.

def HopfAlgebras.LForestTensorAlgebra.constLabelTermAddHom {α : Type u} (a : α) : RootedForest × RootedForest →+ LRootedForest α × LRootedForest α

Constantly label tensor basis terms as an additive homomorphism.

Equations

• HopfAlgebras.LForestTensorAlgebra.constLabelTermAddHom a = { toFun := HopfAlgebras.PLTree.constLabelCoproductTerm a, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def HopfAlgebras.LForestTensorAlgebra.constLabel {α : Type u} {R : Type v} [Semiring R] (a : α) (x : ForestTensorAlgebra R) : LForestTensorAlgebra α R

Label every vertex in tensor-coded unlabelled forest algebra terms by the same label.

Equations

• HopfAlgebras.LForestTensorAlgebra.constLabel a x = AddMonoidAlgebra.mapDomain (⇑(HopfAlgebras.LForestTensorAlgebra.constLabelTermAddHom a)) x

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.constLabel_zero {α : Type u} {R : Type v} [Semiring R] (a : α) : constLabel a 0 = 0

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.constLabel_add {α : Type u} {R : Type v} [Semiring R] (a : α) (x y : ForestTensorAlgebra R) : constLabel a (x + y) = constLabel a x + constLabel a y

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.constLabel_one {α : Type u} {R : Type v} [Semiring R] (a : α) : constLabel a 1 = 1

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.constLabel_mul {α : Type u} {R : Type v} [Semiring R] (a : α) (x y : ForestTensorAlgebra R) : constLabel a (x * y) = constLabel a x * constLabel a y

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.constLabel_ofPair {α : Type u} {R : Type v} [Semiring R] (a : α) (term : RootedForest × RootedForest) : constLabel a (ForestTensorAlgebra.ofPair term) = ofPair (PLTree.constLabelCoproductTerm a term)

theorem HopfAlgebras.LForestTensorAlgebra.constLabel_sumTerms {α : Type u} {R : Type v} [Semiring R] (a : α) (terms : List (RootedForest × RootedForest)) : constLabel a (ForestTensorAlgebra.sumTerms terms) = sumTerms (List.map (PLTree.constLabelCoproductTerm a) terms)

Constant labelling commutes with summing finite tensor basis terms.

def HopfAlgebras.LForestTensorAlgebra.mapLabelsTermAddHom {α : Type u} {β : Type w} (f : α → β) : LRootedForest α × LRootedForest α →+ LRootedForest β × LRootedForest β

Relabel tensor basis terms as an additive homomorphism.

Equations

• HopfAlgebras.LForestTensorAlgebra.mapLabelsTermAddHom f = { toFun := HopfAlgebras.PLTree.mapCoproductTerm f, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def HopfAlgebras.LForestTensorAlgebra.mapLabels {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (x : LForestTensorAlgebra α R) : LForestTensorAlgebra β R

Relabel tensor-coded labelled forest algebra terms.

Equations

• HopfAlgebras.LForestTensorAlgebra.mapLabels f x = AddMonoidAlgebra.mapDomain (⇑(HopfAlgebras.LForestTensorAlgebra.mapLabelsTermAddHom f)) x

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.mapLabels_zero {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) : mapLabels f 0 = 0

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.mapLabels_add {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (x y : LForestTensorAlgebra α R) : mapLabels f (x + y) = mapLabels f x + mapLabels f y

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.mapLabels_one {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) : mapLabels f 1 = 1

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.mapLabels_mul {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (x y : LForestTensorAlgebra α R) : mapLabels f (x * y) = mapLabels f x * mapLabels f y

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.mapLabels_ofPair {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (term : LRootedForest α × LRootedForest α) : mapLabels f (ofPair term) = ofPair (PLTree.mapCoproductTerm f term)

theorem HopfAlgebras.LForestTensorAlgebra.mapLabels_sumTerms {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (terms : List (LRootedForest α × LRootedForest α)) : mapLabels f (sumTerms terms) = sumTerms (List.map (PLTree.mapCoproductTerm f) terms)

Relabelling commutes with summing finite tensor basis terms.

noncomputable def HopfAlgebras.LForestTensorAlgebra.counitLeft {α : Type u} {R : Type v} [CommSemiring R] : LForestTensorAlgebra α R →ₐ[R] LForestAlgebra α R

Apply the labelled counit to the left tensor factor.

Equations

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

noncomputable def HopfAlgebras.LForestTensorAlgebra.counitRight {α : Type u} {R : Type v} [CommSemiring R] : LForestTensorAlgebra α R →ₐ[R] LForestAlgebra α R

Apply the labelled counit to the right tensor factor.

Equations

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

theorem HopfAlgebras.LForestTensorAlgebra.counitLeft_ofPair {α : Type u} {R : Type v} [CommSemiring R] (term : LRootedForest α × LRootedForest α) : counitLeft (ofPair term) = LForestAlgebra.counitCoeff term.1 • LForestAlgebra.ofForest term.2

theorem HopfAlgebras.LForestTensorAlgebra.counitRight_ofPair {α : Type u} {R : Type v} [CommSemiring R] (term : LRootedForest α × LRootedForest α) : counitRight (ofPair term) = LForestAlgebra.counitCoeff term.2 • LForestAlgebra.ofForest term.1

theorem HopfAlgebras.LForestTensorAlgebra.counitLeft_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (terms : List (LRootedForest α × LRootedForest α)) : counitLeft (sumTerms terms) = (List.map (fun (term : LRootedForest α × LRootedForest α) => LForestAlgebra.counitCoeff term.1 • LForestAlgebra.ofForest term.2) terms).sum

theorem HopfAlgebras.LForestTensorAlgebra.counitRight_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (terms : List (LRootedForest α × LRootedForest α)) : counitRight (sumTerms terms) = (List.map (fun (term : LRootedForest α × LRootedForest α) => LForestAlgebra.counitCoeff term.2 • LForestAlgebra.ofForest term.1) terms).sum

@[reducible, inline]

abbrev HopfAlgebras.LForestTripleTensorAlgebra (α : Type u) (R : Type v) [Semiring R] : Type (max u v)

Triple tensor-coded labelled forest algebra: (φ, ψ, η) represents the basis tensor φ ⊗ ψ ⊗ η.

Equations

• HopfAlgebras.LForestTripleTensorAlgebra α R = AddMonoidAlgebra R (HopfAlgebras.LRootedForest α × HopfAlgebras.LRootedForest α × HopfAlgebras.LRootedForest α)

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.ofTriple {α : Type u} {R : Type v} [Semiring R] (term : LRootedForest α × LRootedForest α × LRootedForest α) : LForestTripleTensorAlgebra α R

The basis triple tensor represented by a triple of labelled rooted forests.

Equations

• HopfAlgebras.LForestTripleTensorAlgebra.ofTriple term = AddMonoidAlgebra.single term 1

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.ofForests {α : Type u} {R : Type v} [Semiring R] (φ ψ η : LRootedForest α) : LForestTripleTensorAlgebra α R

The basis tensor φ ⊗ ψ ⊗ η.

Equations

• HopfAlgebras.LForestTripleTensorAlgebra.ofForests φ ψ η = HopfAlgebras.LForestTripleTensorAlgebra.ofTriple (φ, ψ, η)

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.ofTriple_zero {α : Type u} {R : Type v} [Semiring R] : ofTriple 0 = 1

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.ofForests_zero_zero_zero {α : Type u} {R : Type v} [Semiring R] : ofForests 0 0 0 = 1

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.ofTriple_add {α : Type u} {R : Type v} [Semiring R] (x y : LRootedForest α × LRootedForest α × LRootedForest α) : ofTriple (x + y) = ofTriple x * ofTriple y

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.ofForests_add {α : Type u} {R : Type v} [Semiring R] (φ₁ φ₂ ψ₁ ψ₂ η₁ η₂ : LRootedForest α) : ofForests (φ₁ + φ₂) (ψ₁ + ψ₂) (η₁ + η₂) = ofForests φ₁ ψ₁ η₁ * ofForests φ₂ ψ₂ η₂

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.sumTerms {α : Type u} {R : Type v} [Semiring R] (terms : List (LRootedForest α × LRootedForest α × LRootedForest α)) : LForestTripleTensorAlgebra α R

Sum a finite list of labelled basis triple tensors. Duplicates contribute multiplicity.

Equations

• HopfAlgebras.LForestTripleTensorAlgebra.sumTerms terms = (List.map HopfAlgebras.LForestTripleTensorAlgebra.ofTriple terms).sum

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nil {α : Type u} {R : Type v} [Semiring R] : sumTerms [] = 0

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_cons {α : Type u} {R : Type v} [Semiring R] (term : LRootedForest α × LRootedForest α × LRootedForest α) (terms : List (LRootedForest α × LRootedForest α × LRootedForest α)) : sumTerms (term :: terms) = ofTriple term + sumTerms terms

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_singleton {α : Type u} {R : Type v} [Semiring R] (term : LRootedForest α × LRootedForest α × LRootedForest α) : sumTerms [term] = ofTriple term

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_append {α : Type u} {R : Type v} [Semiring R] (xs ys : List (LRootedForest α × LRootedForest α × LRootedForest α)) : sumTerms (xs ++ ys) = sumTerms xs + sumTerms ys

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_perm {α : Type u} {R : Type v} [Semiring R] {xs ys : List (LRootedForest α × LRootedForest α × LRootedForest α)} (h : xs.Perm ys) : sumTerms xs = sumTerms ys

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

Multiply two finite lists of labelled triple tensor basis terms.

Equations

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

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_map_add_left {α : Type u} {R : Type v} [Semiring R] (x : LRootedForest α × LRootedForest α × LRootedForest α) (ys : List (LRootedForest α × LRootedForest α × LRootedForest α)) : sumTerms (List.map (fun (y : LRootedForest α × LRootedForest α × LRootedForest α) => x + y) ys) = ofTriple x * sumTerms ys

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_multiply {α : Type u} {R : Type v} [Semiring R] (xs ys : List (LRootedForest α × LRootedForest α × LRootedForest α)) : sumTerms (multiplyTerms xs ys) = sumTerms xs * sumTerms ys

def HopfAlgebras.LForestTripleTensorAlgebra.eraseTripleTermAddHom {α : Type u} : LRootedForest α × LRootedForest α × LRootedForest α →+ RootedForest × RootedForest × RootedForest

Forget labels in a triple tensor basis term, as an additive homomorphism.

Equations

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

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.erase {α : Type u} {R : Type v} [Semiring R] (x : LForestTripleTensorAlgebra α R) : ForestTripleTensorAlgebra R

Forget labels in the triple tensor-coded labelled forest algebra.

Equations

• x.erase = AddMonoidAlgebra.mapDomain (⇑HopfAlgebras.LForestTripleTensorAlgebra.eraseTripleTermAddHom) x

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_zero {α : Type u} {R : Type v} [Semiring R] : erase 0 = 0

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_add {α : Type u} {R : Type v} [Semiring R] (x y : LForestTripleTensorAlgebra α R) : (x + y).erase = x.erase + y.erase

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_one {α : Type u} {R : Type v} [Semiring R] : erase 1 = 1

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_mul {α : Type u} {R : Type v} [Semiring R] (x y : LForestTripleTensorAlgebra α R) : (x * y).erase = x.erase * y.erase

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_ofTriple {α : Type u} {R : Type v} [Semiring R] (term : LRootedForest α × LRootedForest α × LRootedForest α) : (ofTriple term).erase = ForestTripleTensorAlgebra.ofTriple (eraseTripleTermAddHom term)

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_sumTerms {α : Type u} {R : Type v} [Semiring R] (terms : List (LRootedForest α × LRootedForest α × LRootedForest α)) : (sumTerms terms).erase = ForestTripleTensorAlgebra.sumTerms (List.map (⇑eraseTripleTermAddHom) terms)

Erasing labels commutes with summing finite triple tensor basis terms.

def HopfAlgebras.LForestTripleTensorAlgebra.constLabelTripleTermAddHom {α : Type u} (a : α) : RootedForest × RootedForest × RootedForest →+ LRootedForest α × LRootedForest α × LRootedForest α

Constantly label triple tensor basis terms as an additive homomorphism.

Equations

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

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.constLabel {α : Type u} {R : Type v} [Semiring R] (a : α) (x : ForestTripleTensorAlgebra R) : LForestTripleTensorAlgebra α R

Label every vertex in triple tensor-coded unlabelled forest algebra terms by one label.

Equations

• HopfAlgebras.LForestTripleTensorAlgebra.constLabel a x = AddMonoidAlgebra.mapDomain (⇑(HopfAlgebras.LForestTripleTensorAlgebra.constLabelTripleTermAddHom a)) x

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_zero {α : Type u} {R : Type v} [Semiring R] (a : α) : constLabel a 0 = 0

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_add {α : Type u} {R : Type v} [Semiring R] (a : α) (x y : ForestTripleTensorAlgebra R) : constLabel a (x + y) = constLabel a x + constLabel a y

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_one {α : Type u} {R : Type v} [Semiring R] (a : α) : constLabel a 1 = 1

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_mul {α : Type u} {R : Type v} [Semiring R] (a : α) (x y : ForestTripleTensorAlgebra R) : constLabel a (x * y) = constLabel a x * constLabel a y

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_ofTriple {α : Type u} {R : Type v} [Semiring R] (a : α) (term : RootedForest × RootedForest × RootedForest) : constLabel a (ForestTripleTensorAlgebra.ofTriple term) = ofTriple ((constLabelTripleTermAddHom a) term)

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_sumTerms {α : Type u} {R : Type v} [Semiring R] (a : α) (terms : List (RootedForest × RootedForest × RootedForest)) : constLabel a (ForestTripleTensorAlgebra.sumTerms terms) = sumTerms (List.map (⇑(constLabelTripleTermAddHom a)) terms)

Constant labelling commutes with summing finite triple tensor basis terms.

def HopfAlgebras.LForestTripleTensorAlgebra.mapLabelsTripleTermAddHom {α : Type u} {β : Type w} (f : α → β) : LRootedForest α × LRootedForest α × LRootedForest α →+ LRootedForest β × LRootedForest β × LRootedForest β

Relabel triple tensor basis terms as an additive homomorphism.

Equations

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

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.mapLabels {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (x : LForestTripleTensorAlgebra α R) : LForestTripleTensorAlgebra β R

Relabel triple tensor-coded labelled forest algebra terms.

Equations

• HopfAlgebras.LForestTripleTensorAlgebra.mapLabels f x = AddMonoidAlgebra.mapDomain (⇑(HopfAlgebras.LForestTripleTensorAlgebra.mapLabelsTripleTermAddHom f)) x

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_zero {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) : mapLabels f 0 = 0

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_add {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (x y : LForestTripleTensorAlgebra α R) : mapLabels f (x + y) = mapLabels f x + mapLabels f y

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_one {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) : mapLabels f 1 = 1

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_mul {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (x y : LForestTripleTensorAlgebra α R) : mapLabels f (x * y) = mapLabels f x * mapLabels f y

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_ofTriple {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (term : LRootedForest α × LRootedForest α × LRootedForest α) : mapLabels f (ofTriple term) = ofTriple ((mapLabelsTripleTermAddHom f) term)

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_sumTerms {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (terms : List (LRootedForest α × LRootedForest α × LRootedForest α)) : mapLabels f (sumTerms terms) = sumTerms (List.map (⇑(mapLabelsTripleTermAddHom f)) terms)

Relabelling commutes with summing finite triple tensor basis terms.

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.includeLeftPair {α : Type u} {R : Type v} [CommSemiring R] : LForestTensorAlgebra α R →ₐ[R] LForestTripleTensorAlgebra α R

Embed a labelled pair tensor as the first two factors of a triple tensor.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.includeLeftPair_ofPair {α : Type u} {R : Type v} [CommSemiring R] (term : LRootedForest α × LRootedForest α) : includeLeftPair (LForestTensorAlgebra.ofPair term) = ofTriple (term.1, term.2, 0)

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.includeLeftPair_ofForests {α : Type u} {R : Type v} [CommSemiring R] (φ ψ : LRootedForest α) : includeLeftPair (LForestTensorAlgebra.ofForests φ ψ) = ofForests φ ψ 0

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.includeRightPair {α : Type u} {R : Type v} [CommSemiring R] : LForestTensorAlgebra α R →ₐ[R] LForestTripleTensorAlgebra α R

Embed a labelled pair tensor as the last two factors of a triple tensor.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.includeRightPair_ofPair {α : Type u} {R : Type v} [CommSemiring R] (term : LRootedForest α × LRootedForest α) : includeRightPair (LForestTensorAlgebra.ofPair term) = ofTriple (0, term.1, term.2)

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.includeRightPair_ofForests {α : Type u} {R : Type v} [CommSemiring R] (φ ψ : LRootedForest α) : includeRightPair (LForestTensorAlgebra.ofForests φ ψ) = ofForests 0 φ ψ

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_includeLeftPair {α : Type u} {R : Type v} [CommSemiring R] (x : LForestTensorAlgebra α R) : (includeLeftPair x).erase = ForestTripleTensorAlgebra.includeLeftPair x.erase

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_includeRightPair {α : Type u} {R : Type v} [CommSemiring R] (x : LForestTensorAlgebra α R) : (includeRightPair x).erase = ForestTripleTensorAlgebra.includeRightPair x.erase

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_includeLeftPair {α : Type u} {R : Type v} [CommSemiring R] (a : α) (x : ForestTensorAlgebra R) : constLabel a (ForestTripleTensorAlgebra.includeLeftPair x) = includeLeftPair (LForestTensorAlgebra.constLabel a x)

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_includeRightPair {α : Type u} {R : Type v} [CommSemiring R] (a : α) (x : ForestTensorAlgebra R) : constLabel a (ForestTripleTensorAlgebra.includeRightPair x) = includeRightPair (LForestTensorAlgebra.constLabel a x)

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_includeLeftPair {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (x : LForestTensorAlgebra α R) : mapLabels f (includeLeftPair x) = includeLeftPair (LForestTensorAlgebra.mapLabels f x)

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_includeRightPair {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (x : LForestTensorAlgebra α R) : mapLabels f (includeRightPair x) = includeRightPair (LForestTensorAlgebra.mapLabels f x)

noncomputable def HopfAlgebras.PLTree.labelledCoproduct {α : Type u} {R : Type v} [Semiring R] (t : PLTree α) : LForestTensorAlgebra α R

The planar labelled BCK coproduct, represented in the tensor-coded algebra.

Equations

• t.labelledCoproduct = HopfAlgebras.LForestTensorAlgebra.sumTerms t.coproductTerms

noncomputable def HopfAlgebras.PLTree.labelledReducedCoproduct {α : Type u} {R : Type v} [Semiring R] (t : PLTree α) : LForestTensorAlgebra α R

The reduced planar labelled BCK coproduct, summing only proper cut terms.

Equations

• t.labelledReducedCoproduct = HopfAlgebras.LForestTensorAlgebra.sumTerms t.properCoproductTerms

theorem HopfAlgebras.PLTree.labelledReducedCoproduct_perm {α : Type u} {R : Type v} [Semiring R] {t u : PLTree α} (h : t.Perm u) : t.labelledReducedCoproduct = u.labelledReducedCoproduct

theorem HopfAlgebras.PLTree.labelledCoproduct_eq_of_cuts_listRelPerm {α : Type u} {R : Type v} [Semiring R] {t u : PLTree α} (h : PTree.ListRelPerm Cut.Perm t.cuts u.cuts) : t.labelledCoproduct = u.labelledCoproduct

theorem HopfAlgebras.PLTree.labelledCoproduct_perm {α : Type u} {R : Type v} [Semiring R] {t u : PLTree α} (h : t.Perm u) : t.labelledCoproduct = u.labelledCoproduct

theorem HopfAlgebras.PLTree.labelledCoproduct_node {α : Type u} {R : Type v} [Semiring R] (a : α) (ts : List (PLTree α)) : (node a ts).labelledCoproduct = LForestTensorAlgebra.sumTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, LRootedForest.singleton (LRootedForest.graft a term.2))) (coproductTermsList ts)) + LForestTensorAlgebra.ofPair (LRootedForest.singleton (LRootedTree.ofPLTree (node a ts)), 0)

noncomputable def HopfAlgebras.PLTree.labelledCoproductList {α : Type u} {R : Type v} [Semiring R] (ts : List (PLTree α)) : LForestTensorAlgebra α R

Multiplicative extension of the planar labelled coproduct to labelled forests.

Equations

• HopfAlgebras.PLTree.labelledCoproductList ts = HopfAlgebras.LForestTensorAlgebra.sumTerms (HopfAlgebras.PLTree.coproductTermsList ts)

noncomputable def HopfAlgebras.PLTree.labelledReducedCoproductList {α : Type u} {R : Type v} [Semiring R] (ts : List (PLTree α)) : LForestTensorAlgebra α R

The reduced planar labelled BCK coproduct of a planar labelled forest.

Equations

• HopfAlgebras.PLTree.labelledReducedCoproductList ts = HopfAlgebras.LForestTensorAlgebra.sumTerms (HopfAlgebras.PLTree.properCoproductTermsList ts)

theorem HopfAlgebras.PLTree.erase_labelledCoproduct {α : Type u} {R : Type v} [Semiring R] (t : PLTree α) : t.labelledCoproduct.erase = t.erase.coproduct

Erasing labels sends the labelled planar coproduct to the unlabelled coproduct.

theorem HopfAlgebras.PLTree.erase_labelledReducedCoproduct {α : Type u} {R : Type v} [Semiring R] (t : PLTree α) : t.labelledReducedCoproduct.erase = t.erase.reducedCoproduct

theorem HopfAlgebras.PLTree.erase_labelledCoproductList {α : Type u} {R : Type v} [Semiring R] (ts : List (PLTree α)) : (labelledCoproductList ts).erase = PTree.coproductList (List.map erase ts)

Erasing labels sends the labelled planar forest coproduct to the unlabelled coproduct.

theorem HopfAlgebras.PLTree.erase_labelledReducedCoproductList {α : Type u} {R : Type v} [Semiring R] (ts : List (PLTree α)) : (labelledReducedCoproductList ts).erase = PTree.reducedCoproductList (List.map erase ts)

theorem HopfAlgebras.PLTree.mapLabels_labelledCoproduct {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (t : PLTree α) : LForestTensorAlgebra.mapLabels f t.labelledCoproduct = (map f t).labelledCoproduct

theorem HopfAlgebras.PLTree.mapLabels_labelledReducedCoproduct {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (t : PLTree α) : LForestTensorAlgebra.mapLabels f t.labelledReducedCoproduct = (map f t).labelledReducedCoproduct

theorem HopfAlgebras.PLTree.mapLabels_labelledCoproductList {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (ts : List (PLTree α)) : LForestTensorAlgebra.mapLabels f (labelledCoproductList ts) = labelledCoproductList (List.map (map f) ts)

theorem HopfAlgebras.PLTree.mapLabels_labelledReducedCoproductList {α : Type u} {R : Type v} [Semiring R] {β : Type w} (f : α → β) (ts : List (PLTree α)) : LForestTensorAlgebra.mapLabels f (labelledReducedCoproductList ts) = labelledReducedCoproductList (List.map (map f) ts)

theorem HopfAlgebras.PLTree.constLabel_labelledCoproduct {α : Type u} {R : Type v} [Semiring R] (a : α) (t : PTree) : LForestTensorAlgebra.constLabel a t.coproduct = (constLabel a t).labelledCoproduct

theorem HopfAlgebras.PLTree.constLabel_labelledReducedCoproduct {α : Type u} {R : Type v} [Semiring R] (a : α) (t : PTree) : LForestTensorAlgebra.constLabel a t.reducedCoproduct = (constLabel a t).labelledReducedCoproduct

theorem HopfAlgebras.PLTree.constLabel_labelledCoproductList {α : Type u} {R : Type v} [Semiring R] (a : α) (ts : List PTree) : LForestTensorAlgebra.constLabel a (PTree.coproductList ts) = labelledCoproductList (List.map (constLabel a) ts)

theorem HopfAlgebras.PLTree.constLabel_labelledReducedCoproductList {α : Type u} {R : Type v} [Semiring R] (a : α) (ts : List PTree) : LForestTensorAlgebra.constLabel a (PTree.reducedCoproductList ts) = labelledReducedCoproductList (List.map (constLabel a) ts)

@[simp]

theorem HopfAlgebras.PLTree.labelledCoproductList_nil {α : Type u} {R : Type v} [Semiring R] : labelledCoproductList [] = 1

@[simp]

theorem HopfAlgebras.PLTree.labelledReducedCoproductList_nil {α : Type u} {R : Type v} [Semiring R] : labelledReducedCoproductList [] = 0

theorem HopfAlgebras.PLTree.labelledReducedCoproductList_forall₂_perm {α : Type u} {R : Type v} [Semiring R] {ts us : List (PLTree α)} (h : List.Forall₂ Perm ts us) : labelledReducedCoproductList ts = labelledReducedCoproductList us

@[simp]

theorem HopfAlgebras.PLTree.labelledCoproductList_cons {α : Type u} {R : Type v} [Semiring R] (t : PLTree α) (ts : List (PLTree α)) : labelledCoproductList (t :: ts) = t.labelledCoproduct * labelledCoproductList ts

@[simp]

theorem HopfAlgebras.PLTree.labelledCoproductList_singleton {α : Type u} {R : Type v} [Semiring R] (t : PLTree α) : labelledCoproductList [t] = t.labelledCoproduct

theorem HopfAlgebras.PLTree.labelledCoproductList_append {α : Type u} {R : Type v} [Semiring R] (ts us : List (PLTree α)) : labelledCoproductList (ts ++ us) = labelledCoproductList ts * labelledCoproductList us

theorem HopfAlgebras.PLTree.labelledCoproductList_perm {α : Type u} {R : Type v} [CommSemiring R] {ts us : List (PLTree α)} (h : ts.Perm us) : labelledCoproductList ts = labelledCoproductList us

theorem HopfAlgebras.PLTree.labelledCoproductList_forall₂_perm {α : Type u} {R : Type v} [CommSemiring R] {ts us : List (PLTree α)} : List.Forall₂ Perm ts us → labelledCoproductList ts = labelledCoproductList us

theorem HopfAlgebras.PLTree.counitLeft_labelledCoproduct {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : LForestTensorAlgebra.counitLeft t.labelledCoproduct = LForestAlgebra.ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t))

theorem HopfAlgebras.PLTree.counitRight_labelledCoproduct {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : LForestTensorAlgebra.counitRight t.labelledCoproduct = LForestAlgebra.ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t))

theorem HopfAlgebras.LRootedForest.coproductTermsList_out_order {α : Type u} {ts : List (LRootedTree α)} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ PLTree.coproductTermsList (List.map Quotient.out ts)) : term.1.order + term.2.order = order ↑ts

noncomputable def HopfAlgebras.LRootedForest.coproductTerms {α : Type u} (φ : LRootedForest α) : List (LRootedForest α × LRootedForest α)

A finite representative list for the labelled forest coproduct, using Quotient.out.

Equations

• φ.coproductTerms = HopfAlgebras.PLTree.coproductTermsList (List.map Quotient.out (Quotient.out φ))

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

theorem HopfAlgebras.LRootedForest.coproductTerms_left_eq_zero {α : Type u} {φ : LRootedForest α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ φ.coproductTerms) (hleft : term.1 = 0) : term.2 = φ

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

theorem HopfAlgebras.LRootedForest.coproductTerms_right_eq_zero {α : Type u} {φ : LRootedForest α} {term : LRootedForest α × LRootedForest α} (hterm : term ∈ φ.coproductTerms) (hright : term.2 = 0) : term.1 = φ

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

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

The labelled forest coproduct has exactly one term with empty left factor.

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

The labelled forest coproduct has exactly one term with empty right factor.

theorem HopfAlgebras.LRootedForest.coproductTerms_ofPLTree_list_perm {α : Type u} (ts : List (PLTree α)) : (coproductTerms ↑(List.map LRootedTree.ofPLTree ts)).Perm (PLTree.coproductTermsList ts)

theorem HopfAlgebras.LRootedForest.coproductTerms_singleton_ofPLTree_perm {α : Type u} (t : PLTree α) : (singleton (LRootedTree.ofPLTree t)).coproductTerms.Perm t.coproductTerms

theorem HopfAlgebras.LRootedForest.coproductTerms_singleton_graft_perm {α : Type u} (a : α) (φ : LRootedForest α) : (singleton (graft a φ)).coproductTerms.Perm (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, singleton (graft a term.2))) φ.coproductTerms ++ [(singleton (graft a φ), 0)])

theorem HopfAlgebras.LRootedForest.coproductTerms_add_perm {α : Type u} (φ ψ : LRootedForest α) : (φ + ψ).coproductTerms.Perm (PLTree.multiplyCoproductTerms φ.coproductTerms ψ.coproductTerms)

noncomputable def HopfAlgebras.LRootedForest.properCoproductTerms {α : Type u} (φ : LRootedForest α) : List (LRootedForest α × LRootedForest α)

A finite representative list for the reduced labelled forest coproduct.

Equations

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

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

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

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

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

theorem HopfAlgebras.LRootedForest.coproductTerms_erase_perm {α : Type u} (φ : LRootedForest α) : (List.map PLTree.eraseCoproductTerm φ.coproductTerms).Perm φ.erase.coproductTerms

theorem HopfAlgebras.LRootedForest.properCoproductTerms_erase_perm {α : Type u} (φ : LRootedForest α) : (List.map PLTree.eraseCoproductTerm φ.properCoproductTerms).Perm φ.erase.properCoproductTerms

theorem HopfAlgebras.LRootedForest.properCoproductTerms_mapLabels_perm {α : Type u} {β : Type w} (f : α → β) (φ : LRootedForest α) : (List.map (PLTree.mapCoproductTerm f) φ.properCoproductTerms).Perm (mapLabels f φ).properCoproductTerms

theorem HopfAlgebras.LRootedForest.properCoproductTerms_constLabel_perm {α : Type u} (a : α) (φ : RootedForest) : (List.map (PLTree.constLabelCoproductTerm a) φ.properCoproductTerms).Perm (constLabel a φ).properCoproductTerms

noncomputable def HopfAlgebras.LRootedForest.coproduct {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : LForestTensorAlgebra α R

The multiplicative labelled coproduct of a non-planar labelled forest.

Equations

• φ.coproduct = Quotient.lift (fun (ts : List (HopfAlgebras.LRootedTree α)) => HopfAlgebras.PLTree.labelledCoproductList (List.map Quotient.out ts)) ⋯ φ

@[simp]

theorem HopfAlgebras.LRootedForest.coproduct_coe {α : Type u} {R : Type v} [CommSemiring R] (ts : List (LRootedTree α)) : coproduct ↑ts = PLTree.labelledCoproductList (List.map Quotient.out ts)

theorem HopfAlgebras.LRootedForest.coproduct_ofPLTree_list {α : Type u} {R : Type v} [CommSemiring R] (ts : List (PLTree α)) : coproduct ↑(List.map LRootedTree.ofPLTree ts) = PLTree.labelledCoproductList ts

theorem HopfAlgebras.LRootedForest.coproduct_eq_sumTerms_coproductTerms {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : φ.coproduct = LForestTensorAlgebra.sumTerms φ.coproductTerms

noncomputable def HopfAlgebras.LRootedForest.reducedCoproduct {α : Type u} {R : Type v} [Semiring R] (φ : LRootedForest α) : LForestTensorAlgebra α R

The reduced BCK coproduct of a non-planar labelled forest.

Equations

• φ.reducedCoproduct = HopfAlgebras.LForestTensorAlgebra.sumTerms φ.properCoproductTerms

@[simp]

theorem HopfAlgebras.LRootedForest.reducedCoproduct_zero {α : Type u} {R : Type v} [Semiring R] : reducedCoproduct 0 = 0

@[simp]

theorem HopfAlgebras.LRootedForest.reducedCoproduct_empty {α : Type u} {R : Type v} [Semiring R] : empty.reducedCoproduct = 0

@[simp]

theorem HopfAlgebras.LRootedForest.coproduct_zero {α : Type u} {R : Type v} [CommSemiring R] : coproduct 0 = 1

@[simp]

theorem HopfAlgebras.LRootedForest.coproduct_empty {α : Type u} {R : Type v} [CommSemiring R] : empty.coproduct = 1

@[simp]

theorem HopfAlgebras.LRootedForest.coproduct_singleton {α : Type u} {R : Type v} [CommSemiring R] (τ : LRootedTree α) : (singleton τ).coproduct = (Quotient.out τ).labelledCoproduct

theorem HopfAlgebras.LRootedForest.coproduct_singleton_ofPLTree {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : (singleton (LRootedTree.ofPLTree t)).coproduct = t.labelledCoproduct

@[simp]

theorem HopfAlgebras.LRootedForest.coproduct_add {α : Type u} {R : Type v} [CommSemiring R] (φ ψ : LRootedForest α) : (φ + ψ).coproduct = φ.coproduct * ψ.coproduct

theorem HopfAlgebras.LRootedForest.counitLeft_coproduct {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : LForestTensorAlgebra.counitLeft φ.coproduct = LForestAlgebra.ofForest φ

theorem HopfAlgebras.LRootedForest.counitRight_coproduct {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : LForestTensorAlgebra.counitRight φ.coproduct = LForestAlgebra.ofForest φ

theorem HopfAlgebras.LRootedForest.erase_coproduct {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : φ.coproduct.erase = φ.erase.coproduct

theorem HopfAlgebras.LRootedForest.mapLabels_coproduct {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (φ : LRootedForest α) : LForestTensorAlgebra.mapLabels f φ.coproduct = (mapLabels f φ).coproduct

theorem HopfAlgebras.LRootedForest.constLabel_coproduct {α : Type u} {R : Type v} [CommSemiring R] (a : α) (φ : RootedForest) : LForestTensorAlgebra.constLabel a φ.coproduct = (constLabel a φ).coproduct

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.coproductLeft {α : Type u} {R : Type v} [CommSemiring R] : LForestTensorAlgebra α R →ₐ[R] LForestTripleTensorAlgebra α R

Apply the labelled coproduct to the first tensor factor, the map Δ ⊗ id.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeft_ofPair {α : Type u} {R : Type v} [CommSemiring R] (term : LRootedForest α × LRootedForest α) : coproductLeft (LForestTensorAlgebra.ofPair term) = includeLeftPair term.1.coproduct * ofForests 0 0 term.2

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeft_ofForests {α : Type u} {R : Type v} [CommSemiring R] (φ ψ : LRootedForest α) : coproductLeft (LForestTensorAlgebra.ofForests φ ψ) = includeLeftPair φ.coproduct * ofForests 0 0 ψ

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.coproductRight {α : Type u} {R : Type v} [CommSemiring R] : LForestTensorAlgebra α R →ₐ[R] LForestTripleTensorAlgebra α R

Apply the labelled coproduct to the second tensor factor, the map id ⊗ Δ.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRight_ofPair {α : Type u} {R : Type v} [CommSemiring R] (term : LRootedForest α × LRootedForest α) : coproductRight (LForestTensorAlgebra.ofPair term) = ofForests term.1 0 0 * includeRightPair term.2.coproduct

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRight_ofForests {α : Type u} {R : Type v} [CommSemiring R] (φ ψ : LRootedForest α) : coproductRight (LForestTensorAlgebra.ofForests φ ψ) = ofForests φ 0 0 * includeRightPair ψ.coproduct

theorem HopfAlgebras.LForestTripleTensorAlgebra.includeLeftPair_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (terms : List (LRootedForest α × LRootedForest α)) : includeLeftPair (LForestTensorAlgebra.sumTerms terms) = sumTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, term.2, 0)) terms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.includeRightPair_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (terms : List (LRootedForest α × LRootedForest α)) : includeRightPair (LForestTensorAlgebra.sumTerms terms) = sumTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (0, term.1, term.2)) terms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_liftLeft_mul_ofForests {α : Type u} {R : Type v} [CommSemiring R] (terms : List (LRootedForest α × LRootedForest α)) (ψ : LRootedForest α) : sumTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, term.2, 0)) terms) * ofForests 0 0 ψ = sumTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, term.2, ψ)) terms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.ofForests_mul_sumTerms_liftRight {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) (terms : List (LRootedForest α × LRootedForest α)) : ofForests φ 0 0 * sumTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (0, term.1, term.2)) terms) = sumTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (φ, term.1, term.2)) terms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.multiplyTerms_append_left {α : Type u} (xs ys zs : List (LRootedForest α × LRootedForest α × LRootedForest α)) : multiplyTerms (xs ++ ys) zs = multiplyTerms xs zs ++ multiplyTerms ys zs

theorem HopfAlgebras.LForestTripleTensorAlgebra.multiplyTerms_perm_left {α : Type u} {xs ys zs : List (LRootedForest α × LRootedForest α × LRootedForest α)} (h : xs.Perm ys) : (multiplyTerms xs zs).Perm (multiplyTerms ys zs)

theorem HopfAlgebras.LForestTripleTensorAlgebra.multiplyTerms_perm_right {α : Type u} {xs ys zs : List (LRootedForest α × LRootedForest α × LRootedForest α)} (h : ys.Perm zs) : (multiplyTerms xs ys).Perm (multiplyTerms xs zs)

theorem HopfAlgebras.LForestTripleTensorAlgebra.multiplyTerms_perm {α : Type u} {xs xs' ys ys' : List (LRootedForest α × LRootedForest α × LRootedForest α)} (hxs : xs.Perm xs') (hys : ys.Perm ys') : (multiplyTerms xs ys).Perm (multiplyTerms xs' ys')

theorem HopfAlgebras.LForestTripleTensorAlgebra.flatMap_multiplyTerms_right_perm {α : Type u} {β : Type u_1} (xs : List (LRootedForest α × LRootedForest α × LRootedForest α)) (ys : List β) (f : β → List (LRootedForest α × LRootedForest α × LRootedForest α)) : (List.flatMap (fun (y : β) => multiplyTerms xs (f y)) ys).Perm (multiplyTerms xs (List.flatMap f ys))

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerm {α : Type u} (term : LRootedForest α × LRootedForest α) : List (LRootedForest α × LRootedForest α × LRootedForest α)

Equations

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

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerm {α : Type u} (term : LRootedForest α × LRootedForest α) : List (LRootedForest α × LRootedForest α × LRootedForest α)

Equations

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

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms {α : Type u} (terms : List (LRootedForest α × LRootedForest α)) : List (LRootedForest α × LRootedForest α × LRootedForest α)

Equations

• HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms terms = List.flatMap HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerm terms

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms {α : Type u} (terms : List (LRootedForest α × LRootedForest α)) : List (LRootedForest α × LRootedForest α × LRootedForest α)

Equations

• HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms terms = List.flatMap HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerm terms

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerm_add_perm {α : Type u} (x y : LRootedForest α × LRootedForest α) : (coproductLeftTerm (x + y)).Perm (multiplyTerms (coproductLeftTerm x) (coproductLeftTerm y))

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerm_add_perm {α : Type u} (x y : LRootedForest α × LRootedForest α) : (coproductRightTerm (x + y)).Perm (multiplyTerms (coproductRightTerm x) (coproductRightTerm y))

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerm_singleton_graft_zero_perm {α : Type u} (a : α) (φ : LRootedForest α) : (coproductLeftTerm (LRootedForest.singleton (LRootedForest.graft a φ), 0)).Perm (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, LRootedForest.singleton (LRootedForest.graft a term.2), 0)) φ.coproductTerms ++ [(LRootedForest.singleton (LRootedForest.graft a φ), 0, 0)])

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerm_singleton_graft_perm {α : Type u} (a : α) (φ ψ : LRootedForest α) : (coproductRightTerm (φ, LRootedForest.singleton (LRootedForest.graft a ψ))).Perm (List.map (fun (term : LRootedForest α × LRootedForest α) => (φ, term.1, LRootedForest.singleton (LRootedForest.graft a term.2))) ψ.coproductTerms ++ [(φ, LRootedForest.singleton (LRootedForest.graft a ψ), 0)])

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms_append {α : Type u} (xs ys : List (LRootedForest α × LRootedForest α)) : coproductLeftTerms (xs ++ ys) = coproductLeftTerms xs ++ coproductLeftTerms ys

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms_append {α : Type u} (xs ys : List (LRootedForest α × LRootedForest α)) : coproductRightTerms (xs ++ ys) = coproductRightTerms xs ++ coproductRightTerms ys

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms_map_singleton_graft {α : Type u} (a : α) (terms : List (LRootedForest α × LRootedForest α)) : coproductLeftTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, LRootedForest.singleton (LRootedForest.graft a term.2))) terms) = List.map (fun (triple : LRootedForest α × LRootedForest α × LRootedForest α) => (triple.1, triple.2.1, LRootedForest.singleton (LRootedForest.graft a triple.2.2))) (coproductLeftTerms terms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms_map_singleton_graft_perm {α : Type u} (a : α) (terms : List (LRootedForest α × LRootedForest α)) : (coproductRightTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, LRootedForest.singleton (LRootedForest.graft a term.2))) terms)).Perm (List.map (fun (triple : LRootedForest α × LRootedForest α × LRootedForest α) => (triple.1, triple.2.1, LRootedForest.singleton (LRootedForest.graft a triple.2.2))) (coproductRightTerms terms) ++ List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, LRootedForest.singleton (LRootedForest.graft a term.2), 0)) terms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerm_zero_perm {α : Type u} (φ : LRootedForest α) : (coproductRightTerm (φ, 0)).Perm [(φ, 0, 0)]

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductTerms_node_left_right_perm_of_coproductTermsList_perm {α : Type u} (a : α) (ts : List (PLTree α)) (h : (coproductLeftTerms (PLTree.coproductTermsList ts)).Perm (coproductRightTerms (PLTree.coproductTermsList ts))) : (coproductLeftTerms (PLTree.node a ts).coproductTerms).Perm (coproductRightTerms (PLTree.node a ts).coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms_multiplyCoproductTerms_perm {α : Type u} (xs ys : List (LRootedForest α × LRootedForest α)) : (coproductLeftTerms (PLTree.multiplyCoproductTerms xs ys)).Perm (multiplyTerms (coproductLeftTerms xs) (coproductLeftTerms ys))

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms_multiplyCoproductTerms_perm {α : Type u} (xs ys : List (LRootedForest α × LRootedForest α)) : (coproductRightTerms (PLTree.multiplyCoproductTerms xs ys)).Perm (multiplyTerms (coproductRightTerms xs) (coproductRightTerms ys))

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms_perm {α : Type u} {xs ys : List (LRootedForest α × LRootedForest α)} (h : xs.Perm ys) : (coproductLeftTerms xs).Perm (coproductLeftTerms ys)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms_perm {α : Type u} {xs ys : List (LRootedForest α × LRootedForest α)} (h : xs.Perm ys) : (coproductRightTerms xs).Perm (coproductRightTerms ys)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms_lrootedForest_add_perm {α : Type u} (φ ψ : LRootedForest α) : (coproductLeftTerms (φ + ψ).coproductTerms).Perm (multiplyTerms (coproductLeftTerms φ.coproductTerms) (coproductLeftTerms ψ.coproductTerms))

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms_lrootedForest_add_perm {α : Type u} (φ ψ : LRootedForest α) : (coproductRightTerms (φ + ψ).coproductTerms).Perm (multiplyTerms (coproductRightTerms φ.coproductTerms) (coproductRightTerms ψ.coproductTerms))

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductTermsList_left_right_perm_of_coproductTerms_perm {α : Type u} (h : ∀ (t : PLTree α), (coproductLeftTerms t.coproductTerms).Perm (coproductRightTerms t.coproductTerms)) (ts : List (PLTree α)) : (coproductLeftTerms (PLTree.coproductTermsList ts)).Perm (coproductRightTerms (PLTree.coproductTermsList ts))

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductTerms_left_right_perm {α : Type u} (t : PLTree α) : (coproductLeftTerms t.coproductTerms).Perm (coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductTermsList_left_right_perm {α : Type u} (ts : List (PLTree α)) : (coproductLeftTerms (PLTree.coproductTermsList ts)).Perm (coproductRightTerms (PLTree.coproductTermsList ts))

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductTerms_lrootedForest_left_right_perm_of_coproductTerms_perm {α : Type u} (h : ∀ (t : PLTree α), (coproductLeftTerms t.coproductTerms).Perm (coproductRightTerms t.coproductTerms)) (φ : LRootedForest α) : (coproductLeftTerms φ.coproductTerms).Perm (coproductRightTerms φ.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerm_order {α : Type u} {term : LRootedForest α × LRootedForest α} {triple : LRootedForest α × LRootedForest α × LRootedForest α} (htriple : triple ∈ coproductLeftTerm term) : triple.1.order + triple.2.1.order + triple.2.2.order = term.1.order + term.2.order

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerm_order {α : Type u} {term : LRootedForest α × LRootedForest α} {triple : LRootedForest α × LRootedForest α × LRootedForest α} (htriple : triple ∈ coproductRightTerm term) : triple.1.order + triple.2.1.order + triple.2.2.order = term.1.order + term.2.order

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms_order {α : Type u} {terms : List (LRootedForest α × LRootedForest α)} {m : ℕ} (hterms : ∀ term ∈ terms, term.1.order + term.2.order = m) {triple : LRootedForest α × LRootedForest α × LRootedForest α} (htriple : triple ∈ coproductLeftTerms terms) : triple.1.order + triple.2.1.order + triple.2.2.order = m

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms_order {α : Type u} {terms : List (LRootedForest α × LRootedForest α)} {m : ℕ} (hterms : ∀ term ∈ terms, term.1.order + term.2.order = m) {triple : LRootedForest α × LRootedForest α × LRootedForest α} (htriple : triple ∈ coproductRightTerms terms) : triple.1.order + triple.2.1.order + triple.2.2.order = m

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms_rootedForest_order {α : Type u} {φ : LRootedForest α} {triple : LRootedForest α × LRootedForest α × LRootedForest α} (htriple : triple ∈ coproductLeftTerms φ.coproductTerms) : triple.1.order + triple.2.1.order + triple.2.2.order = φ.order

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms_rootedForest_order {α : Type u} {φ : LRootedForest α} {triple : LRootedForest α × LRootedForest α × LRootedForest α} (htriple : triple ∈ coproductRightTerms φ.coproductTerms) : triple.1.order + triple.2.1.order + triple.2.2.order = φ.order

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeftTerms_pltree_order {α : Type u} {t : PLTree α} {triple : LRootedForest α × LRootedForest α × LRootedForest α} (htriple : triple ∈ coproductLeftTerms t.coproductTerms) : triple.1.order + triple.2.1.order + triple.2.2.order = t.order

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRightTerms_pltree_order {α : Type u} {t : PLTree α} {triple : LRootedForest α × LRootedForest α × LRootedForest α} (htriple : triple ∈ coproductRightTerms t.coproductTerms) : triple.1.order + triple.2.1.order + triple.2.2.order = t.order

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_coproductLeftTerm {α : Type u} {R : Type v} [CommSemiring R] (term : LRootedForest α × LRootedForest α) : sumTerms (coproductLeftTerm term) = coproductLeft (LForestTensorAlgebra.ofPair term)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_coproductRightTerm {α : Type u} {R : Type v} [CommSemiring R] (term : LRootedForest α × LRootedForest α) : sumTerms (coproductRightTerm term) = coproductRight (LForestTensorAlgebra.ofPair term)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_coproductLeftTerms {α : Type u} {R : Type v} [CommSemiring R] (terms : List (LRootedForest α × LRootedForest α)) : sumTerms (coproductLeftTerms terms) = coproductLeft (LForestTensorAlgebra.sumTerms terms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_coproductRightTerms {α : Type u} {R : Type v} [CommSemiring R] (terms : List (LRootedForest α × LRootedForest α)) : sumTerms (coproductRightTerms terms) = coproductRight (LForestTensorAlgebra.sumTerms terms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeft_coproduct_eq_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : coproductLeft φ.coproduct = sumTerms (coproductLeftTerms φ.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRight_coproduct_eq_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : coproductRight φ.coproduct = sumTerms (coproductRightTerms φ.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductLeft_pltree_coproduct_eq_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : coproductLeft t.labelledCoproduct = sumTerms (coproductLeftTerms t.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductRight_pltree_coproduct_eq_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : coproductRight t.labelledCoproduct = sumTerms (coproductRightTerms t.coproductTerms)

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

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

theorem HopfAlgebras.LForestTripleTensorAlgebra.nestedCoproductLeftCuts_perm_coproductLeftTerms {α : Type u} (cuts : List (PLTree.Cut α)) : (List.flatMap (fun (c : PLTree.Cut α) => List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (PLTree.coproductTermsList c.pruned)) cuts).Perm (coproductLeftTerms (List.map (fun (c : PLTree.Cut α) => (c.prunedForest, c.trunkForest)) cuts))

theorem HopfAlgebras.LForestTripleTensorAlgebra.nestedCoproductRightCuts_perm_coproductRightTerms {α : Type u} (cuts : List (PLTree.Cut α)) : (List.flatMap (fun (c : PLTree.Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) cuts).Perm (coproductRightTerms (List.map (fun (c : PLTree.Cut α) => (c.prunedForest, c.trunkForest)) cuts))

theorem HopfAlgebras.LForestTripleTensorAlgebra.nestedCoproductLeftTerms_perm_coproductLeftTerms {α : Type u} (t : PLTree α) : t.nestedCoproductLeftTerms.Perm (coproductLeftTerms t.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.nestedCoproductRightTerms_perm_coproductRightTerms {α : Type u} (t : PLTree α) : t.nestedCoproductRightTerms.Perm (coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.nestedCoproductTerms_perm_iff_coproductTerms_perm {α : Type u} (t : PLTree α) : t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms ↔ (coproductLeftTerms t.coproductTerms).Perm (coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.nestedCoproductTerms_left_right_perm {α : Type u} (t : PLTree α) : t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms

theorem HopfAlgebras.LForestTripleTensorAlgebra.coproductTerms_lrootedForest_left_right_perm_of_nestedCoproductTerms_perm {α : Type u} (h : ∀ (t : PLTree α), t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms) (φ : LRootedForest α) : (coproductLeftTerms φ.coproductTerms).Perm (coproductRightTerms φ.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftCut {α : Type u} {R : Type v} [CommSemiring R] (c : PLTree.Cut α) : sumTerms (List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (PLTree.coproductTermsList c.pruned)) = coproductLeft (LForestTensorAlgebra.ofPair (c.prunedForest, c.trunkForest))

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_trunkCoproductTerms {α : Type u} {R : Type v} [CommSemiring R] (c : PLTree.Cut α) : c.trunkForest.coproduct = LForestTensorAlgebra.sumTerms c.trunkCoproductTerms

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductRightCut {α : Type u} {R : Type v} [CommSemiring R] (c : PLTree.Cut α) : sumTerms (List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) = coproductRight (LForestTensorAlgebra.ofPair (c.prunedForest, c.trunkForest))

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftCut_perm {α : Type u} {R : Type v} [CommSemiring R] {c d : PLTree.Cut α} (h : c.Perm d) : sumTerms (List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (PLTree.coproductTermsList c.pruned)) = sumTerms (List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, d.trunkForest)) (PLTree.coproductTermsList d.pruned))

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductRightCut_perm {α : Type u} {R : Type v} [CommSemiring R] {c d : PLTree.Cut α} (h : c.Perm d) : sumTerms (List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) = sumTerms (List.map (fun (right : LRootedForest α × LRootedForest α) => (d.prunedForest, right.1, right.2)) d.trunkCoproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftCuts {α : Type u} {R : Type v} [CommSemiring R] (cuts : List (PLTree.Cut α)) : sumTerms (List.flatMap (fun (c : PLTree.Cut α) => List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (PLTree.coproductTermsList c.pruned)) cuts) = coproductLeft (LForestTensorAlgebra.sumTerms (List.map (fun (c : PLTree.Cut α) => (c.prunedForest, c.trunkForest)) cuts))

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductRightCuts {α : Type u} {R : Type v} [CommSemiring R] (cuts : List (PLTree.Cut α)) : sumTerms (List.flatMap (fun (c : PLTree.Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) cuts) = coproductRight (LForestTensorAlgebra.sumTerms (List.map (fun (c : PLTree.Cut α) => (c.prunedForest, c.trunkForest)) cuts))

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

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductRightCuts_listRelPerm {α : Type u} {R : Type v} [CommSemiring R] {cs ds : List (PLTree.Cut α)} (h : PTree.ListRelPerm PLTree.Cut.Perm cs ds) : sumTerms (List.flatMap (fun (c : PLTree.Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) cs) = sumTerms (List.flatMap (fun (d : PLTree.Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (d.prunedForest, right.1, right.2)) d.trunkCoproductTerms) ds)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftCuts_forall₂_perm {α : Type u} {R : Type v} [CommSemiring R] {cs ds : List (PLTree.Cut α)} (h : List.Forall₂ PLTree.Cut.Perm cs ds) : sumTerms (List.flatMap (fun (c : PLTree.Cut α) => List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, c.trunkForest)) (PLTree.coproductTermsList c.pruned)) cs) = sumTerms (List.flatMap (fun (d : PLTree.Cut α) => List.map (fun (left : LRootedForest α × LRootedForest α) => (left.1, left.2, d.trunkForest)) (PLTree.coproductTermsList d.pruned)) ds)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductRightCuts_forall₂_perm {α : Type u} {R : Type v} [CommSemiring R] {cs ds : List (PLTree.Cut α)} (h : List.Forall₂ PLTree.Cut.Perm cs ds) : sumTerms (List.flatMap (fun (c : PLTree.Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) cs) = sumTerms (List.flatMap (fun (d : PLTree.Cut α) => List.map (fun (right : LRootedForest α × LRootedForest α) => (d.prunedForest, right.1, right.2)) d.trunkCoproductTerms) ds)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftTerms {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : sumTerms t.nestedCoproductLeftTerms = sumTerms (coproductLeftTerms t.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductRightTerms {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : sumTerms t.nestedCoproductRightTerms = sumTerms (coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftTerms_listRelPerm {α : Type u} {R : Type v} [CommSemiring R] {t u : PLTree α} (h : PTree.ListRelPerm PLTree.Cut.Perm t.cuts u.cuts) : sumTerms t.nestedCoproductLeftTerms = sumTerms u.nestedCoproductLeftTerms

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductRightTerms_listRelPerm {α : Type u} {R : Type v} [CommSemiring R] {t u : PLTree α} (h : PTree.ListRelPerm PLTree.Cut.Perm t.cuts u.cuts) : sumTerms t.nestedCoproductRightTerms = sumTerms u.nestedCoproductRightTerms

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftTerms_perm {α : Type u} {R : Type v} [CommSemiring R] {t u : PLTree α} (h : t.Perm u) : sumTerms t.nestedCoproductLeftTerms = sumTerms u.nestedCoproductLeftTerms

theorem HopfAlgebras.LForestTripleTensorAlgebra.sumTerms_nestedCoproductRightTerms_perm {α : Type u} {R : Type v} [CommSemiring R] {t u : PLTree α} (h : t.Perm u) : sumTerms t.nestedCoproductRightTerms = sumTerms u.nestedCoproductRightTerms

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_coproductLeft {α : Type u} {R : Type v} [CommSemiring R] (x : LForestTensorAlgebra α R) : (coproductLeft x).erase = ForestTripleTensorAlgebra.coproductLeft x.erase

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_coproductRight {α : Type u} {R : Type v} [CommSemiring R] (x : LForestTensorAlgebra α R) : (coproductRight x).erase = ForestTripleTensorAlgebra.coproductRight x.erase

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_coproductLeft {α : Type u} {R : Type v} [CommSemiring R] (a : α) (x : ForestTensorAlgebra R) : constLabel a (ForestTripleTensorAlgebra.coproductLeft x) = coproductLeft (LForestTensorAlgebra.constLabel a x)

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_coproductRight {α : Type u} {R : Type v} [CommSemiring R] (a : α) (x : ForestTensorAlgebra R) : constLabel a (ForestTripleTensorAlgebra.coproductRight x) = coproductRight (LForestTensorAlgebra.constLabel a x)

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_coproductLeft {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (x : LForestTensorAlgebra α R) : mapLabels f (coproductLeft x) = coproductLeft (LForestTensorAlgebra.mapLabels f x)

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_coproductRight {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (x : LForestTensorAlgebra α R) : mapLabels f (coproductRight x) = coproductRight (LForestTensorAlgebra.mapLabels f x)

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_sumTerms_coproductLeftTerms_pltree {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : (sumTerms (coproductLeftTerms t.coproductTerms)).erase = ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductLeftTerms t.erase.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_sumTerms_coproductRightTerms_pltree {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : (sumTerms (coproductRightTerms t.coproductTerms)).erase = ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductRightTerms t.erase.coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_sumTerms_nestedCoproductLeftTerms_pltree {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : (sumTerms t.nestedCoproductLeftTerms).erase = ForestTripleTensorAlgebra.sumTerms t.erase.nestedCoproductLeftTerms

theorem HopfAlgebras.LForestTripleTensorAlgebra.erase_sumTerms_nestedCoproductRightTerms_pltree {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : (sumTerms t.nestedCoproductRightTerms).erase = ForestTripleTensorAlgebra.sumTerms t.erase.nestedCoproductRightTerms

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_sumTerms_coproductLeftTerms_ptree {α : Type u} {R : Type v} [CommSemiring R] (a : α) (t : PTree) : constLabel a (ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms)) = sumTerms (coproductLeftTerms (PLTree.constLabel a t).coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.constLabel_sumTerms_coproductRightTerms_ptree {α : Type u} {R : Type v} [CommSemiring R] (a : α) (t : PTree) : constLabel a (ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)) = sumTerms (coproductRightTerms (PLTree.constLabel a t).coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_sumTerms_coproductLeftTerms_pltree {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (t : PLTree α) : mapLabels f (sumTerms (coproductLeftTerms t.coproductTerms)) = sumTerms (coproductLeftTerms (PLTree.map f t).coproductTerms)

theorem HopfAlgebras.LForestTripleTensorAlgebra.mapLabels_sumTerms_coproductRightTerms_pltree {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (t : PLTree α) : mapLabels f (sumTerms (coproductRightTerms t.coproductTerms)) = sumTerms (coproductRightTerms (PLTree.map f t).coproductTerms)

noncomputable def HopfAlgebras.LRootedTree.coproduct {α : Type u} {R : Type v} [Semiring R] (τ : LRootedTree α) : LForestTensorAlgebra α R

The BCK coproduct of a non-planar labelled rooted tree.

Equations

• τ.coproduct = Quotient.lift HopfAlgebras.PLTree.labelledCoproduct ⋯ τ

@[simp]

theorem HopfAlgebras.LRootedTree.coproduct_ofPLTree {α : Type u} {R : Type v} [Semiring R] (t : PLTree α) : (ofPLTree t).coproduct = t.labelledCoproduct

theorem HopfAlgebras.LRootedTree.coproduct_out {α : Type u} {R : Type v} [Semiring R] (τ : LRootedTree α) : τ.coproduct = (Quotient.out τ).labelledCoproduct

theorem HopfAlgebras.LRootedTree.coproduct_graft_coe {α : Type u} {R : Type v} [Semiring R] (a : α) (ts : List (LRootedTree α)) : (LRootedForest.graft a ↑ts).coproduct = LForestTensorAlgebra.sumTerms (List.map (fun (term : LRootedForest α × LRootedForest α) => (term.1, LRootedForest.singleton (LRootedForest.graft a term.2))) (PLTree.coproductTermsList (List.map Quotient.out ts))) + LForestTensorAlgebra.ofPair (LRootedForest.singleton (LRootedForest.graft a ↑ts), 0)

noncomputable def HopfAlgebras.LRootedTree.reducedCoproduct {α : Type u} {R : Type v} [Semiring R] (τ : LRootedTree α) : LForestTensorAlgebra α R

The reduced BCK coproduct of a non-planar labelled rooted tree.

Equations

• τ.reducedCoproduct = Quotient.lift HopfAlgebras.PLTree.labelledReducedCoproduct ⋯ τ

@[simp]

theorem HopfAlgebras.LRootedTree.reducedCoproduct_ofPLTree {α : Type u} {R : Type v} [Semiring R] (t : PLTree α) : (ofPLTree t).reducedCoproduct = t.labelledReducedCoproduct

theorem HopfAlgebras.LRootedTree.reducedCoproduct_out {α : Type u} {R : Type v} [Semiring R] (τ : LRootedTree α) : τ.reducedCoproduct = (Quotient.out τ).labelledReducedCoproduct

theorem HopfAlgebras.LRootedTree.erase_reducedCoproduct {α : Type u} {R : Type v} [CommSemiring R] (τ : LRootedTree α) : τ.reducedCoproduct.erase = τ.erase.reducedCoproduct

theorem HopfAlgebras.LRootedTree.coproduct_eq_forest_singleton {α : Type u} {R : Type v} [CommSemiring R] (τ : LRootedTree α) : τ.coproduct = (LRootedForest.singleton τ).coproduct

theorem HopfAlgebras.LRootedTree.erase_coproduct {α : Type u} {R : Type v} [CommSemiring R] (τ : LRootedTree α) : τ.coproduct.erase = τ.erase.coproduct

theorem HopfAlgebras.LRootedTree.mapLabels_coproduct {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (τ : LRootedTree α) : LForestTensorAlgebra.mapLabels f τ.coproduct = (map f τ).coproduct

theorem HopfAlgebras.LRootedTree.constLabel_coproduct {α : Type u} {R : Type v} [CommSemiring R] (a : α) (τ : RootedTree) : LForestTensorAlgebra.constLabel a τ.coproduct = (constLabel a τ).coproduct

noncomputable def HopfAlgebras.LForestAlgebra.coproduct (α : Type u) (R : Type v) [CommSemiring R] : LForestAlgebra α R →ₐ[R] LForestTensorAlgebra α R

The labelled BCK coproduct as an algebra morphism on the labelled forest algebra.

Equations

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

noncomputable def HopfAlgebras.LForestAlgebra.coproductLeft (α : Type u) (R : Type v) [CommSemiring R] : LForestAlgebra α R →ₐ[R] LForestTripleTensorAlgebra α R

The iterated labelled coproduct (Δ ⊗ id) ∘ Δ.

Equations

• HopfAlgebras.LForestAlgebra.coproductLeft α R = HopfAlgebras.LForestTripleTensorAlgebra.coproductLeft.comp (HopfAlgebras.LForestAlgebra.coproduct α R)

noncomputable def HopfAlgebras.LForestAlgebra.coproductRight (α : Type u) (R : Type v) [CommSemiring R] : LForestAlgebra α R →ₐ[R] LForestTripleTensorAlgebra α R

The iterated labelled coproduct (id ⊗ Δ) ∘ Δ.

Equations

• HopfAlgebras.LForestAlgebra.coproductRight α R = HopfAlgebras.LForestTripleTensorAlgebra.coproductRight.comp (HopfAlgebras.LForestAlgebra.coproduct α R)

@[simp]

theorem HopfAlgebras.LForestAlgebra.coproduct_ofForest {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : (coproduct α R) (ofForest φ) = φ.coproduct

@[simp]

theorem HopfAlgebras.LForestAlgebra.coproductLeft_ofForest {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : (coproductLeft α R) (ofForest φ) = LForestTripleTensorAlgebra.coproductLeft φ.coproduct

@[simp]

theorem HopfAlgebras.LForestAlgebra.coproductRight_ofForest {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : (coproductRight α R) (ofForest φ) = LForestTripleTensorAlgebra.coproductRight φ.coproduct

@[simp]

theorem HopfAlgebras.LForestAlgebra.coproduct_ofForest_zero {α : Type u} {R : Type v} [CommSemiring R] : (coproduct α R) (ofForest 0) = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.coproduct_ofForest_empty {α : Type u} {R : Type v} [CommSemiring R] : (coproduct α R) (ofForest LRootedForest.empty) = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.coproduct_ofForest_singleton {α : Type u} {R : Type v} [CommSemiring R] (τ : LRootedTree α) : (coproduct α R) (ofForest (LRootedForest.singleton τ)) = (Quotient.out τ).labelledCoproduct

theorem HopfAlgebras.LForestAlgebra.coproduct_ofForest_singleton_tree {α : Type u} {R : Type v} [CommSemiring R] (τ : LRootedTree α) : (coproduct α R) (ofForest (LRootedForest.singleton τ)) = τ.coproduct

theorem HopfAlgebras.LForestAlgebra.coproductLeft_ofForest_singleton_ofPLTree_eq_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : (coproductLeft α R) (ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t))) = LForestTripleTensorAlgebra.sumTerms (LForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms)

theorem HopfAlgebras.LForestAlgebra.coproductRight_ofForest_singleton_ofPLTree_eq_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (t : PLTree α) : (coproductRight α R) (ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t))) = LForestTripleTensorAlgebra.sumTerms (LForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.LForestAlgebra.erase_coproduct_ofForest {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : ((coproduct α R) (ofForest φ)).erase = (ForestAlgebra.coproduct R) (ForestAlgebra.ofForest φ.erase)

theorem HopfAlgebras.LForestAlgebra.constLabel_coproduct_ofForest {α : Type u} {R : Type v} [CommSemiring R] (a : α) (φ : RootedForest) : LForestTensorAlgebra.constLabel a ((ForestAlgebra.coproduct R) (ForestAlgebra.ofForest φ)) = (coproduct α R) ((constLabel a R) (ForestAlgebra.ofForest φ))

theorem HopfAlgebras.LForestAlgebra.eraseLabels_coproduct {α : Type u} {R : Type v} [CommSemiring R] (x : LForestAlgebra α R) : ((coproduct α R) x).erase = (ForestAlgebra.coproduct R) ((eraseLabels R) x)

theorem HopfAlgebras.LForestAlgebra.constLabel_coproduct {α : Type u} {R : Type v} [CommSemiring R] (a : α) (x : ForestAlgebra R) : LForestTensorAlgebra.constLabel a ((ForestAlgebra.coproduct R) x) = (coproduct α R) ((constLabel a R) x)

theorem HopfAlgebras.LForestAlgebra.mapLabels_coproduct {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (x : LForestAlgebra α R) : LForestTensorAlgebra.mapLabels f ((coproduct α R) x) = (coproduct β R) ((mapLabels R f) x)

theorem HopfAlgebras.LForestAlgebra.eraseLabels_coproductLeft {α : Type u} {R : Type v} [CommSemiring R] (x : LForestAlgebra α R) : ((coproductLeft α R) x).erase = (ForestAlgebra.coproductLeft R) ((eraseLabels R) x)

theorem HopfAlgebras.LForestAlgebra.eraseLabels_coproductRight {α : Type u} {R : Type v} [CommSemiring R] (x : LForestAlgebra α R) : ((coproductRight α R) x).erase = (ForestAlgebra.coproductRight R) ((eraseLabels R) x)

theorem HopfAlgebras.LForestAlgebra.constLabel_coproductLeft {α : Type u} {R : Type v} [CommSemiring R] (a : α) (x : ForestAlgebra R) : LForestTripleTensorAlgebra.constLabel a ((ForestAlgebra.coproductLeft R) x) = (coproductLeft α R) ((constLabel a R) x)

theorem HopfAlgebras.LForestAlgebra.constLabel_coproductRight {α : Type u} {R : Type v} [CommSemiring R] (a : α) (x : ForestAlgebra R) : LForestTripleTensorAlgebra.constLabel a ((ForestAlgebra.coproductRight R) x) = (coproductRight α R) ((constLabel a R) x)

theorem HopfAlgebras.LForestAlgebra.mapLabels_coproductLeft {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (x : LForestAlgebra α R) : LForestTripleTensorAlgebra.mapLabels f ((coproductLeft α R) x) = (coproductLeft β R) ((mapLabels R f) x)

theorem HopfAlgebras.LForestAlgebra.mapLabels_coproductRight {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (x : LForestAlgebra α R) : LForestTripleTensorAlgebra.mapLabels f ((coproductRight α R) x) = (coproductRight β R) ((mapLabels R f) x)

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_of_singletons {α : Type u} {R : Type v} [CommSemiring R] (h : ∀ (τ : LRootedTree α), (coproductLeft α R) (ofForest (LRootedForest.singleton τ)) = (coproductRight α R) (ofForest (LRootedForest.singleton τ))) : coproductLeft α R = coproductRight α R

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_iff_singletons {α : Type u} {R : Type v} [CommSemiring R] : coproductLeft α R = coproductRight α R ↔ ∀ (τ : LRootedTree α), (coproductLeft α R) (ofForest (LRootedForest.singleton τ)) = (coproductRight α R) (ofForest (LRootedForest.singleton τ))

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_of_pltree_singletons {α : Type u} {R : Type v} [CommSemiring R] (h : ∀ (t : PLTree α), (coproductLeft α R) (ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t))) = (coproductRight α R) (ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t)))) : coproductLeft α R = coproductRight α R

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_iff_pltree_singletons {α : Type u} {R : Type v} [CommSemiring R] : coproductLeft α R = coproductRight α R ↔ ∀ (t : PLTree α), (coproductLeft α R) (ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t))) = (coproductRight α R) (ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t)))

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_of_pltree_coproductTerms {α : Type u} {R : Type v} [CommSemiring R] (h : ∀ (t : PLTree α), LForestTripleTensorAlgebra.sumTerms (LForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms) = LForestTripleTensorAlgebra.sumTerms (LForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)) : coproductLeft α R = coproductRight α R

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_iff_pltree_coproductTerms {α : Type u} {R : Type v} [CommSemiring R] : coproductLeft α R = coproductRight α R ↔ ∀ (t : PLTree α), LForestTripleTensorAlgebra.sumTerms (LForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms) = LForestTripleTensorAlgebra.sumTerms (LForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_of_nestedCoproductTerms {α : Type u} {R : Type v} [CommSemiring R] (h : ∀ (t : PLTree α), LForestTripleTensorAlgebra.sumTerms t.nestedCoproductLeftTerms = LForestTripleTensorAlgebra.sumTerms t.nestedCoproductRightTerms) : coproductLeft α R = coproductRight α R

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_iff_nestedCoproductTerms {α : Type u} {R : Type v} [CommSemiring R] : coproductLeft α R = coproductRight α R ↔ ∀ (t : PLTree α), LForestTripleTensorAlgebra.sumTerms t.nestedCoproductLeftTerms = LForestTripleTensorAlgebra.sumTerms t.nestedCoproductRightTerms

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_of_nestedCoproductTerms_perm {α : Type u} {R : Type v} [CommSemiring R] (h : ∀ (t : PLTree α), t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms) : coproductLeft α R = coproductRight α R

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_of_pltree_coproductTerms_perm {α : Type u} {R : Type v} [CommSemiring R] (h : ∀ (t : PLTree α), (LForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms).Perm (LForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)) : coproductLeft α R = coproductRight α R

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight_of_lrootedForest_coproductTerms_perm {α : Type u} {R : Type v} [CommSemiring R] (h : ∀ (φ : LRootedForest α), (LForestTripleTensorAlgebra.coproductLeftTerms φ.coproductTerms).Perm (LForestTripleTensorAlgebra.coproductRightTerms φ.coproductTerms)) : coproductLeft α R = coproductRight α R

theorem HopfAlgebras.LForestAlgebra.coproductLeft_eq_coproductRight {α : Type u} {R : Type v} [CommSemiring R] : coproductLeft α R = coproductRight α R

theorem HopfAlgebras.LForestAlgebra.counitLeft_coproduct {α : Type u} {R : Type v} [CommSemiring R] : LForestTensorAlgebra.counitLeft.comp (coproduct α R) = AlgHom.id R (LForestAlgebra α R)

theorem HopfAlgebras.LForestAlgebra.counitRight_coproduct {α : Type u} {R : Type v} [CommSemiring R] : LForestTensorAlgebra.counitRight.comp (coproduct α R) = AlgHom.id R (LForestAlgebra α R)