The Algebra of Ordered Planar Forests

This file defines the noncommutative algebra freely spanned by ordered planar forests. Multiplication is concatenation of ordered forests. The quotient maps to the existing commutative non-planar forest algebras forget sibling order.

This is the algebraic carrier needed for ordered-tree Hopf algebras such as the Munthe-Kaas-Wright Hopf algebra.

Main definitions

• PlanarForestAlgebra - monoid algebra of ordered planar forests
• LPlanarForestAlgebra - labelled ordered planar forest algebra
• PlanarForestAlgebra.toForestAlgebra - forget planar order
• LPlanarForestAlgebra.toLForestAlgebra - forget planar order in the labelled case

@[reducible, inline]

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

The noncommutative algebra freely spanned by ordered planar forests.

Equations

• HopfAlgebras.PlanarForestAlgebra R = MonoidAlgebra R HopfAlgebras.PlanarForest

@[implicit_reducible]

instance HopfAlgebras.instOnePlanarForest : One PlanarForest

Equations

• HopfAlgebras.instOnePlanarForest = { one := [] }

@[implicit_reducible]

instance HopfAlgebras.instMulPlanarForest : Mul PlanarForest

Equations

• HopfAlgebras.instMulPlanarForest = { mul := List.append }

@[implicit_reducible]

instance HopfAlgebras.instMonoidPlanarForest : Monoid PlanarForest

Equations

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

@[simp]

theorem HopfAlgebras.PlanarForest.toRootedForest_nil : toRootedForest [] = 0

@[simp]

theorem HopfAlgebras.PlanarForest.toRootedForest_empty : empty.toRootedForest = 0

@[simp]

theorem HopfAlgebras.PlanarForest.toRootedForest_append (ts us : PlanarForest) : (ts ++ us).toRootedForest = ts.toRootedForest + us.toRootedForest

@[simp]

theorem HopfAlgebras.PlanarForest.toRootedForest_singleton (t : PlanarTree) : (singleton t).toRootedForest = RootedForest.singleton t.toRootedTree

noncomputable def HopfAlgebras.PlanarForestAlgebra.ofForest {R : Type u} [Semiring R] (ts : PlanarForest) : PlanarForestAlgebra R

The monomial associated to an ordered planar forest.

Equations

• HopfAlgebras.PlanarForestAlgebra.ofForest ts = MonoidAlgebra.single ts 1

@[simp]

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

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.ofForest_nil {R : Type u} [Semiring R] : ofForest [] = 1

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.ofForest_append {R : Type u} [Semiring R] (ts us : PlanarForest) : ofForest (ts ++ us) = ofForest ts * ofForest us

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.ofForest_singleton_mul {R : Type u} [Semiring R] (t : PlanarTree) (ts : PlanarForest) : ofForest (t :: ts) = ofForest [t] * ofForest ts

def HopfAlgebras.PlanarForestAlgebra.counitCoeff {R : Type u} [Zero R] [One R] (ts : PlanarForest) : R

The counit value on an ordered forest monomial.

Equations

• HopfAlgebras.PlanarForestAlgebra.counitCoeff ts = if ts = [] then 1 else 0

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.counitCoeff_nil {R : Type u} [Zero R] [One R] : counitCoeff [] = 1

@[simp]

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

theorem HopfAlgebras.PlanarForestAlgebra.counitCoeff_ne_nil {R : Type u} [Zero R] [One R] {ts : PlanarForest} (hts : ts ≠ []) : counitCoeff ts = 0

theorem HopfAlgebras.PlanarForestAlgebra.counitCoeff_append {R : Type u} [Semiring R] (ts us : PlanarForest) : counitCoeff (ts ++ us) = counitCoeff ts * counitCoeff us

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

The counit algebra homomorphism, sending the empty ordered forest to 1.

Equations

• HopfAlgebras.PlanarForestAlgebra.counit R = (MonoidAlgebra.lift R R HopfAlgebras.PlanarForest) (HopfAlgebras.PlanarForestAlgebra.counitMonoidHom✝ R)

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.counit_ofForest {R : Type u} [CommSemiring R] (ts : PlanarForest) : (counit R) (ofForest ts) = counitCoeff ts

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.counit_ofForest_empty {R : Type u} [CommSemiring R] : (counit R) (ofForest PlanarForest.empty) = 1

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.counit_ofForest_nil {R : Type u} [CommSemiring R] : (counit R) (ofForest []) = 1

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.counit_ofForest_ne_nil {R : Type u} [CommSemiring R] {ts : PlanarForest} (hts : ts ≠ []) : (counit R) (ofForest ts) = 0

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

