Coproduct Terms in the Forest Algebra

This file turns the finite cut-term lists from HopfAlgebras.Cuts.Rooted into elements of the monoid algebra on pairs of rooted forests. This is a tensor-coded target for the BCK coproduct: a pair (φ, ψ) represents the basis tensor φ ⊗ ψ.

The tree coproduct is first defined for planar representatives, then quotiented to non-planar rooted trees and forests.

Main definitions

• ForestTensorAlgebra - monoid algebra on pairs of rooted forests
• ForestTensorAlgebra.ofForests - basis tensor represented by a pair
• ForestTensorAlgebra.sumTerms - finite sum of basis tensors
• PTree.coproduct - planar tree coproduct as a finite algebra element
• PTree.coproductList - multiplicative extension to planar forests
• RootedTree.coproduct - non-planar tree coproduct
• RootedForest.coproduct - multiplicative extension to non-planar forests

References

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

@[reducible, inline]

abbrev HopfAlgebras.ForestTensorAlgebra (R : Type u) [Semiring R] : Type u

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

Equations

• HopfAlgebras.ForestTensorAlgebra R = AddMonoidAlgebra R (HopfAlgebras.RootedForest × HopfAlgebras.RootedForest)

noncomputable def HopfAlgebras.ForestTensorAlgebra.ofPair {R : Type u} [Semiring R] (term : RootedForest × RootedForest) : ForestTensorAlgebra R

The basis tensor represented by a pair of rooted forests.

Equations

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

noncomputable def HopfAlgebras.ForestTensorAlgebra.ofForests {R : Type u} [Semiring R] (φ ψ : RootedForest) : ForestTensorAlgebra R

The basis tensor φ ⊗ ψ.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.ofPair_add {R : Type u} [Semiring R] (x y : RootedForest × RootedForest) : ofPair (x + y) = ofPair x * ofPair y

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.ofForests_add {R : Type u} [Semiring R] (φ₁ φ₂ ψ₁ ψ₂ : RootedForest) : ofForests (φ₁ + φ₂) (ψ₁ + ψ₂) = ofForests φ₁ ψ₁ * ofForests φ₂ ψ₂

noncomputable def HopfAlgebras.ForestTensorAlgebra.sumTerms {R : Type u} [Semiring R] (terms : List (RootedForest × RootedForest)) : ForestTensorAlgebra R

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

Equations

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

@[simp]

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

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.sumTerms_cons {R : Type u} [Semiring R] (term : RootedForest × RootedForest) (terms : List (RootedForest × RootedForest)) : sumTerms (term :: terms) = ofPair term + sumTerms terms

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.sumTerms_singleton {R : Type u} [Semiring R] (term : RootedForest × RootedForest) : sumTerms [term] = ofPair term

theorem HopfAlgebras.ForestTensorAlgebra.sumTerms_append {R : Type u} [Semiring R] (xs ys : List (RootedForest × RootedForest)) : sumTerms (xs ++ ys) = sumTerms xs + sumTerms ys

theorem HopfAlgebras.ForestTensorAlgebra.sumTerms_perm {R : Type u} [Semiring R] {xs ys : List (RootedForest × RootedForest)} (h : xs.Perm ys) : sumTerms xs = sumTerms ys

theorem HopfAlgebras.ForestTensorAlgebra.sumTerms_eq_of_forall₂_eq {R : Type u} [Semiring R] {xs ys : List (RootedForest × RootedForest)} : List.Forall₂ (fun (x y : RootedForest × RootedForest) => x = y) xs ys → sumTerms xs = sumTerms ys

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

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

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

theorem HopfAlgebras.ForestTensorAlgebra.sumTerms_multiply {R : Type u} [Semiring R] (xs ys : List (RootedForest × RootedForest)) : sumTerms (PTree.multiplyCoproductTerms xs ys) = sumTerms xs * sumTerms ys

noncomputable def HopfAlgebras.ForestTensorAlgebra.counitLeft {R : Type u} [CommSemiring R] : ForestTensorAlgebra R →ₐ[R] ForestAlgebra R

Apply the counit to the left tensor factor.

Equations

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

noncomputable def HopfAlgebras.ForestTensorAlgebra.counitRight {R : Type u} [CommSemiring R] : ForestTensorAlgebra R →ₐ[R] ForestAlgebra R

Apply the counit to the right tensor factor.

Equations

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

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.counitLeft_ofPair {R : Type u} [CommSemiring R] (term : RootedForest × RootedForest) : counitLeft (ofPair term) = ForestAlgebra.counitCoeff term.1 • ForestAlgebra.ofForest term.2

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.counitRight_ofPair {R : Type u} [CommSemiring R] (term : RootedForest × RootedForest) : counitRight (ofPair term) = ForestAlgebra.counitCoeff term.2 • ForestAlgebra.ofForest term.1

theorem HopfAlgebras.ForestTensorAlgebra.counitLeft_sumTerms {R : Type u} [CommSemiring R] (terms : List (RootedForest × RootedForest)) : counitLeft (sumTerms terms) = (List.map (fun (term : RootedForest × RootedForest) => ForestAlgebra.counitCoeff term.1 • ForestAlgebra.ofForest term.2) terms).sum

theorem HopfAlgebras.ForestTensorAlgebra.counitRight_sumTerms {R : Type u} [CommSemiring R] (terms : List (RootedForest × RootedForest)) : counitRight (sumTerms terms) = (List.map (fun (term : RootedForest × RootedForest) => ForestAlgebra.counitCoeff term.2 • ForestAlgebra.ofForest term.1) terms).sum

@[reducible, inline]

