Dual Convolution

This file defines convolution of linear functionals on the rooted-forest Hopf algebras. It also records the general left inverse identity induced by the recursive antipode after evaluating by a character.

@[reducible, inline]

abbrev HopfAlgebras.ForestAlgebra.LinearFunctional (R : Type u) [CommSemiring R] : Type u

Linear functionals on the rooted-forest algebra.

Equations

• HopfAlgebras.ForestAlgebra.LinearFunctional R = (HopfAlgebras.ForestAlgebra R →ₗ[R] R)

noncomputable def HopfAlgebras.ForestTensorAlgebra.evalByLinearMaps {R : Type u} [CommSemiring R] (f g : ForestAlgebra.LinearFunctional R) : ForestTensorAlgebra R →ₗ[R] R

Evaluate a tensor-coded forest pair by two linear functionals.

Equations

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

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.evalByLinearMaps_ofPair {R : Type u} [CommSemiring R] (f g : ForestAlgebra.LinearFunctional R) (term : RootedForest × RootedForest) : (evalByLinearMaps f g) (ofPair term) = f (ForestAlgebra.ofForest term.1) * g (ForestAlgebra.ofForest term.2)

theorem HopfAlgebras.ForestTensorAlgebra.evalByLinearMaps_sumTerms {R : Type u} [CommSemiring R] (f g : ForestAlgebra.LinearFunctional R) (terms : List (RootedForest × RootedForest)) : (evalByLinearMaps f g) (sumTerms terms) = (List.map (fun (term : RootedForest × RootedForest) => f (ForestAlgebra.ofForest term.1) * g (ForestAlgebra.ofForest term.2)) terms).sum

theorem HopfAlgebras.ForestTensorAlgebra.evalByLinearMaps_compAntipode_ofCharacter {R : Type u} [CommRing R] (χ : ForestAlgebra.Character R) : evalByLinearMaps (AlgHom.toLinearMap χ ∘ₗ ForestAlgebra.antipode) (AlgHom.toLinearMap χ) = AlgHom.toLinearMap χ ∘ₗ antipodeLeft

theorem HopfAlgebras.ForestTensorAlgebra.evalByLinearMaps_compRightAntipode_ofCharacter {R : Type u} [CommRing R] (χ : ForestAlgebra.Character R) : evalByLinearMaps (AlgHom.toLinearMap χ) (AlgHom.toLinearMap χ ∘ₗ ForestAlgebra.rightAntipode) = AlgHom.toLinearMap χ ∘ₗ antipodeRight

noncomputable def HopfAlgebras.ForestAlgebra.LinearFunctional.counit (R : Type u) [CommSemiring R] : LinearFunctional R

The counit as a linear functional.

Equations

• HopfAlgebras.ForestAlgebra.LinearFunctional.counit R = (HopfAlgebras.ForestAlgebra.counit R).toLinearMap

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

The linear functional underlying a forest-algebra character.

Equations

• HopfAlgebras.ForestAlgebra.LinearFunctional.ofCharacter χ = AlgHom.toLinearMap χ

noncomputable def HopfAlgebras.ForestAlgebra.LinearFunctional.evalForest {R : Type u} [CommSemiring R] (f : LinearFunctional R) (φ : RootedForest) : R

Evaluate a linear functional on the forest monomial associated to a rooted forest.

Equations

• f.evalForest φ = f (HopfAlgebras.ForestAlgebra.ofForest φ)

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.evalForest_counit {R : Type u} [CommSemiring R] (φ : RootedForest) : (counit R).evalForest φ = counitCoeff φ

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.evalForest_ofCharacter {R : Type u} [CommSemiring R] (χ : Character R) (φ : RootedForest) : (ofCharacter χ).evalForest φ = χ.evalForest φ

noncomputable def HopfAlgebras.ForestAlgebra.LinearFunctional.compAntipode {R : Type u} [CommRing R] (f : LinearFunctional R) : LinearFunctional R

Compose a linear functional with the recursive antipode.

Equations

• f.compAntipode = f ∘ₗ HopfAlgebras.ForestAlgebra.antipode

noncomputable def HopfAlgebras.ForestAlgebra.LinearFunctional.compRightAntipode {R : Type u} [CommRing R] (f : LinearFunctional R) : LinearFunctional R

Compose a linear functional with the right-recursive antipode.

Equations

• f.compRightAntipode = f ∘ₗ HopfAlgebras.ForestAlgebra.rightAntipode

noncomputable def HopfAlgebras.ForestAlgebra.LinearFunctional.convolution {R : Type u} [CommSemiring R] (f g : LinearFunctional R) : LinearFunctional R

Convolution of linear functionals induced by the BCK coproduct.

Equations

