The BCK Antipode

This file defines the recursive antipode on rooted-forest monomials for the Connes-Kreimer/BCK Hopf algebra.

Main definitions

• RootedForest.antipode - the recursive antipode on rooted forest monomials
• RootedForest.antipodeProperSum - the proper-coproduct part of the recursion

References

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

@[irreducible]

noncomputable def HopfAlgebras.RootedForest.antipode {R : Type u} [CommRing R] (φ : RootedForest) : ForestAlgebra R

The recursive BCK antipode on rooted-forest monomials.

Equations

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

noncomputable def HopfAlgebras.RootedForest.antipodeProperSum {R : Type u} [CommRing R] (φ : RootedForest) : ForestAlgebra R

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

Equations

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

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

antipodeProperSum with the attach plumbing removed.

@[simp]

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

@[simp]

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

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

theorem HopfAlgebras.RootedForest.antipode_singleton {R : Type u} [CommRing R] (τ : RootedTree) : (singleton τ).antipode = -ForestAlgebra.ofForest (singleton τ) - (singleton τ).antipodeProperSum

theorem HopfAlgebras.RootedForest.counit_antipode {R : Type u} [CommRing R] (φ : RootedForest) : (ForestAlgebra.counit R) φ.antipode = ForestAlgebra.counitCoeff φ

@[irreducible]

noncomputable def HopfAlgebras.RootedForest.rightAntipode {R : Type u} [CommRing R] (φ : RootedForest) : ForestAlgebra R

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

Equations

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

noncomputable def HopfAlgebras.RootedForest.rightAntipodeProperSum {R : Type u} [CommRing R] (φ : RootedForest) : ForestAlgebra R

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

Equations

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

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

rightAntipodeProperSum with the attach plumbing removed.

@[simp]

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

@[simp]

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

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

theorem HopfAlgebras.RootedForest.rightAntipode_singleton {R : Type u} [CommRing R] (τ : RootedTree) : (singleton τ).rightAntipode = -ForestAlgebra.ofForest (singleton τ) - (singleton τ).rightAntipodeProperSum

theorem HopfAlgebras.RootedForest.counit_rightAntipode {R : Type u} [CommRing R] (φ : RootedForest) : (ForestAlgebra.counit R) φ.rightAntipode = ForestAlgebra.counitCoeff φ

noncomputable def HopfAlgebras.ForestTensorAlgebra.antipodeLeft {R : Type u} [CommRing R] : ForestTensorAlgebra R →ₗ[R] ForestAlgebra R

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

Equations

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

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.antipodeLeft_ofPair {R : Type u} [CommRing R] (term : RootedForest × RootedForest) : antipodeLeft (ofPair term) = term.1.antipode * ForestAlgebra.ofForest term.2

theorem HopfAlgebras.ForestTensorAlgebra.antipodeLeft_sumTerms {R : Type u} [CommRing R] (terms : List (RootedForest × RootedForest)) : antipodeLeft (sumTerms terms) = (List.map (fun (term : RootedForest × RootedForest) => term.1.antipode * ForestAlgebra.ofForest term.2) terms).sum

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

noncomputable def HopfAlgebras.ForestTensorAlgebra.antipodeRight {R : Type u} [CommRing R] : ForestTensorAlgebra R →ₗ[R] ForestAlgebra R

Evaluate a tensor term by applying the right-recursive antipode to the right factor and multiplying in the forest algebra.

Equations

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

@[simp]

theorem HopfAlgebras.ForestTensorAlgebra.antipodeRight_ofPair {R : Type u} [CommRing R] (term : RootedForest × RootedForest) : antipodeRight (ofPair term) = ForestAlgebra.ofForest term.1 * term.2.rightAntipode

theorem HopfAlgebras.ForestTensorAlgebra.antipodeRight_sumTerms {R : Type u} [CommRing R] (terms : List (RootedForest × RootedForest)) : antipodeRight (sumTerms terms) = (List.map (fun (term : RootedForest × RootedForest) => ForestAlgebra.ofForest term.1 * term.2.rightAntipode) terms).sum

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

theorem HopfAlgebras.RootedForest.antipodeLeft_reducedCoproduct {R : Type u} [CommRing R] (φ : RootedForest) : ForestTensorAlgebra.antipodeLeft φ.reducedCoproduct = φ.antipodeProperSum