Forget planar order as an algebra morphism to the commutative forest algebra.

Equations

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

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.toForestAlgebra_ofForest {R : Type u} [CommSemiring R] (ts : PlanarForest) : (toForestAlgebra R) (ofForest ts) = ForestAlgebra.ofForest ts.toRootedForest

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.toForestAlgebra_ofForest_empty {R : Type u} [CommSemiring R] : (toForestAlgebra R) (ofForest PlanarForest.empty) = 1

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.counit_comp_toForestAlgebra {R : Type u} [CommSemiring R] : (ForestAlgebra.counit R).comp (toForestAlgebra R) = counit R

@[reducible, inline]

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

Algebra characters on the ordered planar forest algebra.

Equations

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

noncomputable def HopfAlgebras.PlanarForestAlgebra.Character.evalForest {R : Type u} [CommSemiring R] (χ : Character R) (ts : PlanarForest) : R

Evaluate a character on the monomial associated to an ordered planar forest.

Equations

• χ.evalForest ts = χ (HopfAlgebras.PlanarForestAlgebra.ofForest ts)

@[simp]

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

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.Character.evalForest_nil {R : Type u} [CommSemiring R] (χ : Character R) : χ.evalForest [] = 1

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.Character.evalForest_append {R : Type u} [CommSemiring R] (χ : Character R) (ts us : PlanarForest) : χ.evalForest (ts ++ us) = χ.evalForest ts * χ.evalForest us

theorem HopfAlgebras.PlanarForestAlgebra.Character.ext {R : Type u} [CommSemiring R] {χ ψ : Character R} (h : ∀ (ts : PlanarForest), χ.evalForest ts = ψ.evalForest ts) : χ = ψ

theorem HopfAlgebras.PlanarForestAlgebra.Character.ext_iff {R : Type u} [CommSemiring R] {χ ψ : Character R} : χ = ψ ↔ ∀ (ts : PlanarForest), χ.evalForest ts = ψ.evalForest ts

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

Pull a commutative forest character back by forgetting planar order.

Equations

• HopfAlgebras.PlanarForestAlgebra.Character.comapToForestAlgebra χ = AlgHom.comp χ (HopfAlgebras.PlanarForestAlgebra.toForestAlgebra R)

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.Character.comapToForestAlgebra_evalForest {R : Type u} [CommSemiring R] (χ : ForestAlgebra.Character R) (ts : PlanarForest) : (comapToForestAlgebra χ).evalForest ts = χ.evalForest ts.toRootedForest

@[simp]

theorem HopfAlgebras.PlanarForestAlgebra.Character.comapToForestAlgebra_counit {R : Type u} [CommSemiring R] : comapToForestAlgebra (ForestAlgebra.counit R) = counit R

@[reducible, inline]

abbrev HopfAlgebras.LPlanarForestAlgebra (α : Type u) (R : Type v) [Semiring R] : Type (max u v)

The noncommutative algebra freely spanned by labelled ordered planar forests.

Equations

• HopfAlgebras.LPlanarForestAlgebra α R = MonoidAlgebra R (HopfAlgebras.LPlanarForest α)

@[implicit_reducible]

instance HopfAlgebras.instOneLPlanarForest (α : Type u) : One (LPlanarForest α)

Equations

• HopfAlgebras.instOneLPlanarForest α = { one := [] }

@[implicit_reducible]

instance HopfAlgebras.instMulLPlanarForest (α : Type u) : Mul (LPlanarForest α)

Equations

• HopfAlgebras.instMulLPlanarForest α = { mul := List.append }

@[implicit_reducible]

instance HopfAlgebras.instMonoidLPlanarForest (α : Type u) : Monoid (LPlanarForest α)

Equations