• f.convolution g = HopfAlgebras.ForestTensorAlgebra.evalByLinearMaps f g ∘ₗ (HopfAlgebras.ForestAlgebra.coproduct R).toLinearMap

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_ofForest {R : Type u} [CommSemiring R] (f g : LinearFunctional R) (φ : RootedForest) : (f.convolution g) (ofForest φ) = (List.map (fun (term : RootedForest × RootedForest) => f (ofForest term.1) * g (ofForest term.2)) φ.coproductTerms).sum

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.evalForest_convolution {R : Type u} [CommSemiring R] (f g : LinearFunctional R) (φ : RootedForest) : (f.convolution g).evalForest φ = (List.map (fun (term : RootedForest × RootedForest) => f.evalForest term.1 * g.evalForest term.2) φ.coproductTerms).sum

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.evalForest_smul {R : Type u} [CommSemiring R] (c : R) (f : LinearFunctional R) (φ : RootedForest) : (c • f).evalForest φ = c * f.evalForest φ

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.evalForest_sum {R : Type u} [CommSemiring R] (fs : List (LinearFunctional R)) (φ : RootedForest) : fs.sum.evalForest φ = (List.map (fun (f : LinearFunctional R) => f.evalForest φ) fs).sum

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.ext_evalForest {R : Type u} [CommSemiring R] {f g : LinearFunctional R} (h : ∀ (φ : RootedForest), f.evalForest φ = g.evalForest φ) : f = g

Linear functionals agreeing on every forest monomial are equal.

def HopfAlgebras.ForestAlgebra.LinearFunctional.AgreeUpToOrder {R : Type u} [CommSemiring R] (f g : LinearFunctional R) (n : ℕ) : Prop

Two forest linear functionals agree on all forests of order at most n.

Equations

• f.AgreeUpToOrder g n = ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → f.evalForest φ = g.evalForest φ

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.agreeUpToOrder_refl {R : Type u} [CommSemiring R] (f : LinearFunctional R) (n : ℕ) : f.AgreeUpToOrder f n

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.AgreeUpToOrder.symm {R : Type u} [CommSemiring R] {f g : LinearFunctional R} {n : ℕ} (h : f.AgreeUpToOrder g n) : g.AgreeUpToOrder f n

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.AgreeUpToOrder.trans {R : Type u} [CommSemiring R] {f g h : LinearFunctional R} {n : ℕ} (hfg : f.AgreeUpToOrder g n) (hgh : g.AgreeUpToOrder h n) : f.AgreeUpToOrder h n

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.AgreeUpToOrder.mono {R : Type u} [CommSemiring R] {f g : LinearFunctional R} {m n : ℕ} (h : f.AgreeUpToOrder g n) (hmn : m ≤ n) : f.AgreeUpToOrder g m

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.AgreeUpToOrder.convolution {R : Type u} [CommSemiring R] {f f' g g' : LinearFunctional R} {n : ℕ} (hf : f.AgreeUpToOrder f' n) (hg : g.AgreeUpToOrder g' n) : (f.convolution g).AgreeUpToOrder (f'.convolution g') n

noncomputable def HopfAlgebras.ForestTripleTensorAlgebra.evalByLinearMaps {R : Type u} [CommSemiring R] (f g h : ForestAlgebra.LinearFunctional R) : ForestTripleTensorAlgebra R →ₗ[R] R

Evaluate a triple tensor-coded forest term by three linear functionals.

Equations

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

@[simp]

theorem HopfAlgebras.ForestTripleTensorAlgebra.evalByLinearMaps_ofTriple {R : Type u} [CommSemiring R] (f g h : ForestAlgebra.LinearFunctional R) (term : RootedForest × RootedForest × RootedForest) : (evalByLinearMaps f g h) (ofTriple term) = f (ForestAlgebra.ofForest term.1) * g (ForestAlgebra.ofForest term.2.1) * h (ForestAlgebra.ofForest term.2.2)

theorem HopfAlgebras.ForestTripleTensorAlgebra.evalByLinearMaps_sumTerms {R : Type u} [CommSemiring R] (f g h : ForestAlgebra.LinearFunctional R) (terms : List (RootedForest × RootedForest × RootedForest)) : (evalByLinearMaps f g h) (sumTerms terms) = (List.map (fun (term : RootedForest × RootedForest × RootedForest) => f (ForestAlgebra.ofForest term.1) * g (ForestAlgebra.ofForest term.2.1) * h (ForestAlgebra.ofForest term.2.2)) terms).sum

theorem HopfAlgebras.ForestTripleTensorAlgebra.evalByLinearMaps_coproductLeft {R : Type u} [CommSemiring R] (f g h : ForestAlgebra.LinearFunctional R) (x : ForestTensorAlgebra R) : (evalByLinearMaps f g h) (coproductLeft x) = (ForestTensorAlgebra.evalByLinearMaps (f.convolution g) h) x

theorem HopfAlgebras.ForestTripleTensorAlgebra.evalByLinearMaps_coproductRight {R : Type u} [CommSemiring R] (f g h : ForestAlgebra.LinearFunctional R) (x : ForestTensorAlgebra R) : (evalByLinearMaps f g h) (coproductRight x) = (ForestTensorAlgebra.evalByLinearMaps f (g.convolution h)) x

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_counit_left {R : Type u} [CommSemiring R] (f : LinearFunctional R) : (counit R).convolution f = f

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_counit_right {R : Type u} [CommSemiring R] (f : LinearFunctional R) : f.convolution (counit R) = f

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_zero_left {R : Type u} [CommSemiring R] (f : LinearFunctional R) : convolution 0 f = 0

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_zero_right {R : Type u} [CommSemiring R] (f : LinearFunctional R) : f.convolution 0 = 0

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_assoc_of_coproduct_eq {R : Type u} [CommSemiring R] (hcoassoc : ∀ (x : ForestAlgebra R), (coproductLeft R) x = (coproductRight R) x) (f g h : LinearFunctional R) : (f.convolution g).convolution h = f.convolution (g.convolution h)

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_assoc_of_coproductLeft_eq_coproductRight {R : Type u} [CommSemiring R] (hcoassoc : coproductLeft R = coproductRight R) (f g h : LinearFunctional R) : (f.convolution g).convolution h = f.convolution (g.convolution h)

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_assoc {R : Type u} [CommSemiring R] (f g h : LinearFunctional R) : (f.convolution g).convolution h = f.convolution (g.convolution h)