abbrev HopfAlgebras.ForestTripleTensorAlgebra (R : Type u) [Semiring R] : Type u

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

Equations

• HopfAlgebras.ForestTripleTensorAlgebra R = AddMonoidAlgebra R (HopfAlgebras.RootedForest × HopfAlgebras.RootedForest × HopfAlgebras.RootedForest)

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.ofTriple {R : Type u} [Semiring R] (term : RootedForest × RootedForest × RootedForest) : ForestTripleTensorAlgebra R

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

Equations

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

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.ofForests {R : Type u} [Semiring R] (φ ψ η : RootedForest) : ForestTripleTensorAlgebra R

The basis tensor φ ⊗ ψ ⊗ η.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.ofTriple_add {R : Type u} [Semiring R] (x y : RootedForest × RootedForest × RootedForest) : ofTriple (x + y) = ofTriple x * ofTriple y

@[simp]

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

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.sumTerms {R : Type u} [Semiring R] (terms : List (RootedForest × RootedForest × RootedForest)) : ForestTripleTensorAlgebra R

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

Equations

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

@[simp]

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

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_cons {R : Type u} [Semiring R] (term : RootedForest × RootedForest × RootedForest) (terms : List (RootedForest × RootedForest × RootedForest)) : sumTerms (term :: terms) = ofTriple term + sumTerms terms

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_singleton {R : Type u} [Semiring R] (term : RootedForest × RootedForest × RootedForest) : sumTerms [term] = ofTriple term

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_append {R : Type u} [Semiring R] (xs ys : List (RootedForest × RootedForest × RootedForest)) : sumTerms (xs ++ ys) = sumTerms xs + sumTerms ys

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_perm {R : Type u} [Semiring R] {xs ys : List (RootedForest × RootedForest × RootedForest)} (h : xs.Perm ys) : sumTerms xs = sumTerms ys

def HopfAlgebras.ForestTripleTensorAlgebra.multiplyTerms (xs ys : List (RootedForest × RootedForest × RootedForest)) : List (RootedForest × RootedForest × RootedForest)

Multiply two finite lists of triple tensor basis terms.

Equations

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

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

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_multiply {R : Type u} [Semiring R] (xs ys : List (RootedForest × RootedForest × RootedForest)) : sumTerms (multiplyTerms xs ys) = sumTerms xs * sumTerms ys

theorem HopfAlgebras.ForestTripleTensorAlgebra.multiplyTerms_append_left (xs ys zs : List (RootedForest × RootedForest × RootedForest)) : multiplyTerms (xs ++ ys) zs = multiplyTerms xs zs ++ multiplyTerms ys zs

theorem HopfAlgebras.ForestTripleTensorAlgebra.multiplyTerms_perm_left {xs ys zs : List (RootedForest × RootedForest × RootedForest)} (h : xs.Perm ys) : (multiplyTerms xs zs).Perm (multiplyTerms ys zs)

theorem HopfAlgebras.ForestTripleTensorAlgebra.multiplyTerms_perm_right {xs ys zs : List (RootedForest × RootedForest × RootedForest)} (h : ys.Perm zs) : (multiplyTerms xs ys).Perm (multiplyTerms xs zs)

theorem HopfAlgebras.ForestTripleTensorAlgebra.multiplyTerms_perm {xs xs' ys ys' : List (RootedForest × RootedForest × RootedForest)} (hxs : xs.Perm xs') (hys : ys.Perm ys') : (multiplyTerms xs ys).Perm (multiplyTerms xs' ys')

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

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.includeLeftPair {R : Type u} [CommSemiring R] : ForestTensorAlgebra R →ₐ[R] ForestTripleTensorAlgebra R

Embed a 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.ForestTripleTensorAlgebra.includeLeftPair_ofPair {R : Type u} [CommSemiring R] (term : RootedForest × RootedForest) : includeLeftPair (ForestTensorAlgebra.ofPair term) = ofTriple (term.1, term.2, 0)

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.includeLeftPair_ofForests {R : Type u} [CommSemiring R] (φ ψ : RootedForest) : includeLeftPair (ForestTensorAlgebra.ofForests φ ψ) = ofForests φ ψ 0

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.includeRightPair {R : Type u} [CommSemiring R] : ForestTensorAlgebra R →ₐ[R] ForestTripleTensorAlgebra R

Embed a 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.ForestTripleTensorAlgebra.includeRightPair_ofPair {R : Type u} [CommSemiring R] (term : RootedForest × RootedForest) : includeRightPair (ForestTensorAlgebra.ofPair term) = ofTriple (0, term.1, term.2)

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.includeRightPair_ofForests {R : Type u} [CommSemiring R] (φ ψ : RootedForest) : includeRightPair (ForestTensorAlgebra.ofForests φ ψ) = ofForests 0 φ ψ

noncomputable def HopfAlgebras.PTree.coproduct {R : Type u} [Semiring R] (t : PTree) : ForestTensorAlgebra R

The planar BCK coproduct of a tree, represented in the tensor-coded algebra.

Equations

• t.coproduct = HopfAlgebras.ForestTensorAlgebra.sumTerms t.coproductTerms

noncomputable def HopfAlgebras.PTree.reducedCoproduct {R : Type u} [Semiring R] (t : PTree) : ForestTensorAlgebra R

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

Equations

• t.reducedCoproduct = HopfAlgebras.ForestTensorAlgebra.sumTerms t.properCoproductTerms

@[simp]

theorem HopfAlgebras.PTree.reducedCoproduct_bullet {R : Type u} [Semiring R] : bullet.reducedCoproduct = 0