• HopfAlgebras.instMonoidLPlanarForest α = { mul := List.append, mul_assoc := ⋯, one := [], one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

@[simp]

theorem HopfAlgebras.LPlanarForest.toRootedForest_nil {α : Type u} : toRootedForest [] = 0

@[simp]

theorem HopfAlgebras.LPlanarForest.toRootedForest_empty {α : Type u} : empty.toRootedForest = 0

@[simp]

theorem HopfAlgebras.LPlanarForest.toRootedForest_append {α : Type u} (ts us : LPlanarForest α) : (ts ++ us).toRootedForest = ts.toRootedForest + us.toRootedForest

@[simp]

theorem HopfAlgebras.LPlanarForest.erase_append' {α : Type u} (ts us : LPlanarForest α) : (ts ++ us).erase = ts.erase.append us.erase

@[simp]

theorem HopfAlgebras.LPlanarForest.constLabel_append {α : Type u} (a : α) (ts us : PlanarForest) : constLabel a (ts ++ us) = constLabel a ts ++ constLabel a us

@[simp]

theorem HopfAlgebras.LPlanarForest.toRootedForest_map {α : Type u} {β : Type v} (f : α → β) (ts : LPlanarForest α) : (map f ts).toRootedForest = LRootedForest.mapLabels f ts.toRootedForest

@[simp]

theorem HopfAlgebras.LPlanarForest.toRootedForest_constLabel {α : Type u} (a : α) (ts : PlanarForest) : (constLabel a ts).toRootedForest = LRootedForest.constLabel a ts.toRootedForest

noncomputable def HopfAlgebras.LPlanarForestAlgebra.ofForest {α : Type u} {R : Type v} [Semiring R] (ts : LPlanarForest α) : LPlanarForestAlgebra α R

The monomial associated to a labelled ordered planar forest.

Equations

• HopfAlgebras.LPlanarForestAlgebra.ofForest ts = MonoidAlgebra.single ts 1

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.ofForest_empty {α : Type u} {R : Type v} [Semiring R] : ofForest LPlanarForest.empty = 1

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.ofForest_nil {α : Type u} {R : Type v} [Semiring R] : ofForest [] = 1

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.ofForest_append {α : Type u} {R : Type v} [Semiring R] (ts us : LPlanarForest α) : ofForest (ts ++ us) = ofForest ts * ofForest us

def HopfAlgebras.LPlanarForestAlgebra.counitCoeff {α : Type u} {R : Type v} [Zero R] [One R] (ts : LPlanarForest α) : R

The counit value on a labelled ordered forest monomial.

Equations

• HopfAlgebras.LPlanarForestAlgebra.counitCoeff ts = if ts = [] then 1 else 0

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.counitCoeff_nil {α : Type u} {R : Type v} [Zero R] [One R] : counitCoeff [] = 1

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.counitCoeff_empty {α : Type u} {R : Type v} [Zero R] [One R] : counitCoeff LPlanarForest.empty = 1

theorem HopfAlgebras.LPlanarForestAlgebra.counitCoeff_ne_nil {α : Type u} {R : Type v} [Zero R] [One R] {ts : LPlanarForest α} (hts : ts ≠ []) : counitCoeff ts = 0

theorem HopfAlgebras.LPlanarForestAlgebra.counitCoeff_append {α : Type u} {R : Type v} [Semiring R] (ts us : LPlanarForest α) : counitCoeff (ts ++ us) = counitCoeff ts * counitCoeff us

theorem HopfAlgebras.LPlanarForestAlgebra.counitCoeff_map {α : Type u} {β : Type w} {R : Type v} [Zero R] [One R] (f : α → β) (ts : LPlanarForest α) : counitCoeff (LPlanarForest.map f ts) = counitCoeff ts

theorem HopfAlgebras.LPlanarForestAlgebra.counitCoeff_erase {α : Type u} {R : Type v} [Zero R] [One R] (ts : LPlanarForest α) : PlanarForestAlgebra.counitCoeff ts.erase = counitCoeff ts

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

The counit algebra homomorphism, sending the empty ordered forest to 1.

Equations

• HopfAlgebras.LPlanarForestAlgebra.counit α R = (MonoidAlgebra.lift R R (HopfAlgebras.LPlanarForest α)) (HopfAlgebras.LPlanarForestAlgebra.counitMonoidHom✝ α R)

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.counit_ofForest {α : Type u} {R : Type v} [CommSemiring R] (ts : LPlanarForest α) : (counit α R) (ofForest ts) = counitCoeff ts

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.counit_ofForest_empty {α : Type u} {R : Type v} [CommSemiring R] : (counit α R) (ofForest LPlanarForest.empty) = 1

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.counit_ofForest_ne_nil {α : Type u} {R : Type v} [CommSemiring R] {ts : LPlanarForest α} (hts : ts ≠ []) : (counit α R) (ofForest ts) = 0

noncomputable def HopfAlgebras.LPlanarForestAlgebra.eraseLabels (α : Type u) (R : Type v) [CommSemiring R] : LPlanarForestAlgebra α R →ₐ[R] PlanarForestAlgebra R

Forget labels as an algebra morphism between ordered planar forest algebras.

Equations

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

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.eraseLabels_ofForest {α : Type u} {R : Type v} [CommSemiring R] (ts : LPlanarForest α) : (eraseLabels α R) (ofForest ts) = PlanarForestAlgebra.ofForest ts.erase

noncomputable def HopfAlgebras.LPlanarForestAlgebra.constLabel {α : Type u} (a : α) (R : Type v) [CommSemiring R] : PlanarForestAlgebra R →ₐ[R] LPlanarForestAlgebra α R

Label every vertex by a fixed label as an algebra morphism.

Equations

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

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.constLabel_ofForest {α : Type u} {R : Type v} [CommSemiring R] (a : α) (ts : PlanarForest) : (constLabel a R) (PlanarForestAlgebra.ofForest ts) = ofForest (LPlanarForest.constLabel a ts)

noncomputable def HopfAlgebras.LPlanarForestAlgebra.mapLabels {α : Type u} {β : Type w} (R : Type v) [CommSemiring R] (f : α → β) : LPlanarForestAlgebra α R →ₐ[R] LPlanarForestAlgebra β R

Relabel ordered planar forests as an algebra morphism.

Equations

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

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.mapLabels_ofForest {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (ts : LPlanarForest α) : (mapLabels R f) (ofForest ts) = ofForest (LPlanarForest.map f ts)

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.mapLabels_id {α : Type u} {R : Type v} [CommSemiring R] : (mapLabels R fun (a : α) => a) = AlgHom.id R (LPlanarForestAlgebra α R)

theorem HopfAlgebras.LPlanarForestAlgebra.mapLabels_comp {α : Type u} {β : Type w} {γ : Type x} {R : Type v} [CommSemiring R] (g : β → γ) (f : α → β) : (mapLabels R g).comp (mapLabels R f) = mapLabels R (g ∘ f)

noncomputable def HopfAlgebras.LPlanarForestAlgebra.toLForestAlgebra (α : Type u) (R : Type v) [CommSemiring R] : LPlanarForestAlgebra α R →ₐ[R] LForestAlgebra α R

Forget planar order as an algebra morphism to the commutative labelled forest algebra.

Equations

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

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.toLForestAlgebra_ofForest {α : Type u} {R : Type v} [CommSemiring R] (ts : LPlanarForest α) : (toLForestAlgebra α R) (ofForest ts) = LForestAlgebra.ofForest ts.toRootedForest

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.eraseLabels_comp_toLForestAlgebra {α : Type u} {R : Type v} [CommSemiring R] : (LForestAlgebra.eraseLabels R).comp (toLForestAlgebra α R) = (PlanarForestAlgebra.toForestAlgebra R).comp (eraseLabels α R)

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.counit_comp_toLForestAlgebra {α : Type u} {R : Type v} [CommSemiring R] : (LForestAlgebra.counit α R).comp (toLForestAlgebra α R) = counit α R

theorem HopfAlgebras.LPlanarForestAlgebra.eraseLabels_comp_mapLabels {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) : (eraseLabels β R).comp (mapLabels R f) = eraseLabels α R

theorem HopfAlgebras.LPlanarForestAlgebra.eraseLabels_comp_constLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) : (eraseLabels α R).comp (constLabel a R) = AlgHom.id R (PlanarForestAlgebra R)

theorem HopfAlgebras.LPlanarForestAlgebra.constLabel_injective {α : Type u} {R : Type v} [CommSemiring R] (a : α) : Function.Injective ⇑(constLabel a R)

theorem HopfAlgebras.LPlanarForestAlgebra.mapLabels_comp_constLabel {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (a : α) : (mapLabels R f).comp (constLabel a R) = constLabel (f a) R

@[reducible, inline]

abbrev HopfAlgebras.LPlanarForestAlgebra.Character (α : Type u) (R : Type v) [CommSemiring R] : Type (max u v)

Algebra characters on the labelled ordered planar forest algebra.

Equations

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

noncomputable def HopfAlgebras.LPlanarForestAlgebra.Character.evalForest {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) (ts : LPlanarForest α) : R

Evaluate a character on the monomial associated to a labelled ordered planar forest.

Equations

• χ.evalForest ts = χ (HopfAlgebras.LPlanarForestAlgebra.ofForest ts)

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.evalForest_empty {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) : χ.evalForest LPlanarForest.empty = 1

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.evalForest_nil {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) : χ.evalForest [] = 1

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.evalForest_append {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) (ts us : LPlanarForest α) : χ.evalForest (ts ++ us) = χ.evalForest ts * χ.evalForest us

theorem HopfAlgebras.LPlanarForestAlgebra.Character.ext {α : Type u} {R : Type v} [CommSemiring R] {χ ψ : Character α R} (h : ∀ (ts : LPlanarForest α), χ.evalForest ts = ψ.evalForest ts) : χ = ψ

theorem HopfAlgebras.LPlanarForestAlgebra.Character.ext_iff {α : Type u} {R : Type v} [CommSemiring R] {χ ψ : Character α R} : χ = ψ ↔ ∀ (ts : LPlanarForest α), χ.evalForest ts = ψ.evalForest ts

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

Pull a labelled commutative forest character back by forgetting planar order.

Equations

• HopfAlgebras.LPlanarForestAlgebra.Character.comapToLForestAlgebra χ = AlgHom.comp χ (HopfAlgebras.LPlanarForestAlgebra.toLForestAlgebra α R)

noncomputable def HopfAlgebras.LPlanarForestAlgebra.Character.comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ : PlanarForestAlgebra.Character R) : Character α R

Pull an unlabelled ordered planar forest character back by forgetting labels.

Equations

• HopfAlgebras.LPlanarForestAlgebra.Character.comapEraseLabels χ = AlgHom.comp χ (HopfAlgebras.LPlanarForestAlgebra.eraseLabels α R)

noncomputable def HopfAlgebras.LPlanarForestAlgebra.Character.comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) (χ : Character α R) : PlanarForestAlgebra.Character R