def HopfAlgebras.ForestAlgebra.LinearFunctional.convolutionPower {R : Type u} [CommSemiring R] (f : LinearFunctional R) : ℕ → LinearFunctional R

Convolution powers of a linear functional, with the counit as the zeroth power.

Equations

• f.convolutionPower 0 = HopfAlgebras.ForestAlgebra.LinearFunctional.counit R
• f.convolutionPower n.succ = f.convolution (f.convolutionPower n)

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolutionPower_zero {R : Type u} [CommSemiring R] (f : LinearFunctional R) : f.convolutionPower 0 = counit R

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolutionPower_succ {R : Type u} [CommSemiring R] (f : LinearFunctional R) (n : ℕ) : f.convolutionPower (n + 1) = f.convolution (f.convolutionPower n)

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolutionPower_one {R : Type u} [CommSemiring R] (f : LinearFunctional R) : f.convolutionPower 1 = f

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolutionPower_add {R : Type u} [CommSemiring R] (f : LinearFunctional R) (m n : ℕ) : f.convolutionPower (m + n) = (f.convolutionPower m).convolution (f.convolutionPower n)

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolutionPower_succ_right {R : Type u} [CommSemiring R] (f : LinearFunctional R) (n : ℕ) : f.convolutionPower (n + 1) = (f.convolutionPower n).convolution f

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolutionPower_zero_succ {R : Type u} [CommSemiring R] (n : ℕ) : convolutionPower 0 (n + 1) = 0

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolutionPower_counit {R : Type u} [CommSemiring R] (n : ℕ) : (counit R).convolutionPower n = counit R

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.AgreeUpToOrder.convolutionPower {R : Type u} [CommSemiring R] {f g : LinearFunctional R} {n : ℕ} (h : f.AgreeUpToOrder g n) (k : ℕ) : (f.convolutionPower k).AgreeUpToOrder (g.convolutionPower k) n

noncomputable def HopfAlgebras.ForestAlgebra.LinearFunctional.augmentationPart {R : Type u} [CommRing R] (χ : Character R) : LinearFunctional R

The augmentation part of a forest character, viewed as a linear functional.

Equations

• HopfAlgebras.ForestAlgebra.LinearFunctional.augmentationPart χ = HopfAlgebras.ForestAlgebra.LinearFunctional.ofCharacter χ - HopfAlgebras.ForestAlgebra.LinearFunctional.counit R

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.augmentationPart_eval_empty {R : Type u} [CommRing R] (χ : Character R) : (augmentationPart χ).evalForest RootedForest.empty = 0

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.agreeUpToOrder_augmentationPart {R : Type u} [CommRing R] {χ ψ : Character R} {n : ℕ} (h : ∀ (φ : RootedForest), φ.order ≤ n → χ.evalForest φ = ψ.evalForest φ) : (augmentationPart χ).AgreeUpToOrder (augmentationPart ψ) n

noncomputable def HopfAlgebras.ForestAlgebra.LinearFunctional.logCharacterTruncated {R : Type u} [Field R] (χ : Character R) (n : ℕ) : LinearFunctional R

The truncated convolution logarithm of a forest character.

Equations

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

@[simp]

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.logCharacterTruncated_zero {R : Type u} [Field R] (χ : Character R) : logCharacterTruncated χ 0 = 0

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.logCharacterTruncated_evalForest {R : Type u} [Field R] (χ : Character R) (n : ℕ) (φ : RootedForest) : (logCharacterTruncated χ n).evalForest φ = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((augmentationPart χ).convolutionPower k).evalForest φ) (List.range n)).sum

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.agreeUpToOrder_logCharacterTruncated {R : Type u} [Field R] {χ ψ : Character R} {m n : ℕ} (h : ∀ (φ : RootedForest), φ.order ≤ n → χ.evalForest φ = ψ.evalForest φ) : (logCharacterTruncated χ m).AgreeUpToOrder (logCharacterTruncated ψ m) n

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

theorem HopfAlgebras.ForestAlgebra.LinearFunctional.convolution_compRightAntipode_ofCharacter_right {R : Type u} [CommRing R] (χ : Character R) : (ofCharacter χ).convolution (ofCharacter χ).compRightAntipode = counit R

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

noncomputable def HopfAlgebras.ForestAlgebra.Character.inverseLinearFunctional {R : Type u} [CommRing R] (χ : Character R) : LinearFunctional R

The antipode-composed linear functional that gives the convolution inverse of a character.

Equations

