Character Convolution on the BCK Hopf Algebra

The convolution product of forest-algebra characters induced by the BCK coproduct, with its unit (the counit), associativity, and the coefficient functions on planar trees, rooted trees and forests.

noncomputable def HopfAlgebras.PTree.evalCoproductTerm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (term : RootedForest × RootedForest) : R

Evaluate one tensor-coded coproduct term against two characters.

Equations

• HopfAlgebras.PTree.evalCoproductTerm χ ψ term = χ.evalForest term.1 * ψ.evalForest term.2

@[simp]

theorem HopfAlgebras.PTree.evalCoproductTerm_zero {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) : evalCoproductTerm χ ψ 0 = 1

@[simp]

theorem HopfAlgebras.PTree.evalCoproductTerm_add {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (x y : RootedForest × RootedForest) : evalCoproductTerm χ ψ (x + y) = evalCoproductTerm χ ψ x * evalCoproductTerm χ ψ y

theorem HopfAlgebras.PTree.evalCoproductTerm_ofPTree_list_forall₂_perm_singleton {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {ps qs : List PTree} (hps : List.Forall₂ Perm ps qs) {t u : PTree} (htu : t.Perm u) : evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree ps), RootedForest.singleton (RootedTree.ofPTree t)) = evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree qs), RootedForest.singleton (RootedTree.ofPTree u))

theorem HopfAlgebras.PTree.evalCoproductTerm_ofPTree_list_forestPerm_singleton {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {ps qs : List PTree} (hps : ForestPerm ps qs) {t u : PTree} (htu : RootedTree.ofPTree t = RootedTree.ofPTree u) : evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree ps), RootedForest.singleton (RootedTree.ofPTree t)) = evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree qs), RootedForest.singleton (RootedTree.ofPTree u))

theorem HopfAlgebras.PTree.evalCoproductTerm_ofPTree_list_forall₂_perm_zero {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {ps qs : List PTree} (hps : List.Forall₂ Perm ps qs) : evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree ps), 0) = evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree qs), 0)

theorem HopfAlgebras.PTree.evalCoproductTerm_ofPTree_list_forestPerm_zero {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {ps qs : List PTree} (hps : ForestPerm ps qs) : evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree ps), 0) = evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree qs), 0)

theorem HopfAlgebras.PTree.evalCoproductTerm_rootCut_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {c d : RootCut} (h : c.Perm d) : evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree c.pruned), RootedForest.singleton (RootedTree.ofPTree c.trunk)) = evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree d.pruned), RootedForest.singleton (RootedTree.ofPTree d.trunk))

theorem HopfAlgebras.PTree.evalCoproductTerm_rootCutList_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {c d : RootCutList} (h : c.Perm d) : evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree c.pruned), RootedForest.singleton (RootedTree.ofPTree (node c.trunks))) = evalCoproductTerm χ ψ (↑(List.map RootedTree.ofPTree d.pruned), RootedForest.singleton (RootedTree.ofPTree (node d.trunks)))

theorem HopfAlgebras.PTree.evalCoproductTerm_cut_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {c d : Cut} (h : c.Perm d) : evalCoproductTerm χ ψ (c.prunedForest, c.trunkForest) = evalCoproductTerm χ ψ (d.prunedForest, d.trunkForest)