theorem HopfAlgebras.RootedForest.antipodeLeft_reducedCoproduct_eq_neg {R : Type u} [CommRing R] {φ : RootedForest} (hφ : φ ≠ 0) : ForestTensorAlgebra.antipodeLeft φ.reducedCoproduct = -ForestAlgebra.ofForest φ - φ.antipode

theorem HopfAlgebras.RootedForest.antipode_add_ofForest_add_antipodeLeft_reducedCoproduct {R : Type u} [CommRing R] {φ : RootedForest} (hφ : φ ≠ 0) : φ.antipode + ForestAlgebra.ofForest φ + ForestTensorAlgebra.antipodeLeft φ.reducedCoproduct = 0

theorem HopfAlgebras.RootedForest.antipodeRight_reducedCoproduct {R : Type u} [CommRing R] (φ : RootedForest) : ForestTensorAlgebra.antipodeRight φ.reducedCoproduct = φ.rightAntipodeProperSum

theorem HopfAlgebras.RootedForest.antipodeRight_reducedCoproduct_eq_neg {R : Type u} [CommRing R] {φ : RootedForest} (hφ : φ ≠ 0) : ForestTensorAlgebra.antipodeRight φ.reducedCoproduct = -ForestAlgebra.ofForest φ - φ.rightAntipode

theorem HopfAlgebras.RootedForest.rightAntipode_add_ofForest_add_antipodeRight_reducedCoproduct {R : Type u} [CommRing R] {φ : RootedForest} (hφ : φ ≠ 0) : φ.rightAntipode + ForestAlgebra.ofForest φ + ForestTensorAlgebra.antipodeRight φ.reducedCoproduct = 0

theorem HopfAlgebras.RootedForest.antipodeLeft_coproduct {R : Type u} [CommRing R] (φ : RootedForest) : ForestTensorAlgebra.antipodeLeft φ.coproduct = ForestAlgebra.counitCoeff φ • 1

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

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

theorem HopfAlgebras.RootedForest.antipodeRight_coproduct {R : Type u} [CommRing R] (φ : RootedForest) : ForestTensorAlgebra.antipodeRight φ.coproduct = ForestAlgebra.counitCoeff φ • 1

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

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

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

The linear extension of the recursive antipode to the rooted-forest algebra.

Equations

• HopfAlgebras.ForestAlgebra.antipode = Finsupp.linearCombination R HopfAlgebras.RootedForest.antipode

@[simp]

theorem HopfAlgebras.ForestAlgebra.antipode_ofForest {R : Type u} [CommRing R] (φ : RootedForest) : antipode (ofForest φ) = φ.antipode

@[simp]

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

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

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

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

The linear extension of the right-recursive antipode to the rooted-forest algebra.

Equations

• HopfAlgebras.ForestAlgebra.rightAntipode = Finsupp.linearCombination R HopfAlgebras.RootedForest.rightAntipode

@[simp]

theorem HopfAlgebras.ForestAlgebra.rightAntipode_ofForest {R : Type u} [CommRing R] (φ : RootedForest) : rightAntipode (ofForest φ) = φ.rightAntipode

@[simp]

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

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

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

theorem HopfAlgebras.ForestAlgebra.antipodeLeft_coproduct {R : Type u} [CommRing R] (x : ForestAlgebra R) : ForestTensorAlgebra.antipodeLeft ((coproduct R) x) = (counit R) x • 1

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

theorem HopfAlgebras.ForestAlgebra.antipodeRight_coproduct {R : Type u} [CommRing R] (x : ForestAlgebra R) : ForestTensorAlgebra.antipodeRight ((coproduct R) x) = (counit R) x • 1

Applying the right-recursive antipode on the right factor of the algebra coproduct gives the counit.

theorem HopfAlgebras.ForestAlgebra.Character.eval_antipodeLeft_coproduct {R : Type u} [CommRing R] (χ : Character R) (x : ForestAlgebra R) : χ (ForestTensorAlgebra.antipodeLeft ((coproduct R) x)) = (counit R) x

theorem HopfAlgebras.ForestAlgebra.Character.eval_antipodeRight_coproduct {R : Type u} [CommRing R] (χ : Character R) (x : ForestAlgebra R) : χ (ForestTensorAlgebra.antipodeRight ((coproduct R) x)) = (counit R) x