Pull a labelled ordered planar forest character back along constant labelling.

Equations

• HopfAlgebras.LPlanarForestAlgebra.Character.comapConstLabel a χ = AlgHom.comp χ (HopfAlgebras.LPlanarForestAlgebra.constLabel a R)

noncomputable def HopfAlgebras.LPlanarForestAlgebra.Character.comapMapLabels {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (χ : Character β R) : Character α R

Pull a labelled ordered planar forest character back along relabelling.

Equations

• HopfAlgebras.LPlanarForestAlgebra.Character.comapMapLabels f χ = AlgHom.comp χ (HopfAlgebras.LPlanarForestAlgebra.mapLabels R f)

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapToLForestAlgebra_evalForest {α : Type u} {R : Type v} [CommSemiring R] (χ : LForestAlgebra.Character α R) (ts : LPlanarForest α) : (comapToLForestAlgebra χ).evalForest ts = χ.evalForest ts.toRootedForest

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapEraseLabels_evalForest {α : Type u} {R : Type v} [CommSemiring R] (χ : PlanarForestAlgebra.Character R) (ts : LPlanarForest α) : (comapEraseLabels χ).evalForest ts = χ.evalForest ts.erase

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapConstLabel_evalForest {α : Type u} {R : Type v} [CommSemiring R] (a : α) (χ : Character α R) (ts : PlanarForest) : (comapConstLabel a χ).evalForest ts = χ.evalForest (LPlanarForest.constLabel a ts)

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapMapLabels_evalForest {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (χ : Character β R) (ts : LPlanarForest α) : (comapMapLabels f χ).evalForest ts = χ.evalForest (LPlanarForest.map f ts)

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapMapLabels_id {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) : comapMapLabels (fun (a : α) => a) χ = χ

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapMapLabels_comp {α : Type u} {β : Type w} {γ : Type x} {R : Type v} [CommSemiring R] (g : β → γ) (f : α → β) (χ : Character γ R) : comapMapLabels f (comapMapLabels g χ) = comapMapLabels (g ∘ f) χ

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapEraseLabels_comapMapLabels {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (χ : PlanarForestAlgebra.Character R) : comapMapLabels f (comapEraseLabels χ) = comapEraseLabels χ

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapConstLabel_comapMapLabels {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (a : α) (χ : Character β R) : comapConstLabel a (comapMapLabels f χ) = comapConstLabel (f a) χ

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapConstLabel_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (a : α) (χ : PlanarForestAlgebra.Character R) : comapConstLabel a (comapEraseLabels χ) = χ

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapToLForestAlgebra_counit {α : Type u} {R : Type v} [CommSemiring R] : comapToLForestAlgebra (LForestAlgebra.counit α R) = counit α R

@[simp]

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapEraseLabels_counit {α : Type u} {R : Type v} [CommSemiring R] : comapEraseLabels (PlanarForestAlgebra.counit R) = counit α R

theorem HopfAlgebras.LPlanarForestAlgebra.Character.comapConstLabel_counit {α : Type u} {R : Type v} [CommSemiring R] (a : α) : comapConstLabel a (counit α R) = PlanarForestAlgebra.counit R