The Labelled BCK Antipode

This file defines the recursive antipode on labelled rooted-forest monomials.

Main definitions

• LRootedForest.antipode - the recursive antipode on labelled rooted forests
• LRootedForest.antipodeProperSum - the proper-coproduct part of the recursion
• LForestAlgebra.antipode - the linear extension to the labelled forest algebra

References

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

@[irreducible]

noncomputable def HopfAlgebras.LRootedForest.antipode {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : LForestAlgebra α R

The recursive BCK antipode on labelled rooted-forest monomials.

Equations

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

noncomputable def HopfAlgebras.LRootedForest.antipodeProperSum {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : LForestAlgebra α R

The proper-coproduct sum appearing in the recursive labelled antipode formula.

Equations

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

theorem HopfAlgebras.LRootedForest.antipodeProperSum_eq_map_sum {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : φ.antipodeProperSum = (List.map (fun (term : LRootedForest α × LRootedForest α) => term.1.antipode * LForestAlgebra.ofForest term.2) φ.properCoproductTerms).sum

antipodeProperSum with the attach plumbing removed.

@[simp]

theorem HopfAlgebras.LRootedForest.antipode_zero {α : Type u} {R : Type v} [CommRing R] : antipode 0 = 1

@[simp]

theorem HopfAlgebras.LRootedForest.antipode_empty {α : Type u} {R : Type v} [CommRing R] : empty.antipode = 1

theorem HopfAlgebras.LRootedForest.antipode_eq_of_ne_zero {α : Type u} {R : Type v} [CommRing R] {φ : LRootedForest α} (hφ : φ ≠ 0) : φ.antipode = -LForestAlgebra.ofForest φ - φ.antipodeProperSum

theorem HopfAlgebras.LRootedForest.antipode_singleton {α : Type u} {R : Type v} [CommRing R] (τ : LRootedTree α) : (singleton τ).antipode = -LForestAlgebra.ofForest (singleton τ) - (singleton τ).antipodeProperSum

@[irreducible]

noncomputable def HopfAlgebras.LRootedForest.rightAntipode {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : LForestAlgebra α R

The symmetric right-recursive BCK antipode on labelled rooted-forest monomials.

Equations

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

noncomputable def HopfAlgebras.LRootedForest.rightAntipodeProperSum {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : LForestAlgebra α R

The proper-coproduct sum appearing in the right-recursive labelled antipode formula.

Equations

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

theorem HopfAlgebras.LRootedForest.rightAntipodeProperSum_eq_map_sum {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : φ.rightAntipodeProperSum = (List.map (fun (term : LRootedForest α × LRootedForest α) => LForestAlgebra.ofForest term.1 * term.2.rightAntipode) φ.properCoproductTerms).sum

rightAntipodeProperSum with the attach plumbing removed.

@[simp]

theorem HopfAlgebras.LRootedForest.rightAntipode_zero {α : Type u} {R : Type v} [CommRing R] : rightAntipode 0 = 1

@[simp]

theorem HopfAlgebras.LRootedForest.rightAntipode_empty {α : Type u} {R : Type v} [CommRing R] : empty.rightAntipode = 1

theorem HopfAlgebras.LRootedForest.rightAntipode_eq_of_ne_zero {α : Type u} {R : Type v} [CommRing R] {φ : LRootedForest α} (hφ : φ ≠ 0) : φ.rightAntipode = -LForestAlgebra.ofForest φ - φ.rightAntipodeProperSum

theorem HopfAlgebras.LRootedForest.rightAntipode_singleton {α : Type u} {R : Type v} [CommRing R] (τ : LRootedTree α) : (singleton τ).rightAntipode = -LForestAlgebra.ofForest (singleton τ) - (singleton τ).rightAntipodeProperSum

theorem HopfAlgebras.LRootedForest.counit_rightAntipode {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : (LForestAlgebra.counit α R) φ.rightAntipode = LForestAlgebra.counitCoeff φ

theorem HopfAlgebras.LRootedForest.eraseLabels_antipode {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : (LForestAlgebra.eraseLabels R) φ.antipode = φ.erase.antipode

theorem HopfAlgebras.LRootedForest.counit_antipode {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : (LForestAlgebra.counit α R) φ.antipode = LForestAlgebra.counitCoeff φ

theorem HopfAlgebras.LRootedForest.mapLabels_antipode {α : Type u} {R : Type v} [CommRing R] {β : Type w} (f : α → β) (φ : LRootedForest α) : (LForestAlgebra.mapLabels R f) φ.antipode = (mapLabels f φ).antipode

theorem HopfAlgebras.LRootedForest.constLabel_antipode {α : Type u} {R : Type v} [CommRing R] (a : α) (φ : RootedForest) : (LForestAlgebra.constLabel a R) φ.antipode = (constLabel a φ).antipode

theorem HopfAlgebras.LRootedForest.eraseLabels_rightAntipode {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : (LForestAlgebra.eraseLabels R) φ.rightAntipode = φ.erase.rightAntipode

theorem HopfAlgebras.LRootedForest.mapLabels_rightAntipode {α : Type u} {R : Type v} [CommRing R] {β : Type w} (f : α → β) (φ : LRootedForest α) : (LForestAlgebra.mapLabels R f) φ.rightAntipode = (mapLabels f φ).rightAntipode

theorem HopfAlgebras.LRootedForest.constLabel_rightAntipode {α : Type u} {R : Type v} [CommRing R] (a : α) (φ : RootedForest) : (LForestAlgebra.constLabel a R) φ.rightAntipode = (constLabel a φ).rightAntipode

noncomputable def HopfAlgebras.LForestTensorAlgebra.antipodeLeft {α : Type u} {R : Type v} [CommRing R] : LForestTensorAlgebra α R →ₗ[R] LForestAlgebra α R

Evaluate a tensor term by applying the labelled antipode to the left factor and multiplying in the labelled forest algebra.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.antipodeLeft_ofPair {α : Type u} {R : Type v} [CommRing R] (term : LRootedForest α × LRootedForest α) : antipodeLeft (ofPair term) = term.1.antipode * LForestAlgebra.ofForest term.2

theorem HopfAlgebras.LForestTensorAlgebra.antipodeLeft_sumTerms {α : Type u} {R : Type v} [CommRing R] (terms : List (LRootedForest α × LRootedForest α)) : antipodeLeft (sumTerms terms) = (List.map (fun (term : LRootedForest α × LRootedForest α) => term.1.antipode * LForestAlgebra.ofForest term.2) terms).sum

theorem HopfAlgebras.LForestTensorAlgebra.evalCharacter_antipodeLeft_sumTerms {α : Type u} {R : Type v} [CommRing R] (χ : LForestAlgebra.Character α R) (terms : List (LRootedForest α × LRootedForest α)) : χ (antipodeLeft (sumTerms terms)) = (List.map (fun (term : LRootedForest α × LRootedForest α) => χ term.1.antipode * χ.evalForest term.2) terms).sum

noncomputable def HopfAlgebras.LForestTensorAlgebra.antipodeRight {α : Type u} {R : Type v} [CommRing R] : LForestTensorAlgebra α R →ₗ[R] LForestAlgebra α R

Evaluate a labelled tensor term by applying the right-recursive antipode to the right factor.

Equations

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

@[simp]

theorem HopfAlgebras.LForestTensorAlgebra.antipodeRight_ofPair {α : Type u} {R : Type v} [CommRing R] (term : LRootedForest α × LRootedForest α) : antipodeRight (ofPair term) = LForestAlgebra.ofForest term.1 * term.2.rightAntipode

theorem HopfAlgebras.LForestTensorAlgebra.antipodeRight_sumTerms {α : Type u} {R : Type v} [CommRing R] (terms : List (LRootedForest α × LRootedForest α)) : antipodeRight (sumTerms terms) = (List.map (fun (term : LRootedForest α × LRootedForest α) => LForestAlgebra.ofForest term.1 * term.2.rightAntipode) terms).sum

theorem HopfAlgebras.LForestTensorAlgebra.evalCharacter_antipodeRight_sumTerms {α : Type u} {R : Type v} [CommRing R] (χ : LForestAlgebra.Character α R) (terms : List (LRootedForest α × LRootedForest α)) : χ (antipodeRight (sumTerms terms)) = (List.map (fun (term : LRootedForest α × LRootedForest α) => χ.evalForest term.1 * χ term.2.rightAntipode) terms).sum

theorem HopfAlgebras.LRootedForest.antipodeLeft_reducedCoproduct {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : LForestTensorAlgebra.antipodeLeft φ.reducedCoproduct = φ.antipodeProperSum

theorem HopfAlgebras.LRootedForest.antipodeLeft_reducedCoproduct_eq_neg {α : Type u} {R : Type v} [CommRing R] {φ : LRootedForest α} (hφ : φ ≠ 0) : LForestTensorAlgebra.antipodeLeft φ.reducedCoproduct = -LForestAlgebra.ofForest φ - φ.antipode

theorem HopfAlgebras.LRootedForest.antipode_add_ofForest_add_antipodeLeft_reducedCoproduct {α : Type u} {R : Type v} [CommRing R] {φ : LRootedForest α} (hφ : φ ≠ 0) : φ.antipode + LForestAlgebra.ofForest φ + LForestTensorAlgebra.antipodeLeft φ.reducedCoproduct = 0

theorem HopfAlgebras.LRootedForest.antipodeRight_reducedCoproduct {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : LForestTensorAlgebra.antipodeRight φ.reducedCoproduct = φ.rightAntipodeProperSum

theorem HopfAlgebras.LRootedForest.antipodeRight_reducedCoproduct_eq_neg {α : Type u} {R : Type v} [CommRing R] {φ : LRootedForest α} (hφ : φ ≠ 0) : LForestTensorAlgebra.antipodeRight φ.reducedCoproduct = -LForestAlgebra.ofForest φ - φ.rightAntipode

theorem HopfAlgebras.LRootedForest.rightAntipode_add_ofForest_add_antipodeRight_reducedCoproduct {α : Type u} {R : Type v} [CommRing R] {φ : LRootedForest α} (hφ : φ ≠ 0) : φ.rightAntipode + LForestAlgebra.ofForest φ + LForestTensorAlgebra.antipodeRight φ.reducedCoproduct = 0

theorem HopfAlgebras.LRootedForest.antipodeLeft_coproduct {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : LForestTensorAlgebra.antipodeLeft φ.coproduct = LForestAlgebra.counitCoeff φ • 1

Evaluating the full labelled coproduct by the labelled antipode on the left gives the counit.

theorem HopfAlgebras.LRootedForest.evalCharacter_antipodeLeft_coproductTerms {α : Type u} {R : Type v} [CommRing R] (χ : LForestAlgebra.Character α R) (φ : LRootedForest α) : (List.map (fun (term : LRootedForest α × LRootedForest α) => χ term.1.antipode * χ.evalForest term.2) φ.coproductTerms).sum = LForestAlgebra.counitCoeff φ

theorem HopfAlgebras.LRootedForest.antipodeRight_coproduct {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : LForestTensorAlgebra.antipodeRight φ.coproduct = LForestAlgebra.counitCoeff φ • 1

Evaluating the full labelled coproduct by the right-recursive antipode gives the counit.

theorem HopfAlgebras.LRootedForest.evalCharacter_antipodeRight_coproductTerms {α : Type u} {R : Type v} [CommRing R] (χ : LForestAlgebra.Character α R) (φ : LRootedForest α) : (List.map (fun (term : LRootedForest α × LRootedForest α) => χ.evalForest term.1 * χ term.2.rightAntipode) φ.coproductTerms).sum = LForestAlgebra.counitCoeff φ

noncomputable def HopfAlgebras.LForestAlgebra.antipode {α : Type u} {R : Type v} [CommRing R] : LForestAlgebra α R →ₗ[R] LForestAlgebra α R

The linear extension of the recursive antipode to the labelled forest algebra.

Equations

• HopfAlgebras.LForestAlgebra.antipode = Finsupp.linearCombination R HopfAlgebras.LRootedForest.antipode

@[simp]

theorem HopfAlgebras.LForestAlgebra.antipode_ofForest {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : antipode (ofForest φ) = φ.antipode

@[simp]

theorem HopfAlgebras.LForestAlgebra.antipode_zero {α : Type u} {R : Type v} [CommRing R] : antipode 0 = 0

theorem HopfAlgebras.LForestAlgebra.antipode_add {α : Type u} {R : Type v} [CommRing R] (x y : LForestAlgebra α R) : antipode (x + y) = antipode x + antipode y

noncomputable def HopfAlgebras.LForestAlgebra.rightAntipode {α : Type u} {R : Type v} [CommRing R] : LForestAlgebra α R →ₗ[R] LForestAlgebra α R

The linear extension of the right-recursive labelled antipode.

Equations

• HopfAlgebras.LForestAlgebra.rightAntipode = Finsupp.linearCombination R HopfAlgebras.LRootedForest.rightAntipode

@[simp]

theorem HopfAlgebras.LForestAlgebra.rightAntipode_ofForest {α : Type u} {R : Type v} [CommRing R] (φ : LRootedForest α) : rightAntipode (ofForest φ) = φ.rightAntipode

@[simp]

theorem HopfAlgebras.LForestAlgebra.rightAntipode_zero {α : Type u} {R : Type v} [CommRing R] : rightAntipode 0 = 0

theorem HopfAlgebras.LForestAlgebra.rightAntipode_add {α : Type u} {R : Type v} [CommRing R] (x y : LForestAlgebra α R) : rightAntipode (x + y) = rightAntipode x + rightAntipode y

theorem HopfAlgebras.LForestAlgebra.counit_rightAntipode {α : Type u} {R : Type v} [CommRing R] (x : LForestAlgebra α R) : (counit α R) (rightAntipode x) = (counit α R) x

theorem HopfAlgebras.LForestAlgebra.antipodeLeft_coproduct {α : Type u} {R : Type v} [CommRing R] (x : LForestAlgebra α R) : LForestTensorAlgebra.antipodeLeft ((coproduct α R) x) = (counit α R) x • 1

Applying the labelled recursive antipode on the left factor of the coproduct gives the counit.

theorem HopfAlgebras.LForestAlgebra.antipodeRight_coproduct {α : Type u} {R : Type v} [CommRing R] (x : LForestAlgebra α R) : LForestTensorAlgebra.antipodeRight ((coproduct α R) x) = (counit α R) x • 1

Applying the right-recursive labelled antipode on the right factor gives the counit.

theorem HopfAlgebras.LForestAlgebra.Character.eval_antipodeLeft_coproduct {α : Type u} {R : Type v} [CommRing R] (χ : Character α R) (x : LForestAlgebra α R) : χ (LForestTensorAlgebra.antipodeLeft ((coproduct α R) x)) = (counit α R) x

theorem HopfAlgebras.LForestAlgebra.Character.eval_antipodeRight_coproduct {α : Type u} {R : Type v} [CommRing R] (χ : Character α R) (x : LForestAlgebra α R) : χ (LForestTensorAlgebra.antipodeRight ((coproduct α R) x)) = (counit α R) x

theorem HopfAlgebras.LForestAlgebra.eraseLabels_antipode {α : Type u} {R : Type v} [CommRing R] (x : LForestAlgebra α R) : (eraseLabels R) (antipode x) = ForestAlgebra.antipode ((eraseLabels R) x)

theorem HopfAlgebras.LForestAlgebra.counit_antipode {α : Type u} {R : Type v} [CommRing R] (x : LForestAlgebra α R) : (counit α R) (antipode x) = (counit α R) x

theorem HopfAlgebras.LForestAlgebra.mapLabels_antipode {α : Type u} {R : Type v} [CommRing R] {β : Type w} (f : α → β) (x : LForestAlgebra α R) : (mapLabels R f) (antipode x) = antipode ((mapLabels R f) x)

theorem HopfAlgebras.LForestAlgebra.constLabel_antipode {α : Type u} {R : Type v} [CommRing R] (a : α) (x : ForestAlgebra R) : (constLabel a R) (ForestAlgebra.antipode x) = antipode ((constLabel a R) x)

theorem HopfAlgebras.LForestAlgebra.eraseLabels_rightAntipode {α : Type u} {R : Type v} [CommRing R] (x : LForestAlgebra α R) : (eraseLabels R) (rightAntipode x) = ForestAlgebra.rightAntipode ((eraseLabels R) x)

theorem HopfAlgebras.LForestAlgebra.mapLabels_rightAntipode {α : Type u} {R : Type v} [CommRing R] {β : Type w} (f : α → β) (x : LForestAlgebra α R) : (mapLabels R f) (rightAntipode x) = rightAntipode ((mapLabels R f) x)

theorem HopfAlgebras.LForestAlgebra.constLabel_rightAntipode {α : Type u} {R : Type v} [CommRing R] (a : α) (x : ForestAlgebra R) : (constLabel a R) (ForestAlgebra.rightAntipode x) = rightAntipode ((constLabel a R) x)