• χ.inverseLinearFunctional = (HopfAlgebras.ForestAlgebra.LinearFunctional.ofCharacter χ).compAntipode

theorem HopfAlgebras.ForestAlgebra.Character.convolution_inverseLinearFunctional_left {R : Type u} [CommRing R] (χ : Character R) : χ.inverseLinearFunctional.convolution (LinearFunctional.ofCharacter χ) = LinearFunctional.counit R

theorem HopfAlgebras.ForestAlgebra.Character.convolution_inverseLinearFunctional_right {R : Type u} [CommRing R] (χ : Character R) : (LinearFunctional.ofCharacter χ).convolution χ.inverseLinearFunctional = LinearFunctional.counit R

@[reducible, inline]

abbrev HopfAlgebras.LForestAlgebra.LinearFunctional (α : Type u) (R : Type v) [CommSemiring R] : Type (max u v)

Linear functionals on the labelled rooted-forest algebra.

Equations

• HopfAlgebras.LForestAlgebra.LinearFunctional α R = (HopfAlgebras.LForestAlgebra α R →ₗ[R] R)

noncomputable def HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps {α : Type u} {R : Type v} [CommSemiring R] (f g : LForestAlgebra.LinearFunctional α R) : LForestTensorAlgebra α R →ₗ[R] R

Evaluate a labelled tensor-coded forest pair by two linear functionals.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps_ofPair {α : Type u} {R : Type v} [CommSemiring R] (f g : LForestAlgebra.LinearFunctional α R) (term : LRootedForest α × LRootedForest α) : (evalByLinearMaps f g) (ofPair term) = f (LForestAlgebra.ofForest term.1) * g (LForestAlgebra.ofForest term.2)

theorem HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (f g : LForestAlgebra.LinearFunctional α R) (terms : List (LRootedForest α × LRootedForest α)) : (evalByLinearMaps f g) (sumTerms terms) = (List.map (fun (term : LRootedForest α × LRootedForest α) => f (LForestAlgebra.ofForest term.1) * g (LForestAlgebra.ofForest term.2)) terms).sum

theorem HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps_erase {α : Type u} {R : Type v} [CommSemiring R] (f g : ForestAlgebra.LinearFunctional R) (x : LForestTensorAlgebra α R) : (ForestTensorAlgebra.evalByLinearMaps f g) x.erase = (evalByLinearMaps (f ∘ₗ (LForestAlgebra.eraseLabels R).toLinearMap) (g ∘ₗ (LForestAlgebra.eraseLabels R).toLinearMap)) x

theorem HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps_constLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) (f g : LForestAlgebra.LinearFunctional α R) (x : ForestTensorAlgebra R) : (evalByLinearMaps f g) (constLabel a x) = (ForestTensorAlgebra.evalByLinearMaps (f ∘ₗ (LForestAlgebra.constLabel a R).toLinearMap) (g ∘ₗ (LForestAlgebra.constLabel a R).toLinearMap)) x

theorem HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps_mapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (labelMap : α → β) (f g : LForestAlgebra.LinearFunctional β R) (x : LForestTensorAlgebra α R) : (evalByLinearMaps f g) (mapLabels labelMap x) = (evalByLinearMaps (f ∘ₗ (LForestAlgebra.mapLabels R labelMap).toLinearMap) (g ∘ₗ (LForestAlgebra.mapLabels R labelMap).toLinearMap)) x

theorem HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps_compAntipode_ofCharacter {α : Type u} {R : Type v} [CommRing R] (χ : LForestAlgebra.Character α R) : evalByLinearMaps (AlgHom.toLinearMap χ ∘ₗ LForestAlgebra.antipode) (AlgHom.toLinearMap χ) = AlgHom.toLinearMap χ ∘ₗ antipodeLeft

theorem HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps_compRightAntipode_ofCharacter {α : Type u} {R : Type v} [CommRing R] (χ : LForestAlgebra.Character α R) : evalByLinearMaps (AlgHom.toLinearMap χ) (AlgHom.toLinearMap χ ∘ₗ LForestAlgebra.rightAntipode) = AlgHom.toLinearMap χ ∘ₗ antipodeRight

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

The labelled counit as a linear functional.

Equations

• HopfAlgebras.LForestAlgebra.LinearFunctional.counit α R = (HopfAlgebras.LForestAlgebra.counit α R).toLinearMap

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

The linear functional underlying a labelled forest-algebra character.

Equations

• HopfAlgebras.LForestAlgebra.LinearFunctional.ofCharacter χ = AlgHom.toLinearMap χ

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) (φ : LRootedForest α) : R

Evaluate a labelled linear functional on the monomial associated to a labelled forest.

Equations

• f.evalForest φ = f (HopfAlgebras.LForestAlgebra.ofForest φ)

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest_counit {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) : (counit α R).evalForest φ = counitCoeff φ

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest_ofCharacter {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) (φ : LRootedForest α) : (ofCharacter χ).evalForest φ = χ.evalForest φ

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (ℓ : LinearFunctional β R) : LinearFunctional α R

Pull a labelled linear functional back along a relabelling map.

Equations

• HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels f ℓ = ℓ ∘ₗ (HopfAlgebras.LForestAlgebra.mapLabels R f).toLinearMap

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (ℓ : LinearFunctional β R) (φ : LRootedForest α) : (comapMapLabels f ℓ).evalForest φ = ℓ.evalForest (LRootedForest.mapLabels f φ)

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels_zero {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) : comapMapLabels f 0 = 0

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels_add {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (ℓ m : LinearFunctional β R) : comapMapLabels f (ℓ + m) = comapMapLabels f ℓ + comapMapLabels f m

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels_smul {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (c : R) (ℓ : LinearFunctional β R) : comapMapLabels f (c • ℓ) = c • comapMapLabels f ℓ

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels_sum {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (ℓs : List (LinearFunctional β R)) : comapMapLabels f ℓs.sum = (List.map (comapMapLabels f) ℓs).sum

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (ℓ : ForestAlgebra.LinearFunctional R) : LinearFunctional α R

Pull an unlabelled linear functional back by forgetting labels.

Equations

• HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels ℓ = ℓ ∘ₗ (HopfAlgebras.LForestAlgebra.eraseLabels R).toLinearMap

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (ℓ : ForestAlgebra.LinearFunctional R) (φ : LRootedForest α) : (comapEraseLabels ℓ).evalForest φ = ℓ.evalForest φ.erase

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels_zero {α : Type u} {R : Type v} [CommSemiring R] : comapEraseLabels 0 = 0

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels_add {α : Type u} {R : Type v} [CommSemiring R] (ℓ m : ForestAlgebra.LinearFunctional R) : comapEraseLabels (ℓ + m) = comapEraseLabels ℓ + comapEraseLabels m

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels_smul {α : Type u} {R : Type v} [CommSemiring R] (c : R) (ℓ : ForestAlgebra.LinearFunctional R) : comapEraseLabels (c • ℓ) = c • comapEraseLabels ℓ

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels_sum {α : Type u} {R : Type v} [CommSemiring R] (ℓs : List (ForestAlgebra.LinearFunctional R)) : comapEraseLabels ℓs.sum = (List.map comapEraseLabels ℓs).sum

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) (ℓ : LinearFunctional α R) : ForestAlgebra.LinearFunctional R

Pull a labelled linear functional back along constant labelling.

Equations

• HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel a ℓ = ℓ ∘ₗ (HopfAlgebras.LForestAlgebra.constLabel a R).toLinearMap

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) (ℓ : LinearFunctional α R) (φ : RootedForest) : (comapConstLabel a ℓ).evalForest φ = ℓ.evalForest (LRootedForest.constLabel a φ)

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel_zero {α : Type u} {R : Type v} [CommSemiring R] (a : α) : comapConstLabel a 0 = 0

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel_add {α : Type u} {R : Type v} [CommSemiring R] (a : α) (ℓ m : LinearFunctional α R) : comapConstLabel a (ℓ + m) = comapConstLabel a ℓ + comapConstLabel a m

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel_smul {α : Type u} {R : Type v} [CommSemiring R] (a : α) (c : R) (ℓ : LinearFunctional α R) : comapConstLabel a (c • ℓ) = c • comapConstLabel a ℓ

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel_sum {α : Type u} {R : Type v} [CommSemiring R] (a : α) (ℓs : List (LinearFunctional α R)) : comapConstLabel a ℓs.sum = (List.map (comapConstLabel a) ℓs).sum

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.compAntipode {α : Type u} {R : Type v} [CommRing R] (f : LinearFunctional α R) : LinearFunctional α R

Compose a labelled linear functional with the recursive antipode.

Equations

• f.compAntipode = f ∘ₗ HopfAlgebras.LForestAlgebra.antipode

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.compRightAntipode {α : Type u} {R : Type v} [CommRing R] (f : LinearFunctional α R) : LinearFunctional α R

Compose a labelled linear functional with the right-recursive antipode.

Equations

• f.compRightAntipode = f ∘ₗ HopfAlgebras.LForestAlgebra.rightAntipode

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.convolution {α : Type u} {R : Type v} [CommSemiring R] (f g : LinearFunctional α R) : LinearFunctional α R

Convolution of labelled linear functionals induced by the labelled BCK coproduct.

Equations

• f.convolution g = HopfAlgebras.LForestTensorAlgebra.evalByLinearMaps f g ∘ₗ (HopfAlgebras.LForestAlgebra.coproduct α R).toLinearMap

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_ofForest {α : Type u} {R : Type v} [CommSemiring R] (f g : LinearFunctional α R) (φ : LRootedForest α) : (f.convolution g) (ofForest φ) = (List.map (fun (term : LRootedForest α × LRootedForest α) => f (ofForest term.1) * g (ofForest term.2)) φ.coproductTerms).sum

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest_convolution {α : Type u} {R : Type v} [CommSemiring R] (f g : LinearFunctional α R) (φ : LRootedForest α) : (f.convolution g).evalForest φ = (List.map (fun (term : LRootedForest α × LRootedForest α) => f.evalForest term.1 * g.evalForest term.2) φ.coproductTerms).sum

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest_smul {α : Type u} {R : Type v} [CommSemiring R] (c : R) (f : LinearFunctional α R) (φ : LRootedForest α) : (c • f).evalForest φ = c * f.evalForest φ

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.evalForest_sum {α : Type u} {R : Type v} [CommSemiring R] (fs : List (LinearFunctional α R)) (φ : LRootedForest α) : fs.sum.evalForest φ = (List.map (fun (f : LinearFunctional α R) => f.evalForest φ) fs).sum

def HopfAlgebras.LForestAlgebra.LinearFunctional.AgreeUpToOrder {α : Type u} {R : Type v} [CommSemiring R] (f g : LinearFunctional α R) (n : ℕ) : Prop

Two labelled forest linear functionals agree on all forests of order at most n.

Equations

• f.AgreeUpToOrder g n = ∀ (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → f.evalForest φ = g.evalForest φ

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.agreeUpToOrder_refl {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) (n : ℕ) : f.AgreeUpToOrder f n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.AgreeUpToOrder.symm {α : Type u} {R : Type v} [CommSemiring R] {f g : LinearFunctional α R} {n : ℕ} (h : f.AgreeUpToOrder g n) : g.AgreeUpToOrder f n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.AgreeUpToOrder.trans {α : Type u} {R : Type v} [CommSemiring R] {f g h : LinearFunctional α R} {n : ℕ} (hfg : f.AgreeUpToOrder g n) (hgh : g.AgreeUpToOrder h n) : f.AgreeUpToOrder h n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.AgreeUpToOrder.mono {α : Type u} {R : Type v} [CommSemiring R] {f g : LinearFunctional α R} {m n : ℕ} (h : f.AgreeUpToOrder g n) (hmn : m ≤ n) : f.AgreeUpToOrder g m

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.AgreeUpToOrder.convolution {α : Type u} {R : Type v} [CommSemiring R] {f f' g g' : LinearFunctional α R} {n : ℕ} (hf : f.AgreeUpToOrder f' n) (hg : g.AgreeUpToOrder g' n) : (f.convolution g).AgreeUpToOrder (f'.convolution g') n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_comp_eraseLabels {α : Type u} {R : Type v} [CommSemiring R] (f g : ForestAlgebra.LinearFunctional R) : f.convolution g ∘ₗ (eraseLabels R).toLinearMap = convolution (f ∘ₗ (eraseLabels R).toLinearMap) (g ∘ₗ (eraseLabels R).toLinearMap)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_comp_constLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) (f g : LinearFunctional α R) : f.convolution g ∘ₗ (constLabel a R).toLinearMap = ForestAlgebra.LinearFunctional.convolution (f ∘ₗ (constLabel a R).toLinearMap) (g ∘ₗ (constLabel a R).toLinearMap)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_comp_mapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (labelMap : α → β) (f g : LinearFunctional β R) : f.convolution g ∘ₗ (mapLabels R labelMap).toLinearMap = convolution (f ∘ₗ (mapLabels R labelMap).toLinearMap) (g ∘ₗ (mapLabels R labelMap).toLinearMap)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapMapLabels_counit {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) : comapMapLabels f (counit β R) = counit α R

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

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels_counit {α : Type u} {R : Type v} [CommSemiring R] : comapEraseLabels (ForestAlgebra.LinearFunctional.counit R) = counit α R

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapEraseLabels_ofCharacter {α : Type u} {R : Type v} [CommSemiring R] (χ : ForestAlgebra.Character R) : comapEraseLabels (ForestAlgebra.LinearFunctional.ofCharacter χ) = ofCharacter (Character.comapEraseLabels χ)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel_counit {α : Type u} {R : Type v} [CommSemiring R] (a : α) : comapConstLabel a (counit α R) = ForestAlgebra.LinearFunctional.counit R

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.comapConstLabel_ofCharacter {α : Type u} {R : Type v} [CommSemiring R] (a : α) (χ : Character α R) : comapConstLabel a (ofCharacter χ) = ForestAlgebra.LinearFunctional.ofCharacter (Character.comapConstLabel a χ)

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

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (ℓ m : ForestAlgebra.LinearFunctional R) : (comapEraseLabels ℓ).convolution (comapEraseLabels m) = comapEraseLabels (ℓ.convolution m)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) (ℓ m : LinearFunctional α R) : (comapConstLabel a ℓ).convolution (comapConstLabel a m) = comapConstLabel a (ℓ.convolution m)

