The Algebra of Rooted Forests

This file defines the commutative algebra freely spanned by non-planar rooted forests. This is the algebraic carrier used by rooted-tree Hopf algebras.

Main definitions

• ForestAlgebra - the monoid algebra of rooted forests
• ForestAlgebra.ofForest - the monomial associated to a rooted forest
• ForestAlgebra.Character - algebra characters on the forest algebra
• ForestAlgebra.Character.evalForest - evaluation of one forest monomial

References

• Philippe Chartier, Ernst Hairer, Gilles Vilmart, Algebraic Structures of B-series
• Alain Connes, Dirk Kreimer, Hopf Algebras, Renormalization and Noncommutative Geometry

@[reducible, inline]

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

The algebra freely spanned by rooted forests over a coefficient semiring.

Equations

• HopfAlgebras.ForestAlgebra R = AddMonoidAlgebra R HopfAlgebras.RootedForest

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

The monomial associated to a rooted forest.

Equations

• HopfAlgebras.ForestAlgebra.ofForest φ = AddMonoidAlgebra.single φ 1

@[simp]

theorem HopfAlgebras.ForestAlgebra.ofForest_zero {R : Type u} [Semiring R] : ofForest 0 = 1

@[simp]

theorem HopfAlgebras.ForestAlgebra.ofForest_empty {R : Type u} [Semiring R] : ofForest RootedForest.empty = 1

@[simp]

theorem HopfAlgebras.ForestAlgebra.ofForest_add {R : Type u} [Semiring R] (φ ψ : RootedForest) : ofForest (φ + ψ) = ofForest φ * ofForest ψ

noncomputable def HopfAlgebras.ForestAlgebra.counitCoeff {R : Type u} [Zero R] [One R] (φ : RootedForest) : R

The counit value on a forest monomial.

Equations

• HopfAlgebras.ForestAlgebra.counitCoeff φ = if φ = 0 then 1 else 0

@[simp]

theorem HopfAlgebras.ForestAlgebra.counitCoeff_zero {R : Type u} [Zero R] [One R] : counitCoeff 0 = 1

@[simp]

theorem HopfAlgebras.ForestAlgebra.counitCoeff_empty {R : Type u} [Zero R] [One R] : counitCoeff RootedForest.empty = 1

theorem HopfAlgebras.ForestAlgebra.counitCoeff_ne_zero {R : Type u} [Zero R] [One R] {φ : RootedForest} (hφ : φ ≠ 0) : counitCoeff φ = 0

theorem HopfAlgebras.ForestAlgebra.counitCoeff_add {R : Type u} [Semiring R] (φ ψ : RootedForest) : counitCoeff (φ + ψ) = counitCoeff φ * counitCoeff ψ

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

The counit algebra homomorphism, sending the empty forest to 1 and other forests to 0.

Equations

• HopfAlgebras.ForestAlgebra.counit R = (AddMonoidAlgebra.lift R R HopfAlgebras.RootedForest) (HopfAlgebras.ForestAlgebra.counitMonoidHom✝ R)

@[simp]

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

@[simp]

theorem HopfAlgebras.ForestAlgebra.counit_ofForest_zero {R : Type u} [CommSemiring R] : (counit R) (ofForest 0) = 1

@[simp]

theorem HopfAlgebras.ForestAlgebra.counit_ofForest_ne_zero {R : Type u} [CommSemiring R] {φ : RootedForest} (hφ : φ ≠ 0) : (counit R) (ofForest φ) = 0

@[reducible, inline]

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

Algebra characters on the rooted-forest algebra.

Equations

• HopfAlgebras.ForestAlgebra.Character R = (HopfAlgebras.ForestAlgebra R →ₐ[R] R)

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

Evaluate a character on the forest monomial associated to a rooted forest.

Equations

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

@[simp]

theorem HopfAlgebras.ForestAlgebra.Character.evalForest_zero {R : Type u} [CommSemiring R] (χ : Character R) : χ.evalForest 0 = 1

@[simp]

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

@[simp]

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

theorem HopfAlgebras.ForestAlgebra.Character.evalForest_ofPTree_list_perm {R : Type u} [CommSemiring R] (χ : Character R) {ts us : List PTree} (h : ts.Perm us) : χ.evalForest ↑(List.map RootedTree.ofPTree ts) = χ.evalForest ↑(List.map RootedTree.ofPTree us)

theorem HopfAlgebras.ForestAlgebra.Character.evalForest_ofPTree_list_forestPerm {R : Type u} [CommSemiring R] (χ : Character R) {ts us : List PTree} (h : PTree.ForestPerm ts us) : χ.evalForest ↑(List.map RootedTree.ofPTree ts) = χ.evalForest ↑(List.map RootedTree.ofPTree us)

theorem HopfAlgebras.ForestAlgebra.Character.evalForest_ofPTree_list_forall₂_perm {R : Type u} [CommSemiring R] (χ : Character R) {ts us : List PTree} (h : List.Forall₂ PTree.Perm ts us) : χ.evalForest ↑(List.map RootedTree.ofPTree ts) = χ.evalForest ↑(List.map RootedTree.ofPTree us)

theorem HopfAlgebras.ForestAlgebra.Character.ext {R : Type u} [CommSemiring R] {χ ψ : Character R} (h : ∀ (φ : RootedForest), χ.evalForest φ = ψ.evalForest φ) : χ = ψ

theorem HopfAlgebras.ForestAlgebra.Character.ext_iff {R : Type u} [CommSemiring R] {χ ψ : Character R} : χ = ψ ↔ ∀ (φ : RootedForest), χ.evalForest φ = ψ.evalForest φ

theorem HopfAlgebras.ForestAlgebra.Character.ext_tree {R : Type u} [CommSemiring R] {χ ψ : Character R} (h : ∀ (τ : RootedTree), χ.evalForest (RootedForest.singleton τ) = ψ.evalForest (RootedForest.singleton τ)) : χ = ψ

@[simp]

theorem HopfAlgebras.ForestAlgebra.Character.map_ofForest_zero {R : Type u} [CommSemiring R] (χ : Character R) : χ (ofForest 0) = 1

@[simp]

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

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