noncomputable def HopfAlgebras.PTree.evalCoproductTerms {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (terms : List (RootedForest × RootedForest)) : R

Evaluate a finite list of tensor-coded coproduct terms.

Equations

• HopfAlgebras.PTree.evalCoproductTerms χ ψ terms = (List.map (HopfAlgebras.PTree.evalCoproductTerm χ ψ) terms).sum

@[simp]

theorem HopfAlgebras.PTree.evalCoproductTerms_nil {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) : evalCoproductTerms χ ψ [] = 0

@[simp]

theorem HopfAlgebras.PTree.evalCoproductTerms_cons {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (term : RootedForest × RootedForest) (terms : List (RootedForest × RootedForest)) : evalCoproductTerms χ ψ (term :: terms) = evalCoproductTerm χ ψ term + evalCoproductTerms χ ψ terms

theorem HopfAlgebras.PTree.evalCoproductTerms_append {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (xs ys : List (RootedForest × RootedForest)) : evalCoproductTerms χ ψ (xs ++ ys) = evalCoproductTerms χ ψ xs + evalCoproductTerms χ ψ ys

theorem HopfAlgebras.PTree.evalCoproductTerms_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {xs ys : List (RootedForest × RootedForest)} (h : xs.Perm ys) : evalCoproductTerms χ ψ xs = evalCoproductTerms χ ψ ys

theorem HopfAlgebras.PTree.evalCoproductTerms_eq_of_forall₂_eval_eq {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {xs ys : List (RootedForest × RootedForest)} : List.Forall₂ (fun (x y : RootedForest × RootedForest) => evalCoproductTerm χ ψ x = evalCoproductTerm χ ψ y) xs ys → evalCoproductTerms χ ψ xs = evalCoproductTerms χ ψ ys

theorem HopfAlgebras.PTree.evalCoproductTerms_rootCut_forall₂_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {cs ds : List RootCut} : List.Forall₂ RootCut.Perm cs ds → evalCoproductTerms χ ψ (List.map (fun (c : RootCut) => (↑(List.map RootedTree.ofPTree c.pruned), RootedForest.singleton (RootedTree.ofPTree c.trunk))) cs) = evalCoproductTerms χ ψ (List.map (fun (d : RootCut) => (↑(List.map RootedTree.ofPTree d.pruned), RootedForest.singleton (RootedTree.ofPTree d.trunk))) ds)

theorem HopfAlgebras.PTree.evalCoproductTerms_rootCut_listRelPerm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {cs ds : List RootCut} (h : ListRelPerm RootCut.Perm cs ds) : evalCoproductTerms χ ψ (List.map (fun (c : RootCut) => (↑(List.map RootedTree.ofPTree c.pruned), RootedForest.singleton (RootedTree.ofPTree c.trunk))) cs) = evalCoproductTerms χ ψ (List.map (fun (d : RootCut) => (↑(List.map RootedTree.ofPTree d.pruned), RootedForest.singleton (RootedTree.ofPTree d.trunk))) ds)

theorem HopfAlgebras.PTree.evalCoproductTerms_rootCutList_forall₂_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {cs ds : List RootCutList} : List.Forall₂ RootCutList.Perm cs ds → evalCoproductTerms χ ψ (List.map (fun (c : RootCutList) => (↑(List.map RootedTree.ofPTree c.pruned), RootedForest.singleton (RootedTree.ofPTree (node c.trunks)))) cs) = evalCoproductTerms χ ψ (List.map (fun (d : RootCutList) => (↑(List.map RootedTree.ofPTree d.pruned), RootedForest.singleton (RootedTree.ofPTree (node d.trunks)))) ds)

theorem HopfAlgebras.PTree.evalCoproductTerms_rootCutList_listRelPerm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {cs ds : List RootCutList} (h : ListRelPerm RootCutList.Perm cs ds) : evalCoproductTerms χ ψ (List.map (fun (c : RootCutList) => (↑(List.map RootedTree.ofPTree c.pruned), RootedForest.singleton (RootedTree.ofPTree (node c.trunks)))) cs) = evalCoproductTerms χ ψ (List.map (fun (d : RootCutList) => (↑(List.map RootedTree.ofPTree d.pruned), RootedForest.singleton (RootedTree.ofPTree (node d.trunks)))) ds)

theorem HopfAlgebras.PTree.evalCoproductTerms_cut_forall₂_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {cs ds : List Cut} : List.Forall₂ Cut.Perm cs ds → evalCoproductTerms χ ψ (List.map (fun (c : Cut) => (c.prunedForest, c.trunkForest)) cs) = evalCoproductTerms χ ψ (List.map (fun (d : Cut) => (d.prunedForest, d.trunkForest)) ds)

theorem HopfAlgebras.PTree.evalCoproductTerms_cut_listRelPerm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {cs ds : List Cut} (h : ListRelPerm Cut.Perm cs ds) : evalCoproductTerms χ ψ (List.map (fun (c : Cut) => (c.prunedForest, c.trunkForest)) cs) = evalCoproductTerms χ ψ (List.map (fun (d : Cut) => (d.prunedForest, d.trunkForest)) ds)

theorem HopfAlgebras.PTree.evalCoproductTerms_map_add_left {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (x : RootedForest × RootedForest) (ys : List (RootedForest × RootedForest)) : evalCoproductTerms χ ψ (List.map (fun (y : RootedForest × RootedForest) => x + y) ys) = evalCoproductTerm χ ψ x * evalCoproductTerms χ ψ ys

theorem HopfAlgebras.PTree.evalCoproductTerms_multiply {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (xs ys : List (RootedForest × RootedForest)) : evalCoproductTerms χ ψ (multiplyCoproductTerms xs ys) = evalCoproductTerms χ ψ xs * evalCoproductTerms χ ψ ys

noncomputable def HopfAlgebras.PTree.evalTripleCoproductTerm {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (term : RootedForest × RootedForest × RootedForest) : R

Evaluate one triple tensor-coded term against three characters.

Equations

• HopfAlgebras.PTree.evalTripleCoproductTerm χ ψ η term = χ.evalForest term.1 * ψ.evalForest term.2.1 * η.evalForest term.2.2

@[simp]

theorem HopfAlgebras.PTree.evalTripleCoproductTerm_zero {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) : evalTripleCoproductTerm χ ψ η 0 = 1

@[simp]

theorem HopfAlgebras.PTree.evalTripleCoproductTerm_add {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (x y : RootedForest × RootedForest × RootedForest) : evalTripleCoproductTerm χ ψ η (x + y) = evalTripleCoproductTerm χ ψ η x * evalTripleCoproductTerm χ ψ η y

noncomputable def HopfAlgebras.PTree.evalTripleCoproductTerms {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (terms : List (RootedForest × RootedForest × RootedForest)) : R

Evaluate a finite list of triple tensor-coded terms.

Equations

• HopfAlgebras.PTree.evalTripleCoproductTerms χ ψ η terms = (List.map (HopfAlgebras.PTree.evalTripleCoproductTerm χ ψ η) terms).sum

@[simp]

theorem HopfAlgebras.PTree.evalTripleCoproductTerms_nil {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) : evalTripleCoproductTerms χ ψ η [] = 0

@[simp]

theorem HopfAlgebras.PTree.evalTripleCoproductTerms_cons {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (term : RootedForest × RootedForest × RootedForest) (terms : List (RootedForest × RootedForest × RootedForest)) : evalTripleCoproductTerms χ ψ η (term :: terms) = evalTripleCoproductTerm χ ψ η term + evalTripleCoproductTerms χ ψ η terms

theorem HopfAlgebras.PTree.evalTripleCoproductTerms_append {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (xs ys : List (RootedForest × RootedForest × RootedForest)) : evalTripleCoproductTerms χ ψ η (xs ++ ys) = evalTripleCoproductTerms χ ψ η xs + evalTripleCoproductTerms χ ψ η ys

theorem HopfAlgebras.PTree.evalTripleCoproductTerms_perm {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) {xs ys : List (RootedForest × RootedForest × RootedForest)} (h : xs.Perm ys) : evalTripleCoproductTerms χ ψ η xs = evalTripleCoproductTerms χ ψ η ys

theorem HopfAlgebras.PTree.evalTripleCoproductTerms_map_add_left {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (x : RootedForest × RootedForest × RootedForest) (ys : List (RootedForest × RootedForest × RootedForest)) : evalTripleCoproductTerms χ ψ η (List.map (fun (y : RootedForest × RootedForest × RootedForest) => x + y) ys) = evalTripleCoproductTerm χ ψ η x * evalTripleCoproductTerms χ ψ η ys

theorem HopfAlgebras.PTree.evalTripleCoproductTerms_multiply {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (xs ys : List (RootedForest × RootedForest × RootedForest)) : evalTripleCoproductTerms χ ψ η (ForestTripleTensorAlgebra.multiplyTerms xs ys) = evalTripleCoproductTerms χ ψ η xs * evalTripleCoproductTerms χ ψ η ys

noncomputable def HopfAlgebras.PTree.convolutionCoeff {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (t : PTree) : R

The convolution coefficient of two characters on a planar rooted tree.

Equations

• HopfAlgebras.PTree.convolutionCoeff χ ψ t = HopfAlgebras.PTree.evalCoproductTerms χ ψ t.coproductTerms

theorem HopfAlgebras.PTree.convolutionCoeff_eq_of_cuts_listRelPerm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {t u : PTree} (h : ListRelPerm Cut.Perm t.cuts u.cuts) : convolutionCoeff χ ψ t = convolutionCoeff χ ψ u

theorem HopfAlgebras.PTree.convolutionCoeff_eq_of_rootCuts_listRelPerm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {t u : PTree} (htu : t.Perm u) (hroot : ListRelPerm RootCut.Perm t.rootCuts u.rootCuts) : convolutionCoeff χ ψ t = convolutionCoeff χ ψ u

theorem HopfAlgebras.PTree.convolutionCoeff_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {t u : PTree} (h : t.Perm u) : convolutionCoeff χ ψ t = convolutionCoeff χ ψ u

theorem HopfAlgebras.PTree.convolutionCoeff_node_eq_of_forall₂_perm_rootCuts {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {ts us : List PTree} (h : List.Forall₂ (fun (t u : PTree) => t.Perm u ∧ ListRelPerm RootCut.Perm t.rootCuts u.rootCuts) ts us) : convolutionCoeff χ ψ (node ts) = convolutionCoeff χ ψ (node us)

noncomputable def HopfAlgebras.PTree.convolutionForestCoeff {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (ts : List PTree) : R

Multiplicative extension of convolution coefficients to planar forests.

Equations

• HopfAlgebras.PTree.convolutionForestCoeff χ ψ ts = HopfAlgebras.PTree.evalCoproductTerms χ ψ (HopfAlgebras.PTree.coproductTermsList ts)

@[simp]

theorem HopfAlgebras.PTree.convolutionForestCoeff_nil {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) : convolutionForestCoeff χ ψ [] = 1

@[simp]

theorem HopfAlgebras.PTree.convolutionForestCoeff_cons {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (t : PTree) (ts : List PTree) : convolutionForestCoeff χ ψ (t :: ts) = convolutionCoeff χ ψ t * convolutionForestCoeff χ ψ ts

theorem HopfAlgebras.PTree.convolutionForestCoeff_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {ts us : List PTree} (h : ts.Perm us) : convolutionForestCoeff χ ψ ts = convolutionForestCoeff χ ψ us

theorem HopfAlgebras.PTree.convolutionForestCoeff_forall₂_perm {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) {ts us : List PTree} : List.Forall₂ Perm ts us → convolutionForestCoeff χ ψ ts = convolutionForestCoeff χ ψ us

theorem HopfAlgebras.PTree.convolutionCoeff_unit_right {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (t : PTree) : convolutionCoeff χ (ForestAlgebra.counit R) t = χ.evalForest (RootedForest.singleton (RootedTree.ofPTree t))

theorem HopfAlgebras.PTree.convolutionCoeff_unit_left {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (t : PTree) : convolutionCoeff (ForestAlgebra.counit R) χ t = χ.evalForest (RootedForest.singleton (RootedTree.ofPTree t))

theorem HopfAlgebras.PTree.convolutionForestCoeff_unit_right {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (ts : List PTree) : convolutionForestCoeff χ (ForestAlgebra.counit R) ts = χ.evalForest ↑(List.map RootedTree.ofPTree ts)

theorem HopfAlgebras.PTree.convolutionForestCoeff_unit_left {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (ts : List PTree) : convolutionForestCoeff (ForestAlgebra.counit R) χ ts = χ.evalForest ↑(List.map RootedTree.ofPTree ts)

noncomputable def HopfAlgebras.ForestTensorAlgebra.evalByCharacters {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) : ForestTensorAlgebra R →ₐ[R] R

Evaluate the tensor-coded forest algebra using two characters.

Equations

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

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.evalByCharacters_ofPair {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (term : RootedForest × RootedForest) : (evalByCharacters χ ψ) (ofPair term) = PTree.evalCoproductTerm χ ψ term

theorem HopfAlgebras.ForestTensorAlgebra.evalByCharacters_sumTerms {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (terms : List (RootedForest × RootedForest)) : (evalByCharacters χ ψ) (sumTerms terms) = PTree.evalCoproductTerms χ ψ terms

theorem HopfAlgebras.ForestTensorAlgebra.evalByLinearMaps_ofCharacter {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) : evalByLinearMaps (ForestAlgebra.LinearFunctional.ofCharacter χ) (ForestAlgebra.LinearFunctional.ofCharacter ψ) = (evalByCharacters χ ψ).toLinearMap

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.evalByCharacters_coproduct {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (t : PTree) : (evalByCharacters χ ψ) t.coproduct = PTree.convolutionCoeff χ ψ t

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.evalByCharacters_coproductList {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (ts : List PTree) : (evalByCharacters χ ψ) (PTree.coproductList ts) = PTree.convolutionForestCoeff χ ψ ts

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.evalByCharacters {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) : ForestTripleTensorAlgebra R →ₐ[R] R

Evaluate the triple tensor-coded forest algebra using three characters.

Equations

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

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.evalByCharacters_ofTriple {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (term : RootedForest × RootedForest × RootedForest) : (evalByCharacters χ ψ η) (ofTriple term) = PTree.evalTripleCoproductTerm χ ψ η term

theorem HopfAlgebras.ForestTripleTensorAlgebra.evalByCharacters_sumTerms {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (terms : List (RootedForest × RootedForest × RootedForest)) : (evalByCharacters χ ψ η) (sumTerms terms) = PTree.evalTripleCoproductTerms χ ψ η terms

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.evalByCharacters_includeLeftPair {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (x : ForestTensorAlgebra R) : (evalByCharacters χ ψ η) (includeLeftPair x) = (ForestTensorAlgebra.evalByCharacters χ ψ) x

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.evalByCharacters_includeRightPair {R : Type u} [CommSemiring R] (χ ψ η : ForestAlgebra.Character R) (x : ForestTensorAlgebra R) : (evalByCharacters χ ψ η) (includeRightPair x) = (ForestTensorAlgebra.evalByCharacters ψ η) x

noncomputable def HopfAlgebras.RootedForest.convolutionCoeff {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (φ : RootedForest) : R

Character convolution evaluated on a non-planar rooted forest.

Equations

• HopfAlgebras.RootedForest.convolutionCoeff χ ψ φ = (HopfAlgebras.ForestTensorAlgebra.evalByCharacters χ ψ) φ.coproduct

@[simp]

theorem HopfAlgebras.RootedForest.convolutionCoeff_zero {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) : convolutionCoeff χ ψ 0 = 1

@[simp]

theorem HopfAlgebras.RootedForest.convolutionCoeff_empty {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) : convolutionCoeff χ ψ empty = 1

@[simp]

theorem HopfAlgebras.RootedForest.convolutionCoeff_singleton {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (τ : RootedTree) : convolutionCoeff χ ψ (singleton τ) = PTree.convolutionCoeff χ ψ (Quotient.out τ)

theorem HopfAlgebras.RootedForest.convolutionCoeff_singleton_ofPTree {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (t : PTree) : convolutionCoeff χ ψ (singleton (RootedTree.ofPTree t)) = PTree.convolutionCoeff χ ψ t

@[simp]

theorem HopfAlgebras.RootedForest.convolutionCoeff_add {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (φ η : RootedForest) : convolutionCoeff χ ψ (φ + η) = convolutionCoeff χ ψ φ * convolutionCoeff χ ψ η

theorem HopfAlgebras.RootedForest.convolutionCoeff_unit_right {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (φ : RootedForest) : convolutionCoeff χ (ForestAlgebra.counit R) φ = χ.evalForest φ

theorem HopfAlgebras.RootedForest.convolutionCoeff_unit_left {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (φ : RootedForest) : convolutionCoeff (ForestAlgebra.counit R) χ φ = χ.evalForest φ

noncomputable def HopfAlgebras.RootedTree.convolutionCoeff {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (τ : RootedTree) : R

Character convolution coefficient on a non-planar rooted tree.

Equations

• HopfAlgebras.RootedTree.convolutionCoeff χ ψ τ = (HopfAlgebras.ForestTensorAlgebra.evalByCharacters χ ψ) τ.coproduct

theorem HopfAlgebras.RootedTree.convolutionCoeff_eq_singleton {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (τ : RootedTree) : convolutionCoeff χ ψ τ = RootedForest.convolutionCoeff χ ψ (RootedForest.singleton τ)

theorem HopfAlgebras.RootedTree.convolutionCoeff_out {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (τ : RootedTree) : convolutionCoeff χ ψ τ = PTree.convolutionCoeff χ ψ (Quotient.out τ)

theorem HopfAlgebras.RootedTree.convolutionCoeff_ofPTree {R : Type u} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (t : PTree) : convolutionCoeff χ ψ (ofPTree t) = PTree.convolutionCoeff χ ψ t

theorem HopfAlgebras.RootedTree.convolutionCoeff_unit_right {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (τ : RootedTree) : convolutionCoeff χ (ForestAlgebra.counit R) τ = χ.evalForest (RootedForest.singleton τ)

theorem HopfAlgebras.RootedTree.convolutionCoeff_unit_left {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (τ : RootedTree) : convolutionCoeff (ForestAlgebra.counit R) χ τ = χ.evalForest (RootedForest.singleton τ)

noncomputable def HopfAlgebras.ForestAlgebra.Character.unit (R : Type u) [CommSemiring R] : Character R

The identity character for convolution.

Equations

• HopfAlgebras.ForestAlgebra.Character.unit R = HopfAlgebras.ForestAlgebra.counit R

@[simp]

theorem HopfAlgebras.ForestAlgebra.Character.unit_evalForest {R : Type u} [CommSemiring R] (φ : RootedForest) : (unit R).evalForest φ = counitCoeff φ

theorem HopfAlgebras.ForestAlgebra.Character.unit_eq_counit {R : Type u} [CommSemiring R] : unit R = counit R

@[simp]

theorem HopfAlgebras.ForestAlgebra.Character.linearFunctional_ofCharacter_unit {R : Type u} [CommSemiring R] : LinearFunctional.ofCharacter (unit R) = LinearFunctional.counit R

noncomputable def HopfAlgebras.ForestAlgebra.Character.convolution {R : Type u} [CommSemiring R] (χ ψ : Character R) : Character R

Character convolution induced by the BCK coproduct.

Equations

• χ.convolution ψ = (HopfAlgebras.ForestTensorAlgebra.evalByCharacters χ ψ).comp (HopfAlgebras.ForestAlgebra.coproduct R)

@[simp]

theorem HopfAlgebras.ForestAlgebra.Character.convolution_evalForest {R : Type u} [CommSemiring R] (χ ψ : Character R) (φ : RootedForest) : (χ.convolution ψ).evalForest φ = RootedForest.convolutionCoeff χ ψ φ

@[simp]

theorem HopfAlgebras.ForestAlgebra.Character.convolution_ofForest {R : Type u} [CommSemiring R] (χ ψ : Character R) (φ : RootedForest) : (χ.convolution ψ) (ofForest φ) = RootedForest.convolutionCoeff χ ψ φ

theorem HopfAlgebras.ForestAlgebra.Character.linearFunctional_ofCharacter_convolution {R : Type u} [CommSemiring R] (χ ψ : Character R) : LinearFunctional.ofCharacter (χ.convolution ψ) = (LinearFunctional.ofCharacter χ).convolution (LinearFunctional.ofCharacter ψ)

theorem HopfAlgebras.ForestAlgebra.Character.linearFunctional_ofCharacter_injective {R : Type u} [CommSemiring R] : Function.Injective LinearFunctional.ofCharacter

theorem HopfAlgebras.ForestAlgebra.Character.convolution_unit_right {R : Type u} [CommSemiring R] (χ : Character R) : χ.convolution (unit R) = χ

theorem HopfAlgebras.ForestAlgebra.Character.convolution_unit_left {R : Type u} [CommSemiring R] (χ : Character R) : (unit R).convolution χ = χ

theorem HopfAlgebras.ForestAlgebra.Character.linearFunctional_convolution_compAntipode_ofCharacter_left {R : Type u} [CommRing R] (χ : Character R) : (LinearFunctional.ofCharacter χ).compAntipode.convolution (LinearFunctional.ofCharacter χ) = LinearFunctional.ofCharacter (unit R)

theorem HopfAlgebras.ForestAlgebra.Character.linearFunctional_convolution_compAntipode_ofCharacter_right {R : Type u} [CommRing R] (χ : Character R) : (LinearFunctional.ofCharacter χ).convolution (LinearFunctional.ofCharacter χ).compAntipode = LinearFunctional.ofCharacter (unit R)

theorem HopfAlgebras.ForestAlgebra.Character.convolution_left_cancel {R : Type u} [CommRing R] {χ ψ η : Character R} (h : χ.convolution ψ = χ.convolution η) : ψ = η

theorem HopfAlgebras.ForestAlgebra.Character.convolution_right_cancel {R : Type u} [CommRing R] {χ ψ η : Character R} (h : ψ.convolution χ = η.convolution χ) : ψ = η

theorem HopfAlgebras.ForestAlgebra.Character.evalByCharacters_coproductLeft {R : Type u} [CommSemiring R] (χ ψ η : Character R) (x : ForestTensorAlgebra R) : (ForestTripleTensorAlgebra.evalByCharacters χ ψ η) (ForestTripleTensorAlgebra.coproductLeft x) = (ForestTensorAlgebra.evalByCharacters (χ.convolution ψ) η) x

theorem HopfAlgebras.ForestAlgebra.Character.evalByCharacters_coproductRight {R : Type u} [CommSemiring R] (χ ψ η : Character R) (x : ForestTensorAlgebra R) : (ForestTripleTensorAlgebra.evalByCharacters χ ψ η) (ForestTripleTensorAlgebra.coproductRight x) = (ForestTensorAlgebra.evalByCharacters χ (ψ.convolution η)) x

theorem HopfAlgebras.ForestAlgebra.Character.evalByCharacters_forestCoproductLeft {R : Type u} [CommSemiring R] (χ ψ η : Character R) (x : ForestAlgebra R) : (ForestTripleTensorAlgebra.evalByCharacters χ ψ η) ((coproductLeft R) x) = ((χ.convolution ψ).convolution η) x

theorem HopfAlgebras.ForestAlgebra.Character.evalByCharacters_forestCoproductRight {R : Type u} [CommSemiring R] (χ ψ η : Character R) (x : ForestAlgebra R) : (ForestTripleTensorAlgebra.evalByCharacters χ ψ η) ((coproductRight R) x) = (χ.convolution (ψ.convolution η)) x

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_coproductLeftTerms {R : Type u} [CommSemiring R] (χ ψ η : Character R) (terms : List (RootedForest × RootedForest)) : PTree.evalTripleCoproductTerms χ ψ η (ForestTripleTensorAlgebra.coproductLeftTerms terms) = PTree.evalCoproductTerms (χ.convolution ψ) η terms

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_coproductRightTerms {R : Type u} [CommSemiring R] (χ ψ η : Character R) (terms : List (RootedForest × RootedForest)) : PTree.evalTripleCoproductTerms χ ψ η (ForestTripleTensorAlgebra.coproductRightTerms terms) = PTree.evalCoproductTerms χ (ψ.convolution η) terms

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_coproductLeftTerms_ptree {R : Type u} [CommSemiring R] (χ ψ η : Character R) (t : PTree) : PTree.evalTripleCoproductTerms χ ψ η (ForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms) = PTree.convolutionCoeff (χ.convolution ψ) η t

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_coproductRightTerms_ptree {R : Type u} [CommSemiring R] (χ ψ η : Character R) (t : PTree) : PTree.evalTripleCoproductTerms χ ψ η (ForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms) = PTree.convolutionCoeff χ (ψ.convolution η) t

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_nestedCoproductLeftTerms {R : Type u} [CommSemiring R] (χ ψ η : Character R) (t : PTree) : PTree.evalTripleCoproductTerms χ ψ η t.nestedCoproductLeftTerms = PTree.convolutionCoeff (χ.convolution ψ) η t

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_nestedCoproductRightTerms {R : Type u} [CommSemiring R] (χ ψ η : Character R) (t : PTree) : PTree.evalTripleCoproductTerms χ ψ η t.nestedCoproductRightTerms = PTree.convolutionCoeff χ (ψ.convolution η) t

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_nestedCoproductLeftTerms_listRelPerm {R : Type u} [CommSemiring R] (χ ψ η : Character R) {t u : PTree} (h : PTree.ListRelPerm PTree.Cut.Perm t.cuts u.cuts) : PTree.evalTripleCoproductTerms χ ψ η t.nestedCoproductLeftTerms = PTree.evalTripleCoproductTerms χ ψ η u.nestedCoproductLeftTerms

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_nestedCoproductRightTerms_listRelPerm {R : Type u} [CommSemiring R] (χ ψ η : Character R) {t u : PTree} (h : PTree.ListRelPerm PTree.Cut.Perm t.cuts u.cuts) : PTree.evalTripleCoproductTerms χ ψ η t.nestedCoproductRightTerms = PTree.evalTripleCoproductTerms χ ψ η u.nestedCoproductRightTerms

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_nestedCoproductLeftTerms_perm {R : Type u} [CommSemiring R] (χ ψ η : Character R) {t u : PTree} (h : t.Perm u) : PTree.evalTripleCoproductTerms χ ψ η t.nestedCoproductLeftTerms = PTree.evalTripleCoproductTerms χ ψ η u.nestedCoproductLeftTerms

theorem HopfAlgebras.ForestAlgebra.Character.evalTripleCoproductTerms_nestedCoproductRightTerms_perm {R : Type u} [CommSemiring R] (χ ψ η : Character R) {t u : PTree} (h : t.Perm u) : PTree.evalTripleCoproductTerms χ ψ η t.nestedCoproductRightTerms = PTree.evalTripleCoproductTerms χ ψ η u.nestedCoproductRightTerms

theorem HopfAlgebras.ForestAlgebra.Character.convolution_assoc_of_coproduct_eq {R : Type u} [CommSemiring R] (hcoassoc : ∀ (x : ForestAlgebra R), (coproductLeft R) x = (coproductRight R) x) (χ ψ η : Character R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.ForestAlgebra.Character.convolution_assoc_of_coproductLeft_eq_coproductRight {R : Type u} [CommSemiring R] (hcoassoc : coproductLeft R = coproductRight R) (χ ψ η : Character R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.ForestAlgebra.Character.convolution_assoc_of_coproduct_eq_singletons {R : Type u} [CommSemiring R] (hcoassoc : ∀ (τ : RootedTree), (coproductLeft R) (ofForest (RootedForest.singleton τ)) = (coproductRight R) (ofForest (RootedForest.singleton τ))) (χ ψ η : Character R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.ForestAlgebra.Character.convolution_assoc_of_coproduct_eq_ptree_singletons {R : Type u} [CommSemiring R] (hcoassoc : ∀ (t : PTree), (coproductLeft R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t))) = (coproductRight R) (ofForest (RootedForest.singleton (RootedTree.ofPTree t)))) (χ ψ η : Character R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.ForestAlgebra.Character.convolution_assoc_of_coproduct_eq_ptree_coproductTerms {R : Type u} [CommSemiring R] (hcoassoc : ∀ (t : PTree), ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms) = ForestTripleTensorAlgebra.sumTerms (ForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)) (χ ψ η : Character R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.ForestAlgebra.Character.convolution_assoc_of_nestedCoproductTerms {R : Type u} [CommSemiring R] (hcoassoc : ∀ (t : PTree), ForestTripleTensorAlgebra.sumTerms t.nestedCoproductLeftTerms = ForestTripleTensorAlgebra.sumTerms t.nestedCoproductRightTerms) (χ ψ η : Character R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.ForestAlgebra.Character.convolution_assoc_of_nestedCoproductTerms_perm {R : Type u} [CommSemiring R] (hcoassoc : ∀ (t : PTree), t.nestedCoproductLeftTerms.Perm t.nestedCoproductRightTerms) (χ ψ η : Character R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.ForestAlgebra.Character.convolution_assoc {R : Type u} [CommSemiring R] (χ ψ η : Character R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

@[implicit_reducible]

noncomputable instance HopfAlgebras.ForestAlgebra.Character.instMonoid {R : Type u} [CommSemiring R] : Monoid (Character R)

Equations

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