theorem HopfAlgebras.PTree.reducedCoproduct_perm {R : Type u} [Semiring R] {t u : PTree} (h : t.Perm u) : t.reducedCoproduct = u.reducedCoproduct

theorem HopfAlgebras.PTree.coproduct_eq_of_cuts_listRelPerm {R : Type u} [Semiring R] {t u : PTree} (h : ListRelPerm Cut.Perm t.cuts u.cuts) : t.coproduct = u.coproduct

theorem HopfAlgebras.PTree.coproduct_perm {R : Type u} [Semiring R] {t u : PTree} (h : t.Perm u) : t.coproduct = u.coproduct

theorem HopfAlgebras.PTree.coproduct_node {R : Type u} [Semiring R] (ts : List PTree) : (node ts).coproduct = ForestTensorAlgebra.sumTerms (List.map (fun (term : RootedForest × RootedForest) => (term.1, RootedForest.singleton term.2.graft)) (coproductTermsList ts)) + ForestTensorAlgebra.ofPair (RootedForest.singleton (RootedTree.ofPTree (node ts)), 0)

noncomputable def HopfAlgebras.PTree.coproductList {R : Type u} [Semiring R] (ts : List PTree) : ForestTensorAlgebra R

Multiplicative extension of the planar coproduct to planar forests.

Equations

• HopfAlgebras.PTree.coproductList ts = HopfAlgebras.ForestTensorAlgebra.sumTerms (HopfAlgebras.PTree.coproductTermsList ts)

noncomputable def HopfAlgebras.PTree.reducedCoproductList {R : Type u} [Semiring R] (ts : List PTree) : ForestTensorAlgebra R

The reduced planar BCK coproduct of a planar forest.

Equations

• HopfAlgebras.PTree.reducedCoproductList ts = HopfAlgebras.ForestTensorAlgebra.sumTerms (HopfAlgebras.PTree.properCoproductTermsList ts)

@[simp]

theorem HopfAlgebras.PTree.reducedCoproductList_nil {R : Type u} [Semiring R] : reducedCoproductList [] = 0

theorem HopfAlgebras.PTree.reducedCoproductList_forall₂_perm {R : Type u} [Semiring R] {ts us : List PTree} (h : List.Forall₂ Perm ts us) : reducedCoproductList ts = reducedCoproductList us

@[simp]

theorem HopfAlgebras.PTree.coproductList_nil {R : Type u} [Semiring R] : coproductList [] = 1

@[simp]

theorem HopfAlgebras.PTree.coproductList_cons {R : Type u} [Semiring R] (t : PTree) (ts : List PTree) : coproductList (t :: ts) = t.coproduct * coproductList ts

@[simp]

theorem HopfAlgebras.PTree.coproductList_singleton {R : Type u} [Semiring R] (t : PTree) : coproductList [t] = t.coproduct

theorem HopfAlgebras.PTree.coproductList_forall₂_perm {R : Type u} [Semiring R] {ts us : List PTree} : List.Forall₂ Perm ts us → coproductList ts = coproductList us

theorem HopfAlgebras.PTree.coproductList_append {R : Type u} [Semiring R] (ts us : List PTree) : coproductList (ts ++ us) = coproductList ts * coproductList us

theorem HopfAlgebras.PTree.coproductList_perm {R : Type u} [CommSemiring R] {ts us : List PTree} (h : ts.Perm us) : coproductList ts = coproductList us

theorem HopfAlgebras.PTree.counitLeft_coproduct {R : Type u} [CommSemiring R] (t : PTree) : ForestTensorAlgebra.counitLeft t.coproduct = ForestAlgebra.ofForest (RootedForest.singleton (RootedTree.ofPTree t))

theorem HopfAlgebras.PTree.counitRight_coproduct {R : Type u} [CommSemiring R] (t : PTree) : ForestTensorAlgebra.counitRight t.coproduct = ForestAlgebra.ofForest (RootedForest.singleton (RootedTree.ofPTree t))

noncomputable def HopfAlgebras.RootedTree.coproduct {R : Type u} [Semiring R] (τ : RootedTree) : ForestTensorAlgebra R

The BCK coproduct of a non-planar rooted tree.

Equations

• τ.coproduct = Quotient.lift HopfAlgebras.PTree.coproduct ⋯ τ

@[simp]

theorem HopfAlgebras.RootedTree.coproduct_ofPTree {R : Type u} [Semiring R] (t : PTree) : (ofPTree t).coproduct = t.coproduct

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

theorem HopfAlgebras.RootedTree.coproduct_graft_coe {R : Type u} [Semiring R] (ts : List RootedTree) : (RootedForest.graft ↑ts).coproduct = ForestTensorAlgebra.sumTerms (List.map (fun (term : RootedForest × RootedForest) => (term.1, RootedForest.singleton term.2.graft)) (PTree.coproductTermsList (List.map Quotient.out ts))) + ForestTensorAlgebra.ofPair (RootedForest.singleton (RootedForest.graft ↑ts), 0)

noncomputable def HopfAlgebras.RootedTree.reducedCoproduct {R : Type u} [Semiring R] (τ : RootedTree) : ForestTensorAlgebra R

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

Equations

• τ.reducedCoproduct = Quotient.lift HopfAlgebras.PTree.reducedCoproduct ⋯ τ

@[simp]

theorem HopfAlgebras.RootedTree.reducedCoproduct_ofPTree {R : Type u} [Semiring R] (t : PTree) : (ofPTree t).reducedCoproduct = t.reducedCoproduct

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

@[simp]

theorem HopfAlgebras.RootedTree.reducedCoproduct_bullet {R : Type u} [Semiring R] : bullet.reducedCoproduct = 0

