Labelled Character Convolution

The convolution of labelled forest-algebra characters induced by the labelled BCK coproduct, with unit (the counit), associativity, the coefficient functions on labelled trees and forests, and the erase-labels bridges to the unlabelled character convolution.

noncomputable def HopfAlgebras.PLTree.evalCoproductTerm {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (term : LRootedForest α × LRootedForest α) : R

Evaluate one labelled tensor-coded coproduct term against two characters.

Equations

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

@[simp]

theorem HopfAlgebras.PLTree.evalCoproductTerm_zero {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) : evalCoproductTerm χ ψ 0 = 1

@[simp]

theorem HopfAlgebras.PLTree.evalCoproductTerm_add {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (x y : LRootedForest α × LRootedForest α) : evalCoproductTerm χ ψ (x + y) = evalCoproductTerm χ ψ x * evalCoproductTerm χ ψ y

noncomputable def HopfAlgebras.PLTree.evalCoproductTerms {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (terms : List (LRootedForest α × LRootedForest α)) : R

Evaluate a finite list of labelled tensor-coded coproduct terms.

Equations

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

@[simp]

theorem HopfAlgebras.PLTree.evalCoproductTerms_nil {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) : evalCoproductTerms χ ψ [] = 0

@[simp]

theorem HopfAlgebras.PLTree.evalCoproductTerms_cons {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (term : LRootedForest α × LRootedForest α) (terms : List (LRootedForest α × LRootedForest α)) : evalCoproductTerms χ ψ (term :: terms) = evalCoproductTerm χ ψ term + evalCoproductTerms χ ψ terms

theorem HopfAlgebras.PLTree.evalCoproductTerms_append {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (xs ys : List (LRootedForest α × LRootedForest α)) : evalCoproductTerms χ ψ (xs ++ ys) = evalCoproductTerms χ ψ xs + evalCoproductTerms χ ψ ys

theorem HopfAlgebras.PLTree.evalCoproductTerms_perm {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) {xs ys : List (LRootedForest α × LRootedForest α)} (h : xs.Perm ys) : evalCoproductTerms χ ψ xs = evalCoproductTerms χ ψ ys

theorem HopfAlgebras.PLTree.evalCoproductTerms_map_add_left {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (x : LRootedForest α × LRootedForest α) (ys : List (LRootedForest α × LRootedForest α)) : evalCoproductTerms χ ψ (List.map (fun (y : LRootedForest α × LRootedForest α) => x + y) ys) = evalCoproductTerm χ ψ x * evalCoproductTerms χ ψ ys

theorem HopfAlgebras.PLTree.evalCoproductTerms_multiply {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (xs ys : List (LRootedForest α × LRootedForest α)) : evalCoproductTerms χ ψ (multiplyCoproductTerms xs ys) = evalCoproductTerms χ ψ xs * evalCoproductTerms χ ψ ys

noncomputable def HopfAlgebras.PLTree.evalTripleCoproductTerm {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (term : LRootedForest α × LRootedForest α × LRootedForest α) : R

Evaluate one labelled triple tensor-coded term against three characters.

Equations

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

@[simp]

theorem HopfAlgebras.PLTree.evalTripleCoproductTerm_zero {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) : evalTripleCoproductTerm χ ψ η 0 = 1

@[simp]

theorem HopfAlgebras.PLTree.evalTripleCoproductTerm_add {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (x y : LRootedForest α × LRootedForest α × LRootedForest α) : evalTripleCoproductTerm χ ψ η (x + y) = evalTripleCoproductTerm χ ψ η x * evalTripleCoproductTerm χ ψ η y

noncomputable def HopfAlgebras.PLTree.evalTripleCoproductTerms {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (terms : List (LRootedForest α × LRootedForest α × LRootedForest α)) : R

Evaluate a finite list of labelled triple tensor-coded terms.

Equations

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

@[simp]

theorem HopfAlgebras.PLTree.evalTripleCoproductTerms_nil {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) : evalTripleCoproductTerms χ ψ η [] = 0

@[simp]

theorem HopfAlgebras.PLTree.evalTripleCoproductTerms_cons {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (term : LRootedForest α × LRootedForest α × LRootedForest α) (terms : List (LRootedForest α × LRootedForest α × LRootedForest α)) : evalTripleCoproductTerms χ ψ η (term :: terms) = evalTripleCoproductTerm χ ψ η term + evalTripleCoproductTerms χ ψ η terms

theorem HopfAlgebras.PLTree.evalTripleCoproductTerms_append {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (xs ys : List (LRootedForest α × LRootedForest α × LRootedForest α)) : evalTripleCoproductTerms χ ψ η (xs ++ ys) = evalTripleCoproductTerms χ ψ η xs + evalTripleCoproductTerms χ ψ η ys

theorem HopfAlgebras.PLTree.evalTripleCoproductTerms_perm {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) {xs ys : List (LRootedForest α × LRootedForest α × LRootedForest α)} (h : xs.Perm ys) : evalTripleCoproductTerms χ ψ η xs = evalTripleCoproductTerms χ ψ η ys

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

theorem HopfAlgebras.PLTree.evalTripleCoproductTerms_multiply {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (xs ys : List (LRootedForest α × LRootedForest α × LRootedForest α)) : evalTripleCoproductTerms χ ψ η (LForestTripleTensorAlgebra.multiplyTerms xs ys) = evalTripleCoproductTerms χ ψ η xs * evalTripleCoproductTerms χ ψ η ys

theorem HopfAlgebras.PLTree.evalCoproductTerms_cut_forall₂_perm {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.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.PLTree.evalCoproductTerms_cut_listRelPerm {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) {cs ds : List (Cut α)} (h : PTree.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.PLTree.evalCoproductTerm_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (term : LRootedForest α × LRootedForest α) : evalCoproductTerm (LForestAlgebra.Character.comapEraseLabels χ) (LForestAlgebra.Character.comapEraseLabels ψ) term = PTree.evalCoproductTerm χ ψ (eraseCoproductTerm term)

Pulling characters back along label erasure commutes with one coproduct-term evaluation.

theorem HopfAlgebras.PLTree.evalCoproductTerms_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (terms : List (LRootedForest α × LRootedForest α)) : evalCoproductTerms (LForestAlgebra.Character.comapEraseLabels χ) (LForestAlgebra.Character.comapEraseLabels ψ) terms = PTree.evalCoproductTerms χ ψ (List.map eraseCoproductTerm terms)

Pulling characters back along label erasure commutes with finite coproduct evaluation.

theorem HopfAlgebras.PLTree.evalCoproductTerm_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (χ ψ : LForestAlgebra.Character β R) (term : LRootedForest α × LRootedForest α) : evalCoproductTerm (LForestAlgebra.Character.comapMapLabels f χ) (LForestAlgebra.Character.comapMapLabels f ψ) term = evalCoproductTerm χ ψ (mapCoproductTerm f term)

Pulling characters back along relabelling commutes with one coproduct-term evaluation.

theorem HopfAlgebras.PLTree.evalCoproductTerms_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (χ ψ : LForestAlgebra.Character β R) (terms : List (LRootedForest α × LRootedForest α)) : evalCoproductTerms (LForestAlgebra.Character.comapMapLabels f χ) (LForestAlgebra.Character.comapMapLabels f ψ) terms = evalCoproductTerms χ ψ (List.map (mapCoproductTerm f) terms)

Pulling characters back along relabelling commutes with finite coproduct evaluation.

theorem HopfAlgebras.PLTree.evalCoproductTerm_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (x : α) (χ ψ : LForestAlgebra.Character α R) (term : RootedForest × RootedForest) : PTree.evalCoproductTerm (LForestAlgebra.Character.comapConstLabel x χ) (LForestAlgebra.Character.comapConstLabel x ψ) term = evalCoproductTerm χ ψ (constLabelCoproductTerm x term)

Pulling characters back along constant labelling commutes with one coproduct-term evaluation.

theorem HopfAlgebras.PLTree.evalCoproductTerms_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (x : α) (χ ψ : LForestAlgebra.Character α R) (terms : List (RootedForest × RootedForest)) : PTree.evalCoproductTerms (LForestAlgebra.Character.comapConstLabel x χ) (LForestAlgebra.Character.comapConstLabel x ψ) terms = evalCoproductTerms χ ψ (List.map (constLabelCoproductTerm x) terms)

Pulling characters back along constant labelling commutes with finite coproduct evaluation.

noncomputable def HopfAlgebras.PLTree.convolutionCoeff {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (t : PLTree α) : R

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

Equations

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

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

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

theorem HopfAlgebras.PLTree.convolutionCoeff_perm {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) {t u : PLTree α} (h : t.Perm u) : convolutionCoeff χ ψ t = convolutionCoeff χ ψ u

noncomputable def HopfAlgebras.PLTree.convolutionForestCoeff {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (ts : List (PLTree α)) : R

Multiplicative extension of labelled convolution coefficients to planar labelled forests.

Equations

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

theorem HopfAlgebras.PLTree.convolutionCoeff_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (t : PLTree α) : convolutionCoeff (LForestAlgebra.Character.comapEraseLabels χ) (LForestAlgebra.Character.comapEraseLabels ψ) t = PTree.convolutionCoeff χ ψ t.erase

Labelled convolution with characters pulled back by erasure is unlabelled convolution.

theorem HopfAlgebras.PLTree.convolutionForestCoeff_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (ts : List (PLTree α)) : convolutionForestCoeff (LForestAlgebra.Character.comapEraseLabels χ) (LForestAlgebra.Character.comapEraseLabels ψ) ts = PTree.convolutionForestCoeff χ ψ (List.map erase ts)

Labelled forest convolution pulled back by erasure is unlabelled forest convolution.

theorem HopfAlgebras.PLTree.convolutionCoeff_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (χ ψ : LForestAlgebra.Character β R) (t : PLTree α) : convolutionCoeff (LForestAlgebra.Character.comapMapLabels f χ) (LForestAlgebra.Character.comapMapLabels f ψ) t = convolutionCoeff χ ψ (map f t)

theorem HopfAlgebras.PLTree.convolutionForestCoeff_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (χ ψ : LForestAlgebra.Character β R) (ts : List (PLTree α)) : convolutionForestCoeff (LForestAlgebra.Character.comapMapLabels f χ) (LForestAlgebra.Character.comapMapLabels f ψ) ts = convolutionForestCoeff χ ψ (List.map (map f) ts)

theorem HopfAlgebras.PLTree.convolutionCoeff_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (x : α) (χ ψ : LForestAlgebra.Character α R) (t : PTree) : PTree.convolutionCoeff (LForestAlgebra.Character.comapConstLabel x χ) (LForestAlgebra.Character.comapConstLabel x ψ) t = convolutionCoeff χ ψ (constLabel x t)

theorem HopfAlgebras.PLTree.convolutionForestCoeff_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (x : α) (χ ψ : LForestAlgebra.Character α R) (ts : List PTree) : PTree.convolutionForestCoeff (LForestAlgebra.Character.comapConstLabel x χ) (LForestAlgebra.Character.comapConstLabel x ψ) ts = convolutionForestCoeff χ ψ (List.map (constLabel x) ts)

theorem HopfAlgebras.PLTree.convolutionCoeff_labelInvariant_eq {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] {χ ψ : LForestAlgebra.Character α R} (hχ : χ.LabelInvariant) (hψ : ψ.LabelInvariant) {t u : PLTree α} (htu : t.erase = u.erase) : convolutionCoeff χ ψ t = convolutionCoeff χ ψ u

If two labelled characters ignore labels, their planar convolution does too.

theorem HopfAlgebras.PLTree.convolutionForestCoeff_labelInvariant_eq {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] {χ ψ : LForestAlgebra.Character α R} (hχ : χ.LabelInvariant) (hψ : ψ.LabelInvariant) {ts us : List (PLTree α)} (hts : List.map erase ts = List.map erase us) : convolutionForestCoeff χ ψ ts = convolutionForestCoeff χ ψ us

If two labelled characters ignore labels, their planar forest convolution does too.

@[simp]

theorem HopfAlgebras.PLTree.convolutionForestCoeff_nil {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) : convolutionForestCoeff χ ψ [] = 1

@[simp]

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

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

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

theorem HopfAlgebras.PLTree.convolutionCoeff_unit_right {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (t : PLTree α) : convolutionCoeff χ (LForestAlgebra.counit α R) t = χ.evalForest (LRootedForest.singleton (LRootedTree.ofPLTree t))

theorem HopfAlgebras.PLTree.convolutionCoeff_unit_left {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (t : PLTree α) : convolutionCoeff (LForestAlgebra.counit α R) χ t = χ.evalForest (LRootedForest.singleton (LRootedTree.ofPLTree t))

theorem HopfAlgebras.PLTree.convolutionForestCoeff_unit_right {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (ts : List (PLTree α)) : convolutionForestCoeff χ (LForestAlgebra.counit α R) ts = χ.evalForest ↑(List.map LRootedTree.ofPLTree ts)

theorem HopfAlgebras.PLTree.convolutionForestCoeff_unit_left {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (ts : List (PLTree α)) : convolutionForestCoeff (LForestAlgebra.counit α R) χ ts = χ.evalForest ↑(List.map LRootedTree.ofPLTree ts)

noncomputable def HopfAlgebras.LForestTensorAlgebra.evalByCharacters {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) : LForestTensorAlgebra α R →ₐ[R] R

Evaluate tensor-coded labelled forest algebra terms by a pair of characters.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.evalByCharacters_ofPair {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (term : LRootedForest α × LRootedForest α) : (evalByCharacters χ ψ) (ofPair term) = PLTree.evalCoproductTerm χ ψ term

theorem HopfAlgebras.LForestTensorAlgebra.evalByCharacters_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (terms : List (LRootedForest α × LRootedForest α)) : (evalByCharacters χ ψ) (sumTerms terms) = PLTree.evalCoproductTerms χ ψ terms

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

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.evalByCharacters_labelledCoproduct {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (t : PLTree α) : (evalByCharacters χ ψ) t.labelledCoproduct = PLTree.convolutionCoeff χ ψ t

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.evalByCharacters_labelledCoproductList {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (ts : List (PLTree α)) : (evalByCharacters χ ψ) (PLTree.labelledCoproductList ts) = PLTree.convolutionForestCoeff χ ψ ts

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.evalByCharacters {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) : LForestTripleTensorAlgebra α R →ₐ[R] R

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

Equations

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

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.evalByCharacters_ofTriple {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (term : LRootedForest α × LRootedForest α × LRootedForest α) : (evalByCharacters χ ψ η) (ofTriple term) = PLTree.evalTripleCoproductTerm χ ψ η term

theorem HopfAlgebras.LForestTripleTensorAlgebra.evalByCharacters_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (terms : List (LRootedForest α × LRootedForest α × LRootedForest α)) : (evalByCharacters χ ψ η) (sumTerms terms) = PLTree.evalTripleCoproductTerms χ ψ η terms

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.evalByCharacters_includeLeftPair {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (x : LForestTensorAlgebra α R) : (evalByCharacters χ ψ η) (includeLeftPair x) = (LForestTensorAlgebra.evalByCharacters χ ψ) x

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.evalByCharacters_includeRightPair {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : LForestAlgebra.Character α R) (x : LForestTensorAlgebra α R) : (evalByCharacters χ ψ η) (includeRightPair x) = (LForestTensorAlgebra.evalByCharacters ψ η) x

noncomputable def HopfAlgebras.LRootedForest.convolutionCoeff {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (φ : LRootedForest α) : R

Character convolution evaluated on a non-planar labelled rooted forest.

Equations

• HopfAlgebras.LRootedForest.convolutionCoeff χ ψ φ = (HopfAlgebras.LForestTensorAlgebra.evalByCharacters χ ψ) φ.coproduct

@[simp]

theorem HopfAlgebras.LRootedForest.convolutionCoeff_zero {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) : convolutionCoeff χ ψ 0 = 1

@[simp]

theorem HopfAlgebras.LRootedForest.convolutionCoeff_empty {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) : convolutionCoeff χ ψ empty = 1

@[simp]

theorem HopfAlgebras.LRootedForest.convolutionCoeff_singleton {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (τ : LRootedTree α) : convolutionCoeff χ ψ (singleton τ) = PLTree.convolutionCoeff χ ψ (Quotient.out τ)

@[simp]

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

theorem HopfAlgebras.LRootedForest.convolutionCoeff_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (φ : LRootedForest α) : convolutionCoeff (LForestAlgebra.Character.comapEraseLabels χ) (LForestAlgebra.Character.comapEraseLabels ψ) φ = RootedForest.convolutionCoeff χ ψ φ.erase

theorem HopfAlgebras.LRootedForest.convolutionCoeff_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (χ ψ : LForestAlgebra.Character β R) (φ : LRootedForest α) : convolutionCoeff (LForestAlgebra.Character.comapMapLabels f χ) (LForestAlgebra.Character.comapMapLabels f ψ) φ = convolutionCoeff χ ψ (mapLabels f φ)

theorem HopfAlgebras.LRootedForest.convolutionCoeff_unit_right {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (φ : LRootedForest α) : convolutionCoeff χ (LForestAlgebra.counit α R) φ = χ.evalForest φ

theorem HopfAlgebras.LRootedForest.convolutionCoeff_unit_left {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (φ : LRootedForest α) : convolutionCoeff (LForestAlgebra.counit α R) χ φ = χ.evalForest φ

theorem HopfAlgebras.RootedForest.convolutionCoeff_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (x : α) (χ ψ : LForestAlgebra.Character α R) (φ : RootedForest) : convolutionCoeff (LForestAlgebra.Character.comapConstLabel x χ) (LForestAlgebra.Character.comapConstLabel x ψ) φ = LRootedForest.convolutionCoeff χ ψ (LRootedForest.constLabel x φ)

noncomputable def HopfAlgebras.LRootedTree.convolutionCoeff {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (τ : LRootedTree α) : R

Character convolution coefficient on a non-planar labelled rooted tree.

Equations

• HopfAlgebras.LRootedTree.convolutionCoeff χ ψ τ = (HopfAlgebras.LForestTensorAlgebra.evalByCharacters χ ψ) τ.coproduct

theorem HopfAlgebras.LRootedTree.convolutionCoeff_eq_singleton {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (τ : LRootedTree α) : convolutionCoeff χ ψ τ = LRootedForest.convolutionCoeff χ ψ (LRootedForest.singleton τ)

theorem HopfAlgebras.LRootedTree.convolutionCoeff_out {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (τ : LRootedTree α) : convolutionCoeff χ ψ τ = PLTree.convolutionCoeff χ ψ (Quotient.out τ)

theorem HopfAlgebras.LRootedTree.convolutionCoeff_ofPLTree {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : LForestAlgebra.Character α R) (t : PLTree α) : convolutionCoeff χ ψ (ofPLTree t) = PLTree.convolutionCoeff χ ψ t

theorem HopfAlgebras.LRootedTree.convolutionCoeff_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) (τ : LRootedTree α) : convolutionCoeff (LForestAlgebra.Character.comapEraseLabels χ) (LForestAlgebra.Character.comapEraseLabels ψ) τ = RootedTree.convolutionCoeff χ ψ τ.erase

theorem HopfAlgebras.LRootedTree.convolutionCoeff_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (χ ψ : LForestAlgebra.Character β R) (τ : LRootedTree α) : convolutionCoeff (LForestAlgebra.Character.comapMapLabels f χ) (LForestAlgebra.Character.comapMapLabels f ψ) τ = convolutionCoeff χ ψ (map f τ)

theorem HopfAlgebras.LRootedTree.convolutionCoeff_unit_right {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (τ : LRootedTree α) : convolutionCoeff χ (LForestAlgebra.counit α R) τ = χ.evalForest (LRootedForest.singleton τ)

theorem HopfAlgebras.LRootedTree.convolutionCoeff_unit_left {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (τ : LRootedTree α) : convolutionCoeff (LForestAlgebra.counit α R) χ τ = χ.evalForest (LRootedForest.singleton τ)

theorem HopfAlgebras.RootedTree.convolutionCoeff_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (x : α) (χ ψ : LForestAlgebra.Character α R) (τ : RootedTree) : convolutionCoeff (LForestAlgebra.Character.comapConstLabel x χ) (LForestAlgebra.Character.comapConstLabel x ψ) τ = LRootedTree.convolutionCoeff χ ψ (LRootedTree.constLabel x τ)

noncomputable def HopfAlgebras.LForestAlgebra.Character.unit (α : Type u) (R : Type v) [CommSemiring R] : Character α R

The identity labelled character for convolution.

Equations

• HopfAlgebras.LForestAlgebra.Character.unit α R = HopfAlgebras.LForestAlgebra.counit α R

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.unit_evalForest {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : (unit α R).evalForest φ = counitCoeff φ

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

@[simp]

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

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

Labelled character convolution induced by the labelled BCK coproduct.

Equations

• χ.convolution ψ = (HopfAlgebras.LForestTensorAlgebra.evalByCharacters χ ψ).comp (HopfAlgebras.LForestAlgebra.coproduct α R)

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.convolution_evalForest {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : Character α R) (φ : LRootedForest α) : (χ.convolution ψ).evalForest φ = LRootedForest.convolutionCoeff χ ψ φ

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.convolution_ofForest {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : Character α R) (φ : LRootedForest α) : (χ.convolution ψ) (ofForest φ) = LRootedForest.convolutionCoeff χ ψ φ

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

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

theorem HopfAlgebras.LForestAlgebra.Character.convolution_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ ψ : ForestAlgebra.Character R) : (comapEraseLabels χ).convolution (comapEraseLabels ψ) = comapEraseLabels (χ.convolution ψ)

theorem HopfAlgebras.LForestAlgebra.Character.convolution_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (χ ψ : Character β R) : (comapMapLabels f χ).convolution (comapMapLabels f ψ) = comapMapLabels f (χ.convolution ψ)

theorem HopfAlgebras.LForestAlgebra.Character.convolution_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (x : α) (χ ψ : Character α R) : (comapConstLabel x χ).convolution (comapConstLabel x ψ) = comapConstLabel x (χ.convolution ψ)

theorem HopfAlgebras.LForestAlgebra.Character.LabelInvariant.convolution {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] {χ ψ : Character α R} (hχ : χ.LabelInvariant) (hψ : ψ.LabelInvariant) : (χ.convolution ψ).LabelInvariant

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv_convolution {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] (χ ψ : ForestAlgebra.Character R) : labelInvariantEquiv (χ.convolution ψ) = ⟨(↑(labelInvariantEquiv χ)).convolution ↑(labelInvariantEquiv ψ), ⋯⟩

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv_symm_convolution {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] (χ ψ : { χ : Character α R // χ.LabelInvariant }) : labelInvariantEquiv.symm ⟨(↑χ).convolution ↑ψ, ⋯⟩ = (labelInvariantEquiv.symm χ).convolution (labelInvariantEquiv.symm ψ)

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

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

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

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

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

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

theorem HopfAlgebras.LForestAlgebra.Character.evalByCharacters_coproductLeft {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : Character α R) (x : LForestTensorAlgebra α R) : (LForestTripleTensorAlgebra.evalByCharacters χ ψ η) (LForestTripleTensorAlgebra.coproductLeft x) = (LForestTensorAlgebra.evalByCharacters (χ.convolution ψ) η) x

theorem HopfAlgebras.LForestAlgebra.Character.evalByCharacters_coproductRight {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : Character α R) (x : LForestTensorAlgebra α R) : (LForestTripleTensorAlgebra.evalByCharacters χ ψ η) (LForestTripleTensorAlgebra.coproductRight x) = (LForestTensorAlgebra.evalByCharacters χ (ψ.convolution η)) x

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

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

theorem HopfAlgebras.LForestAlgebra.Character.evalTripleCoproductTerms_coproductLeftTerms {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : Character α R) (terms : List (LRootedForest α × LRootedForest α)) : PLTree.evalTripleCoproductTerms χ ψ η (LForestTripleTensorAlgebra.coproductLeftTerms terms) = PLTree.evalCoproductTerms (χ.convolution ψ) η terms

theorem HopfAlgebras.LForestAlgebra.Character.evalTripleCoproductTerms_coproductRightTerms {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : Character α R) (terms : List (LRootedForest α × LRootedForest α)) : PLTree.evalTripleCoproductTerms χ ψ η (LForestTripleTensorAlgebra.coproductRightTerms terms) = PLTree.evalCoproductTerms χ (ψ.convolution η) terms

theorem HopfAlgebras.LForestAlgebra.Character.evalTripleCoproductTerms_coproductLeftTerms_pltree {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : Character α R) (t : PLTree α) : PLTree.evalTripleCoproductTerms χ ψ η (LForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms) = PLTree.convolutionCoeff (χ.convolution ψ) η t

theorem HopfAlgebras.LForestAlgebra.Character.evalTripleCoproductTerms_coproductRightTerms_pltree {α : Type u} {R : Type v} [CommSemiring R] (χ ψ η : Character α R) (t : PLTree α) : PLTree.evalTripleCoproductTerms χ ψ η (LForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms) = PLTree.convolutionCoeff χ (ψ.convolution η) t

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

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

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

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

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

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

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

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

theorem HopfAlgebras.LForestAlgebra.Character.convolution_assoc_of_coproduct_eq_singletons {α : Type u} {R : Type v} [CommSemiring R] (hcoassoc : ∀ (τ : LRootedTree α), (coproductLeft α R) (ofForest (LRootedForest.singleton τ)) = (coproductRight α R) (ofForest (LRootedForest.singleton τ))) (χ ψ η : Character α R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.LForestAlgebra.Character.convolution_assoc_of_coproduct_eq_pltree_singletons {α : Type u} {R : Type v} [CommSemiring R] (hcoassoc : ∀ (t : PLTree α), (coproductLeft α R) (ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t))) = (coproductRight α R) (ofForest (LRootedForest.singleton (LRootedTree.ofPLTree t)))) (χ ψ η : Character α R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.LForestAlgebra.Character.convolution_assoc_of_coproduct_eq_pltree_coproductTerms {α : Type u} {R : Type v} [CommSemiring R] (hcoassoc : ∀ (t : PLTree α), LForestTripleTensorAlgebra.sumTerms (LForestTripleTensorAlgebra.coproductLeftTerms t.coproductTerms) = LForestTripleTensorAlgebra.sumTerms (LForestTripleTensorAlgebra.coproductRightTerms t.coproductTerms)) (χ ψ η : Character α R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

theorem HopfAlgebras.LForestAlgebra.Character.convolution_assoc_of_nestedCoproductTerms {α : Type u} {R : Type v} [CommSemiring R] (hcoassoc : ∀ (t : PLTree α), LForestTripleTensorAlgebra.sumTerms t.nestedCoproductLeftTerms = LForestTripleTensorAlgebra.sumTerms t.nestedCoproductRightTerms) (χ ψ η : Character α R) : (χ.convolution ψ).convolution η = χ.convolution (ψ.convolution η)

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

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

noncomputable instance HopfAlgebras.LForestAlgebra.Character.instLabelInvariantMonoid {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] : Monoid { χ : Character α R // χ.LabelInvariant }

Equations

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

noncomputable def HopfAlgebras.LForestAlgebra.Character.labelInvariantMulEquiv {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] : ForestAlgebra.Character R ≃* { χ : Character α R // χ.LabelInvariant }

Equations

• HopfAlgebras.LForestAlgebra.Character.labelInvariantMulEquiv = { toEquiv := HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv, map_mul' := ⋯ }