noncomputable def HopfAlgebras.LForestTripleTensorAlgebra.evalByLinearMaps {α : Type u} {R : Type v} [CommSemiring R] (f g h : LForestAlgebra.LinearFunctional α R) : LForestTripleTensorAlgebra α R →ₗ[R] R

Evaluate a labelled triple tensor term by three linear functionals.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTripleTensorAlgebra.evalByLinearMaps_ofTriple {α : Type u} {R : Type v} [CommSemiring R] (f g h : LForestAlgebra.LinearFunctional α R) (term : LRootedForest α × LRootedForest α × LRootedForest α) : (evalByLinearMaps f g h) (ofTriple term) = f (LForestAlgebra.ofForest term.1) * g (LForestAlgebra.ofForest term.2.1) * h (LForestAlgebra.ofForest term.2.2)

theorem HopfAlgebras.LForestTripleTensorAlgebra.evalByLinearMaps_sumTerms {α : Type u} {R : Type v} [CommSemiring R] (f g h : LForestAlgebra.LinearFunctional α R) (terms : List (LRootedForest α × LRootedForest α × LRootedForest α)) : (evalByLinearMaps f g h) (sumTerms terms) = (List.map (fun (term : LRootedForest α × LRootedForest α × LRootedForest α) => f (LForestAlgebra.ofForest term.1) * g (LForestAlgebra.ofForest term.2.1) * h (LForestAlgebra.ofForest term.2.2)) terms).sum