theorem HopfAlgebras.RootedForest.coproductTermsList_out_order {ts : List RootedTree} {term : RootedForest × RootedForest} (hterm : term ∈ PTree.coproductTermsList (List.map Quotient.out ts)) : term.1.order + term.2.order = order ↑ts

noncomputable def HopfAlgebras.RootedForest.coproductTerms (φ : RootedForest) : List (RootedForest × RootedForest)

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

Equations

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

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

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

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

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

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

theorem HopfAlgebras.RootedForest.coproductTerms_leftBoundaryCoproductTerm (φ : RootedForest) : List.filterMap PTree.leftBoundaryCoproductTerm? φ.coproductTerms = [(0, φ)]

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

theorem HopfAlgebras.RootedForest.coproductTerms_rightBoundaryCoproductTerm (φ : RootedForest) : List.filterMap PTree.rightBoundaryCoproductTerm? φ.coproductTerms = [(φ, 0)]

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

theorem HopfAlgebras.RootedForest.coproductTerms_ofPTree_list_perm (ts : List PTree) : (coproductTerms ↑(List.map RootedTree.ofPTree ts)).Perm (PTree.coproductTermsList ts)

theorem HopfAlgebras.RootedForest.coproductTerms_singleton_ofPTree_perm (t : PTree) : (singleton (RootedTree.ofPTree t)).coproductTerms.Perm t.coproductTerms

theorem HopfAlgebras.RootedForest.coproductTerms_singleton_graft_perm (φ : RootedForest) : (singleton φ.graft).coproductTerms.Perm (List.map (fun (term : RootedForest × RootedForest) => (term.1, singleton term.2.graft)) φ.coproductTerms ++ [(singleton φ.graft, 0)])

theorem HopfAlgebras.RootedForest.coproductTerms_add_perm (φ ψ : RootedForest) : (φ + ψ).coproductTerms.Perm (PTree.multiplyCoproductTerms φ.coproductTerms ψ.coproductTerms)

noncomputable def HopfAlgebras.RootedForest.properCoproductTerms (φ : RootedForest) : List (RootedForest × RootedForest)

A finite representative list for the reduced forest coproduct.

Equations

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

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

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

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

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

noncomputable def HopfAlgebras.RootedForest.coproduct {R : Type u} [CommSemiring R] (φ : RootedForest) : ForestTensorAlgebra R

The multiplicative coproduct of a non-planar rooted forest.

Equations

• φ.coproduct = Quotient.lift (fun (ts : List HopfAlgebras.RootedTree) => HopfAlgebras.PTree.coproductList (List.map Quotient.out ts)) ⋯ φ

@[simp]

theorem HopfAlgebras.RootedForest.coproduct_coe {R : Type u} [CommSemiring R] (ts : List RootedTree) : coproduct ↑ts = PTree.coproductList (List.map Quotient.out ts)

theorem HopfAlgebras.RootedForest.coproduct_ofPTree_list {R : Type u} [CommSemiring R] (ts : List PTree) : coproduct ↑(List.map RootedTree.ofPTree ts) = PTree.coproductList ts

theorem HopfAlgebras.RootedForest.coproduct_eq_sumTerms_coproductTerms {R : Type u} [CommSemiring R] (φ : RootedForest) : φ.coproduct = ForestTensorAlgebra.sumTerms φ.coproductTerms

noncomputable def HopfAlgebras.RootedForest.reducedCoproduct {R : Type u} [Semiring R] (φ : RootedForest) : ForestTensorAlgebra R

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem HopfAlgebras.RootedForest.coproduct_singleton {R : Type u} [CommSemiring R] (τ : RootedTree) : (singleton τ).coproduct = (Quotient.out τ).coproduct

theorem HopfAlgebras.RootedForest.coproduct_singleton_tree {R : Type u} [CommSemiring R] (τ : RootedTree) : (singleton τ).coproduct = τ.coproduct

theorem HopfAlgebras.RootedForest.coproduct_singleton_ofPTree {R : Type u} [CommSemiring R] (t : PTree) : (singleton (RootedTree.ofPTree t)).coproduct = t.coproduct

@[simp]

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

theorem HopfAlgebras.RootedForest.counitLeft_coproduct {R : Type u} [CommSemiring R] (φ : RootedForest) : ForestTensorAlgebra.counitLeft φ.coproduct = ForestAlgebra.ofForest φ

theorem HopfAlgebras.RootedForest.counitRight_coproduct {R : Type u} [CommSemiring R] (φ : RootedForest) : ForestTensorAlgebra.counitRight φ.coproduct = ForestAlgebra.ofForest φ

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.coproductLeft {R : Type u} [CommSemiring R] : ForestTensorAlgebra R →ₐ[R] ForestTripleTensorAlgebra R

Apply the 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.ForestTripleTensorAlgebra.coproductLeft_ofPair {R : Type u} [CommSemiring R] (term : RootedForest × RootedForest) : coproductLeft (ForestTensorAlgebra.ofPair term) = includeLeftPair term.1.coproduct * ofForests 0 0 term.2

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeft_ofForests {R : Type u} [CommSemiring R] (φ ψ : RootedForest) : coproductLeft (ForestTensorAlgebra.ofForests φ ψ) = includeLeftPair φ.coproduct * ofForests 0 0 ψ

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.coproductRight {R : Type u} [CommSemiring R] : ForestTensorAlgebra R →ₐ[R] ForestTripleTensorAlgebra R

Apply the 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.ForestTripleTensorAlgebra.coproductRight_ofPair {R : Type u} [CommSemiring R] (term : RootedForest × RootedForest) : coproductRight (ForestTensorAlgebra.ofPair term) = ofForests term.1 0 0 * includeRightPair term.2.coproduct

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRight_ofForests {R : Type u} [CommSemiring R] (φ ψ : RootedForest) : coproductRight (ForestTensorAlgebra.ofForests φ ψ) = ofForests φ 0 0 * includeRightPair ψ.coproduct

theorem HopfAlgebras.ForestTripleTensorAlgebra.includeLeftPair_sumTerms {R : Type u} [CommSemiring R] (terms : List (RootedForest × RootedForest)) : includeLeftPair (ForestTensorAlgebra.sumTerms terms) = sumTerms (List.map (fun (term : RootedForest × RootedForest) => (term.1, term.2, 0)) terms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.includeRightPair_sumTerms {R : Type u} [CommSemiring R] (terms : List (RootedForest × RootedForest)) : includeRightPair (ForestTensorAlgebra.sumTerms terms) = sumTerms (List.map (fun (term : RootedForest × RootedForest) => (0, term.1, term.2)) terms)

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

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

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerm (term : RootedForest × RootedForest) : List (RootedForest × RootedForest × RootedForest)

Equations

• HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerm term = List.map (fun (left : HopfAlgebras.RootedForest × HopfAlgebras.RootedForest) => (left.1, left.2, term.2)) term.1.coproductTerms

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerm (term : RootedForest × RootedForest) : List (RootedForest × RootedForest × RootedForest)

Equations

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

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerms (terms : List (RootedForest × RootedForest)) : List (RootedForest × RootedForest × RootedForest)

Equations

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

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerms (terms : List (RootedForest × RootedForest)) : List (RootedForest × RootedForest × RootedForest)

Equations

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

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerm_add_perm (x y : RootedForest × RootedForest) : (coproductLeftTerm (x + y)).Perm (multiplyTerms (coproductLeftTerm x) (coproductLeftTerm y))

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerm_add_perm (x y : RootedForest × RootedForest) : (coproductRightTerm (x + y)).Perm (multiplyTerms (coproductRightTerm x) (coproductRightTerm y))

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerm_singleton_graft_zero_perm (φ : RootedForest) : (coproductLeftTerm (RootedForest.singleton φ.graft, 0)).Perm (List.map (fun (term : RootedForest × RootedForest) => (term.1, RootedForest.singleton term.2.graft, 0)) φ.coproductTerms ++ [(RootedForest.singleton φ.graft, 0, 0)])

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerm_singleton_graft_perm (φ ψ : RootedForest) : (coproductRightTerm (φ, RootedForest.singleton ψ.graft)).Perm (List.map (fun (term : RootedForest × RootedForest) => (φ, term.1, RootedForest.singleton term.2.graft)) ψ.coproductTerms ++ [(φ, RootedForest.singleton ψ.graft, 0)])

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerms_append (xs ys : List (RootedForest × RootedForest)) : coproductLeftTerms (xs ++ ys) = coproductLeftTerms xs ++ coproductLeftTerms ys

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerms_append (xs ys : List (RootedForest × RootedForest)) : coproductRightTerms (xs ++ ys) = coproductRightTerms xs ++ coproductRightTerms ys

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerms_map_singleton_graft (terms : List (RootedForest × RootedForest)) : coproductLeftTerms (List.map (fun (term : RootedForest × RootedForest) => (term.1, RootedForest.singleton term.2.graft)) terms) = List.map (fun (triple : RootedForest × RootedForest × RootedForest) => (triple.1, triple.2.1, RootedForest.singleton triple.2.2.graft)) (coproductLeftTerms terms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerms_map_singleton_graft_perm (terms : List (RootedForest × RootedForest)) : (coproductRightTerms (List.map (fun (term : RootedForest × RootedForest) => (term.1, RootedForest.singleton term.2.graft)) terms)).Perm (List.map (fun (triple : RootedForest × RootedForest × RootedForest) => (triple.1, triple.2.1, RootedForest.singleton triple.2.2.graft)) (coproductRightTerms terms) ++ List.map (fun (term : RootedForest × RootedForest) => (term.1, RootedForest.singleton term.2.graft, 0)) terms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerm_zero_perm (φ : RootedForest) : (coproductRightTerm (φ, 0)).Perm [(φ, 0, 0)]

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductTerms_node_left_right_perm_of_coproductTermsList_perm (ts : List PTree) (h : (coproductLeftTerms (PTree.coproductTermsList ts)).Perm (coproductRightTerms (PTree.coproductTermsList ts))) : (coproductLeftTerms (PTree.node ts).coproductTerms).Perm (coproductRightTerms (PTree.node ts).coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerms_multiplyCoproductTerms_perm (xs ys : List (RootedForest × RootedForest)) : (coproductLeftTerms (PTree.multiplyCoproductTerms xs ys)).Perm (multiplyTerms (coproductLeftTerms xs) (coproductLeftTerms ys))

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerms_multiplyCoproductTerms_perm (xs ys : List (RootedForest × RootedForest)) : (coproductRightTerms (PTree.multiplyCoproductTerms xs ys)).Perm (multiplyTerms (coproductRightTerms xs) (coproductRightTerms ys))

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerms_perm {xs ys : List (RootedForest × RootedForest)} (h : xs.Perm ys) : (coproductLeftTerms xs).Perm (coproductLeftTerms ys)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerms_perm {xs ys : List (RootedForest × RootedForest)} (h : xs.Perm ys) : (coproductRightTerms xs).Perm (coproductRightTerms ys)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerms_rootedForest_add_perm (φ ψ : RootedForest) : (coproductLeftTerms (φ + ψ).coproductTerms).Perm (multiplyTerms (coproductLeftTerms φ.coproductTerms) (coproductLeftTerms ψ.coproductTerms))

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerms_rootedForest_add_perm (φ ψ : RootedForest) : (coproductRightTerms (φ + ψ).coproductTerms).Perm (multiplyTerms (coproductRightTerms φ.coproductTerms) (coproductRightTerms ψ.coproductTerms))

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductTermsList_left_right_perm_of_coproductTerms_perm (h : ∀ (t : PTree), (coproductLeftTerms t.coproductTerms).Perm (coproductRightTerms t.coproductTerms)) (ts : List PTree) : (coproductLeftTerms (PTree.coproductTermsList ts)).Perm (coproductRightTerms (PTree.coproductTermsList ts))

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductTerms_left_right_perm (t : PTree) : (coproductLeftTerms t.coproductTerms).Perm (coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductTermsList_left_right_perm (ts : List PTree) : (coproductLeftTerms (PTree.coproductTermsList ts)).Perm (coproductRightTerms (PTree.coproductTermsList ts))

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductTerms_rootedForest_left_right_perm_of_coproductTerms_perm (h : ∀ (t : PTree), (coproductLeftTerms t.coproductTerms).Perm (coproductRightTerms t.coproductTerms)) (φ : RootedForest) : (coproductLeftTerms φ.coproductTerms).Perm (coproductRightTerms φ.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerm_order {term : RootedForest × RootedForest} {triple : RootedForest × RootedForest × RootedForest} (htriple : triple ∈ coproductLeftTerm term) : triple.1.order + triple.2.1.order + triple.2.2.order = term.1.order + term.2.order

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerm_order {term : RootedForest × RootedForest} {triple : RootedForest × RootedForest × RootedForest} (htriple : triple ∈ coproductRightTerm term) : triple.1.order + triple.2.1.order + triple.2.2.order = term.1.order + term.2.order

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

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

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerms_rootedForest_order {φ : RootedForest} {triple : RootedForest × RootedForest × RootedForest} (htriple : triple ∈ coproductLeftTerms φ.coproductTerms) : triple.1.order + triple.2.1.order + triple.2.2.order = φ.order

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerms_rootedForest_order {φ : RootedForest} {triple : RootedForest × RootedForest × RootedForest} (htriple : triple ∈ coproductRightTerms φ.coproductTerms) : triple.1.order + triple.2.1.order + triple.2.2.order = φ.order

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeftTerms_ptree_order {t : PTree} {triple : RootedForest × RootedForest × RootedForest} (htriple : triple ∈ coproductLeftTerms t.coproductTerms) : triple.1.order + triple.2.1.order + triple.2.2.order = t.order

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRightTerms_ptree_order {t : PTree} {triple : RootedForest × RootedForest × RootedForest} (htriple : triple ∈ coproductRightTerms t.coproductTerms) : triple.1.order + triple.2.1.order + triple.2.2.order = t.order

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_coproductLeftTerm {R : Type u} [CommSemiring R] (term : RootedForest × RootedForest) : sumTerms (coproductLeftTerm term) = coproductLeft (ForestTensorAlgebra.ofPair term)

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_coproductRightTerm {R : Type u} [CommSemiring R] (term : RootedForest × RootedForest) : sumTerms (coproductRightTerm term) = coproductRight (ForestTensorAlgebra.ofPair term)

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_coproductLeftTerms {R : Type u} [CommSemiring R] (terms : List (RootedForest × RootedForest)) : sumTerms (coproductLeftTerms terms) = coproductLeft (ForestTensorAlgebra.sumTerms terms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_coproductRightTerms {R : Type u} [CommSemiring R] (terms : List (RootedForest × RootedForest)) : sumTerms (coproductRightTerms terms) = coproductRight (ForestTensorAlgebra.sumTerms terms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeft_coproduct_eq_sumTerms {R : Type u} [CommSemiring R] (φ : RootedForest) : coproductLeft φ.coproduct = sumTerms (coproductLeftTerms φ.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRight_coproduct_eq_sumTerms {R : Type u} [CommSemiring R] (φ : RootedForest) : coproductRight φ.coproduct = sumTerms (coproductRightTerms φ.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductLeft_ptree_coproduct_eq_sumTerms {R : Type u} [CommSemiring R] (t : PTree) : coproductLeft t.coproduct = sumTerms (coproductLeftTerms t.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductRight_ptree_coproduct_eq_sumTerms {R : Type u} [CommSemiring R] (t : PTree) : coproductRight t.coproduct = sumTerms (coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.nestedCoproductLeftCut_perm_coproductLeftTerm (c : PTree.Cut) : (List.map (fun (left : RootedForest × RootedForest) => (left.1, left.2, c.trunkForest)) (PTree.coproductTermsList c.pruned)).Perm (coproductLeftTerm (c.prunedForest, c.trunkForest))

theorem HopfAlgebras.ForestTripleTensorAlgebra.nestedCoproductRightCut_perm_coproductRightTerm (c : PTree.Cut) : (List.map (fun (right : RootedForest × RootedForest) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms).Perm (coproductRightTerm (c.prunedForest, c.trunkForest))

theorem HopfAlgebras.ForestTripleTensorAlgebra.nestedCoproductLeftCuts_perm_coproductLeftTerms (cuts : List PTree.Cut) : (List.flatMap (fun (c : PTree.Cut) => List.map (fun (left : RootedForest × RootedForest) => (left.1, left.2, c.trunkForest)) (PTree.coproductTermsList c.pruned)) cuts).Perm (coproductLeftTerms (List.map (fun (c : PTree.Cut) => (c.prunedForest, c.trunkForest)) cuts))

theorem HopfAlgebras.ForestTripleTensorAlgebra.nestedCoproductRightCuts_perm_coproductRightTerms (cuts : List PTree.Cut) : (List.flatMap (fun (c : PTree.Cut) => List.map (fun (right : RootedForest × RootedForest) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) cuts).Perm (coproductRightTerms (List.map (fun (c : PTree.Cut) => (c.prunedForest, c.trunkForest)) cuts))

theorem HopfAlgebras.ForestTripleTensorAlgebra.nestedCoproductLeftTerms_perm_coproductLeftTerms (t : PTree) : t.nestedCoproductLeftTerms.Perm (coproductLeftTerms t.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.nestedCoproductRightTerms_perm_coproductRightTerms (t : PTree) : t.nestedCoproductRightTerms.Perm (coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.nestedCoproductTerms_perm_iff_coproductTerms_perm (t : PTree) : t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms ↔ (coproductLeftTerms t.coproductTerms).Perm (coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.nestedCoproductTerms_left_right_perm (t : PTree) : t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms

theorem HopfAlgebras.ForestTripleTensorAlgebra.coproductTerms_rootedForest_left_right_perm_of_nestedCoproductTerms_perm (h : ∀ (t : PTree), t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms) (φ : RootedForest) : (coproductLeftTerms φ.coproductTerms).Perm (coproductRightTerms φ.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftCut {R : Type u} [CommSemiring R] (c : PTree.Cut) : sumTerms (List.map (fun (left : RootedForest × RootedForest) => (left.1, left.2, c.trunkForest)) (PTree.coproductTermsList c.pruned)) = coproductLeft (ForestTensorAlgebra.ofPair (c.prunedForest, c.trunkForest))

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_trunkCoproductTerms {R : Type u} [CommSemiring R] (c : PTree.Cut) : c.trunkForest.coproduct = ForestTensorAlgebra.sumTerms c.trunkCoproductTerms

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_nestedCoproductRightCut {R : Type u} [CommSemiring R] (c : PTree.Cut) : sumTerms (List.map (fun (right : RootedForest × RootedForest) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) = coproductRight (ForestTensorAlgebra.ofPair (c.prunedForest, c.trunkForest))

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

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

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftCuts {R : Type u} [CommSemiring R] (cuts : List PTree.Cut) : sumTerms (List.flatMap (fun (c : PTree.Cut) => List.map (fun (left : RootedForest × RootedForest) => (left.1, left.2, c.trunkForest)) (PTree.coproductTermsList c.pruned)) cuts) = coproductLeft (ForestTensorAlgebra.sumTerms (List.map (fun (c : PTree.Cut) => (c.prunedForest, c.trunkForest)) cuts))

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_nestedCoproductRightCuts {R : Type u} [CommSemiring R] (cuts : List PTree.Cut) : sumTerms (List.flatMap (fun (c : PTree.Cut) => List.map (fun (right : RootedForest × RootedForest) => (c.prunedForest, right.1, right.2)) c.trunkCoproductTerms) cuts) = coproductRight (ForestTensorAlgebra.sumTerms (List.map (fun (c : PTree.Cut) => (c.prunedForest, c.trunkForest)) cuts))

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

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

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

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

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftTerms {R : Type u} [CommSemiring R] (t : PTree) : sumTerms t.nestedCoproductLeftTerms = sumTerms (coproductLeftTerms t.coproductTerms)

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_nestedCoproductRightTerms {R : Type u} [CommSemiring R] (t : PTree) : sumTerms t.nestedCoproductRightTerms = sumTerms (coproductRightTerms t.coproductTerms)

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

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

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_nestedCoproductLeftTerms_perm {R : Type u} [CommSemiring R] {t u : PTree} (h : t.Perm u) : sumTerms t.nestedCoproductLeftTerms = sumTerms u.nestedCoproductLeftTerms

theorem HopfAlgebras.ForestTripleTensorAlgebra.sumTerms_nestedCoproductRightTerms_perm {R : Type u} [CommSemiring R] {t u : PTree} (h : t.Perm u) : sumTerms t.nestedCoproductRightTerms = sumTerms u.nestedCoproductRightTerms

noncomputable def HopfAlgebras.ForestAlgebra.coproduct (R : Type u) [CommSemiring R] : ForestAlgebra R →ₐ[R] ForestTensorAlgebra R

The BCK coproduct as an algebra morphism on the rooted-forest algebra.

Equations

• HopfAlgebras.ForestAlgebra.coproduct R = (AddMonoidAlgebra.lift R (HopfAlgebras.ForestTensorAlgebra R) HopfAlgebras.RootedForest) (HopfAlgebras.ForestAlgebra.coproductMonoidHom✝ R)

noncomputable def HopfAlgebras.ForestAlgebra.coproductLeft (R : Type u) [CommSemiring R] : ForestAlgebra R →ₐ[R] ForestTripleTensorAlgebra R

The iterated coproduct (Δ ⊗ id) ∘ Δ.

Equations

• HopfAlgebras.ForestAlgebra.coproductLeft R = HopfAlgebras.ForestTripleTensorAlgebra.coproductLeft.comp (HopfAlgebras.ForestAlgebra.coproduct R)

noncomputable def HopfAlgebras.ForestAlgebra.coproductRight (R : Type u) [CommSemiring R] : ForestAlgebra R →ₐ[R] ForestTripleTensorAlgebra R

The iterated coproduct (id ⊗ Δ) ∘ Δ.

Equations

• HopfAlgebras.ForestAlgebra.coproductRight R = HopfAlgebras.ForestTripleTensorAlgebra.coproductRight.comp (HopfAlgebras.ForestAlgebra.coproduct R)

@[simp]

theorem HopfAlgebras.ForestAlgebra.coproduct_ofForest {R : Type u} [CommSemiring R] (φ : RootedForest) : (coproduct R) (ofForest φ) = φ.coproduct

@[simp]

theorem HopfAlgebras.ForestAlgebra.coproductLeft_ofForest {R : Type u} [CommSemiring R] (φ : RootedForest) : (coproductLeft R) (ofForest φ) = ForestTripleTensorAlgebra.coproductLeft φ.coproduct

@[simp]

theorem HopfAlgebras.ForestAlgebra.coproductRight_ofForest {R : Type u} [CommSemiring R] (φ : RootedForest) : (coproductRight R) (ofForest φ) = ForestTripleTensorAlgebra.coproductRight φ.coproduct

@[simp]

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

@[simp]

theorem HopfAlgebras.ForestAlgebra.coproduct_ofForest_empty {R : Type u} [CommSemiring R] : (coproduct R) (ofForest RootedForest.empty) = 1

@[simp]

theorem HopfAlgebras.ForestAlgebra.coproduct_ofForest_singleton {R : Type u} [CommSemiring R] (τ : RootedTree) : (coproduct R) (ofForest (RootedForest.singleton τ)) = (Quotient.out τ).coproduct

theorem HopfAlgebras.ForestAlgebra.coproduct_ofForest_singleton_tree {R : Type u} [CommSemiring R] (τ : RootedTree) : (coproduct R) (ofForest (RootedForest.singleton τ)) = τ.coproduct

theorem HopfAlgebras.ForestAlgebra.coproduct_ofForest_singleton_ofPTree {R : Type u} [CommSemiring R] (t : PTree) : (coproduct R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t))) = t.coproduct

theorem HopfAlgebras.ForestAlgebra.coproductLeft_ofForest_singleton_ofPTree_eq_sumTerms {R : Type u} [CommSemiring R] (t : PTree) : (coproductLeft R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t))) = ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms)

theorem HopfAlgebras.ForestAlgebra.coproductRight_ofForest_singleton_ofPTree_eq_sumTerms {R : Type u} [CommSemiring R] (t : PTree) : (coproductRight R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t))) = ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_of_singletons {R : Type u} [CommSemiring R] (h : ∀ (τ : RootedTree), (coproductLeft R) (ofForest (RootedForest.singleton τ)) = (coproductRight R) (ofForest (RootedForest.singleton τ))) : coproductLeft R = coproductRight R

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_iff_singletons {R : Type u} [CommSemiring R] : coproductLeft R = coproductRight R ↔ ∀ (τ : RootedTree), (coproductLeft R) (ofForest (RootedForest.singleton τ)) = (coproductRight R) (ofForest (RootedForest.singleton τ))

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_of_ptree_singletons {R : Type u} [CommSemiring R] (h : ∀ (t : PTree), (coproductLeft R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t))) = (coproductRight R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t)))) : coproductLeft R = coproductRight R

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_iff_ptree_singletons {R : Type u} [CommSemiring R] : coproductLeft R = coproductRight R ↔ ∀ (t : PTree), (coproductLeft R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t))) = (coproductRight R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t)))

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_of_ptree_coproductTerms {R : Type u} [CommSemiring R] (h : ∀ (t : PTree), ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms) = ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)) : coproductLeft R = coproductRight R

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_iff_ptree_coproductTerms {R : Type u} [CommSemiring R] : coproductLeft R = coproductRight R ↔ ∀ (t : PTree), ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms) = ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_of_nestedCoproductTerms {R : Type u} [CommSemiring R] (h : ∀ (t : PTree), ForestTripleTensorAlgebra.sumTerms t.nestedCoproductLeftTerms = ForestTripleTensorAlgebra.sumTerms t.nestedCoproductRightTerms) : coproductLeft R = coproductRight R

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_iff_nestedCoproductTerms {R : Type u} [CommSemiring R] : coproductLeft R = coproductRight R ↔ ∀ (t : PTree), ForestTripleTensorAlgebra.sumTerms t.nestedCoproductLeftTerms = ForestTripleTensorAlgebra.sumTerms t.nestedCoproductRightTerms

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

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_of_ptree_coproductTerms_perm {R : Type u} [CommSemiring R] (h : ∀ (t : PTree), (ForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms).Perm (ForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)) : coproductLeft R = coproductRight R

theorem HopfAlgebras.ForestAlgebra.coproductLeft_eq_coproductRight_of_rootedForest_coproductTerms_perm {R : Type u} [CommSemiring R] (h : ∀ (φ : RootedForest), (ForestTripleTensorAlgebra.coproductLeftTerms φ.coproductTerms).Perm (ForestTripleTensorAlgebra.coproductRightTerms φ.coproductTerms)) : coproductLeft R = coproductRight R

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

theorem HopfAlgebras.ForestAlgebra.counitLeft_coproduct {R : Type u} [CommSemiring R] : ForestTensorAlgebra.counitLeft.comp (coproduct R) = AlgHom.id R (ForestAlgebra R)

theorem HopfAlgebras.ForestAlgebra.counitRight_coproduct {R : Type u} [CommSemiring R] : ForestTensorAlgebra.counitRight.comp (coproduct R) = AlgHom.id R (ForestAlgebra R)