theorem HopfAlgebras.LForestTripleTensorAlgebra.evalByLinearMaps_coproductLeft {α : Type u} {R : Type v} [CommSemiring R] (f g h : LForestAlgebra.LinearFunctional α R) (x : LForestTensorAlgebra α R) : (evalByLinearMaps f g h) (coproductLeft x) = (LForestTensorAlgebra.evalByLinearMaps (f.convolution g) h) x

theorem HopfAlgebras.LForestTripleTensorAlgebra.evalByLinearMaps_coproductRight {α : Type u} {R : Type v} [CommSemiring R] (f g h : LForestAlgebra.LinearFunctional α R) (x : LForestTensorAlgebra α R) : (evalByLinearMaps f g h) (coproductRight x) = (LForestTensorAlgebra.evalByLinearMaps f (g.convolution h)) x

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_counit_left {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) : (counit α R).convolution f = f

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_counit_right {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) : f.convolution (counit α R) = f

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_zero_left {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) : convolution 0 f = 0

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_zero_right {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) : f.convolution 0 = 0

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_assoc_of_coproduct_eq {α : Type u} {R : Type v} [CommSemiring R] (hcoassoc : ∀ (x : LForestAlgebra α R), (coproductLeft α R) x = (coproductRight α R) x) (f g h : LinearFunctional α R) : (f.convolution g).convolution h = f.convolution (g.convolution h)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_assoc_of_coproductLeft_eq_coproductRight {α : Type u} {R : Type v} [CommSemiring R] (hcoassoc : coproductLeft α R = coproductRight α R) (f g h : LinearFunctional α R) : (f.convolution g).convolution h = f.convolution (g.convolution h)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_assoc {α : Type u} {R : Type v} [CommSemiring R] (f g h : LinearFunctional α R) : (f.convolution g).convolution h = f.convolution (g.convolution h)

def HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) : ℕ → LinearFunctional α R

Convolution powers of a labelled linear functional, with the counit as zeroth power.

Equations

• f.convolutionPower 0 = HopfAlgebras.LForestAlgebra.LinearFunctional.counit α R
• f.convolutionPower n.succ = f.convolution (f.convolutionPower n)

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_zero {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) : f.convolutionPower 0 = counit α R

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_succ {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) (n : ℕ) : f.convolutionPower (n + 1) = f.convolution (f.convolutionPower n)

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_one {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) : f.convolutionPower 1 = f

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_add {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) (m n : ℕ) : f.convolutionPower (m + n) = (f.convolutionPower m).convolution (f.convolutionPower n)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_succ_right {α : Type u} {R : Type v} [CommSemiring R] (f : LinearFunctional α R) (n : ℕ) : f.convolutionPower (n + 1) = (f.convolutionPower n).convolution f

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_zero_succ {α : Type u} {R : Type v} [CommSemiring R] (n : ℕ) : convolutionPower 0 (n + 1) = 0

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_counit {α : Type u} {R : Type v} [CommSemiring R] (n : ℕ) : (counit α R).convolutionPower n = counit α R

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.AgreeUpToOrder.convolutionPower {α : Type u} {R : Type v} [CommSemiring R] {f g : LinearFunctional α R} {n : ℕ} (h : f.AgreeUpToOrder g n) (k : ℕ) : (f.convolutionPower k).AgreeUpToOrder (g.convolutionPower k) n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_comp_eraseLabels {α : Type u} {R : Type v} [CommSemiring R] (f : ForestAlgebra.LinearFunctional R) (n : ℕ) : f.convolutionPower n ∘ₗ (eraseLabels R).toLinearMap = convolutionPower (f ∘ₗ (eraseLabels R).toLinearMap) n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_comp_constLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) (f : LinearFunctional α R) (n : ℕ) : f.convolutionPower n ∘ₗ (constLabel a R).toLinearMap = ForestAlgebra.LinearFunctional.convolutionPower (f ∘ₗ (constLabel a R).toLinearMap) n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_comp_mapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (labelMap : α → β) (f : LinearFunctional β R) (n : ℕ) : f.convolutionPower n ∘ₗ (mapLabels R labelMap).toLinearMap = convolutionPower (f ∘ₗ (mapLabels R labelMap).toLinearMap) n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_comapMapLabels {α : Type u} {R : Type v} [CommSemiring R] {β : Type w} (f : α → β) (ℓ : LinearFunctional β R) (n : ℕ) : (comapMapLabels f ℓ).convolutionPower n = comapMapLabels f (ℓ.convolutionPower n)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (ℓ : ForestAlgebra.LinearFunctional R) (n : ℕ) : (comapEraseLabels ℓ).convolutionPower n = comapEraseLabels (ℓ.convolutionPower n)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolutionPower_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) (ℓ : LinearFunctional α R) (n : ℕ) : (comapConstLabel a ℓ).convolutionPower n = comapConstLabel a (ℓ.convolutionPower n)

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart {α : Type u} {R : Type v} [CommRing R] (χ : Character α R) : LinearFunctional α R

The augmentation part of a labelled forest character.

Equations

• HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart χ = HopfAlgebras.LForestAlgebra.LinearFunctional.ofCharacter χ - HopfAlgebras.LForestAlgebra.LinearFunctional.counit α R

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart_eval_empty {α : Type u} {R : Type v} [CommRing R] (χ : Character α R) : (augmentationPart χ).evalForest LRootedForest.empty = 0

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.agreeUpToOrder_augmentationPart {α : Type u} {R : Type v} [CommRing R] {χ ψ : Character α R} {n : ℕ} (h : ∀ (φ : LRootedForest α), φ.order ≤ n → χ.evalForest φ = ψ.evalForest φ) : (augmentationPart χ).AgreeUpToOrder (augmentationPart ψ) n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart_comapMapLabels {α : Type u} {β : Type w} (f : α → β) {R : Type v} [CommRing R] (χ : Character β R) : augmentationPart (Character.comapMapLabels f χ) = comapMapLabels f (augmentationPart χ)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart_comapEraseLabels {α : Type u} {R : Type v} [CommRing R] (χ : ForestAlgebra.Character R) : augmentationPart (Character.comapEraseLabels χ) = comapEraseLabels (ForestAlgebra.LinearFunctional.augmentationPart χ)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.augmentationPart_comapConstLabel {α : Type u} (a : α) {R : Type v} [CommRing R] (χ : Character α R) : ForestAlgebra.LinearFunctional.augmentationPart (Character.comapConstLabel a χ) = comapConstLabel a (augmentationPart χ)

noncomputable def HopfAlgebras.LForestAlgebra.LinearFunctional.logCharacterTruncated {α : Type u} {R : Type v} [Field R] (χ : Character α R) (n : ℕ) : LinearFunctional α R

The truncated convolution logarithm of a labelled forest character.

Equations

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

@[simp]

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.logCharacterTruncated_zero {α : Type u} {R : Type v} [Field R] (χ : Character α R) : logCharacterTruncated χ 0 = 0

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.logCharacterTruncated_evalForest {α : Type u} {R : Type v} [Field R] (χ : Character α R) (n : ℕ) (φ : LRootedForest α) : (logCharacterTruncated χ n).evalForest φ = (List.map (fun (i : ℕ) => have k := i + 1; (-1) ^ (k + 1) * (↑k)⁻¹ * ((augmentationPart χ).convolutionPower k).evalForest φ) (List.range n)).sum

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.agreeUpToOrder_logCharacterTruncated {α : Type u} {R : Type v} [Field R] {χ ψ : Character α R} {m n : ℕ} (h : ∀ (φ : LRootedForest α), φ.order ≤ n → χ.evalForest φ = ψ.evalForest φ) : (logCharacterTruncated χ m).AgreeUpToOrder (logCharacterTruncated ψ m) n

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.logCharacterTruncated_comapMapLabels {α : Type u} {β : Type w} (f : α → β) {R : Type v} [Field R] (χ : Character β R) (n : ℕ) : logCharacterTruncated (Character.comapMapLabels f χ) n = comapMapLabels f (logCharacterTruncated χ n)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.logCharacterTruncated_comapEraseLabels {α : Type u} {R : Type v} [Field R] (χ : ForestAlgebra.Character R) (n : ℕ) : logCharacterTruncated (Character.comapEraseLabels χ) n = comapEraseLabels (ForestAlgebra.LinearFunctional.logCharacterTruncated χ n)

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.logCharacterTruncated_comapConstLabel {α : Type u} (a : α) {R : Type v} [Field R] (χ : Character α R) (n : ℕ) : ForestAlgebra.LinearFunctional.logCharacterTruncated (Character.comapConstLabel a χ) n = comapConstLabel a (logCharacterTruncated χ n)

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

theorem HopfAlgebras.LForestAlgebra.LinearFunctional.convolution_compRightAntipode_ofCharacter_right {α : Type u} {R : Type v} [CommRing R] (χ : Character α R) : (ofCharacter χ).convolution (ofCharacter χ).compRightAntipode = counit α R

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

noncomputable def HopfAlgebras.LForestAlgebra.Character.inverseLinearFunctional {α : Type u} {R : Type v} [CommRing R] (χ : Character α R) : LinearFunctional α R

The antipode-composed linear functional that gives the convolution inverse of a character.

Equations

• χ.inverseLinearFunctional = (HopfAlgebras.LForestAlgebra.LinearFunctional.ofCharacter χ).compAntipode

theorem HopfAlgebras.LForestAlgebra.Character.convolution_inverseLinearFunctional_left {α : Type u} {R : Type v} [CommRing R] (χ : Character α R) : χ.inverseLinearFunctional.convolution (LinearFunctional.ofCharacter χ) = LinearFunctional.counit α R

theorem HopfAlgebras.LForestAlgebra.Character.convolution_inverseLinearFunctional_right {α : Type u} {R : Type v} [CommRing R] (χ : Character α R) : (LinearFunctional.ofCharacter χ).convolution χ.inverseLinearFunctional = LinearFunctional.counit α R