Documentation

HopfAlgebras.Algebra.LabelledForest

The Algebra of Labelled Rooted Forests #

This file defines the commutative algebra freely spanned by labelled rooted forests. It is the labelled analogue of HopfAlgebras.Algebra.Forest.

Main definitions #

LForestAlgebra - monoid algebra of labelled rooted forests
LForestAlgebra.ofForest - the monomial associated to a labelled forest
LForestAlgebra.eraseLabels - forget labels as an algebra morphism
LForestAlgebra.constLabel - label every vertex by a fixed label as an algebra morphism
LForestAlgebra.mapLabels - relabel forests as an algebra morphism
LForestAlgebra.counit - algebra counit sending the empty forest to 1
LForestAlgebra.Character - algebra characters on labelled forest algebra

@[reducible, inline]

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

Type (max u v)

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

Equations

HopfAlgebras.LForestAlgebra α R = AddMonoidAlgebra R (HopfAlgebras.LRootedForest α)

Instances For

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

LForestAlgebra α R

The monomial associated to a labelled rooted forest.

Equations

HopfAlgebras.LForestAlgebra.ofForest φ = AddMonoidAlgebra.single φ 1

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.ofForest_zero {α : Type u} {R : Type v} [Semiring R] :

@[simp]

theorem HopfAlgebras.LForestAlgebra.ofForest_empty {α : Type u} {R : Type v} [Semiring R] :

ofForest LRootedForest.empty = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.ofForest_add {α : Type u} {R : Type v} [Semiring R] (φ ψ : LRootedForest α) :

ofForest (φ + ψ) = ofForest φ * ofForest ψ

noncomputable def HopfAlgebras.LForestAlgebra.eraseLabels {α : Type u} (R : Type v) [CommSemiring R] :

LForestAlgebra α R →ₐ[R] ForestAlgebra R

Forget labels as an algebra morphism from labelled to unlabelled forest algebra.

Equations

HopfAlgebras.LForestAlgebra.eraseLabels R = (AddMonoidAlgebra.lift R (HopfAlgebras.ForestAlgebra R) (HopfAlgebras.LRootedForest α)) (HopfAlgebras.LForestAlgebra.eraseLabelsMonoidHom✝ α R)

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.eraseLabels_ofForest {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) :

(eraseLabels R) (ofForest φ) = ForestAlgebra.ofForest φ.erase

@[simp]

theorem HopfAlgebras.LForestAlgebra.eraseLabels_ofForest_zero {α : Type u} {R : Type v} [CommSemiring R] :

(eraseLabels R) (ofForest 0) = 1

noncomputable def HopfAlgebras.LForestAlgebra.constLabel {α : Type u} (a : α) (R : Type v) [CommSemiring R] :

ForestAlgebra R →ₐ[R] LForestAlgebra α R

Label every vertex as an algebra morphism from unlabelled to labelled forests.

Equations

HopfAlgebras.LForestAlgebra.constLabel a R = (AddMonoidAlgebra.lift R (HopfAlgebras.LForestAlgebra α R) HopfAlgebras.RootedForest) (HopfAlgebras.LForestAlgebra.constLabelMonoidHom✝ a R)

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.constLabel_ofForest {α : Type u} {R : Type v} [CommSemiring R] (a : α) (φ : RootedForest) :

(constLabel a R) (ForestAlgebra.ofForest φ) = ofForest (LRootedForest.constLabel a φ)

@[simp]

theorem HopfAlgebras.LForestAlgebra.constLabel_ofForest_zero {α : Type u} {R : Type v} [CommSemiring R] (a : α) :

(constLabel a R) (ForestAlgebra.ofForest 0) = 1

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

LForestAlgebra α R →ₐ[R] LForestAlgebra β R

Relabel labelled forests as an algebra morphism.

Equations

HopfAlgebras.LForestAlgebra.mapLabels R f = (AddMonoidAlgebra.lift R (HopfAlgebras.LForestAlgebra β R) (HopfAlgebras.LRootedForest α)) (HopfAlgebras.LForestAlgebra.mapLabelsMonoidHom✝ f R)

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.mapLabels_ofForest {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (φ : LRootedForest α) :

(mapLabels R f) (ofForest φ) = ofForest (LRootedForest.mapLabels f φ)

@[simp]

theorem HopfAlgebras.LForestAlgebra.mapLabels_ofForest_zero {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) :

(mapLabels R f) (ofForest 0) = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.mapLabels_id {α : Type u} {R : Type v} [CommSemiring R] :

(mapLabels R fun (a : α) => a) = AlgHom.id R (LForestAlgebra α R)

theorem HopfAlgebras.LForestAlgebra.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)

theorem HopfAlgebras.LForestAlgebra.eraseLabels_comp_mapLabels {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) :

(eraseLabels R).comp (mapLabels R f) = eraseLabels R

theorem HopfAlgebras.LForestAlgebra.eraseLabels_comp_constLabel {α : Type u} {R : Type v} [CommSemiring R] (a : α) :

(eraseLabels R).comp (constLabel a R) = AlgHom.id R (ForestAlgebra R)

theorem HopfAlgebras.LForestAlgebra.constLabel_injective {α : Type u} {R : Type v} [CommSemiring R] (a : α) :

Function.Injective ⇑(constLabel a R)

theorem HopfAlgebras.LForestAlgebra.constLabel_eq_constLabel_iff {α : Type u} {R : Type v} [CommSemiring R] (a : α) {x y : ForestAlgebra R} :

(constLabel a R) x = (constLabel a R) y ↔ x = y

theorem HopfAlgebras.LForestAlgebra.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

noncomputable def HopfAlgebras.LForestAlgebra.counitCoeff {α : Type u} {R : Type v} [Zero R] [One R] (φ : LRootedForest α) :

R

The counit value on a labelled forest monomial.

Equations

HopfAlgebras.LForestAlgebra.counitCoeff φ = if φ = 0 then 1 else 0

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.counitCoeff_zero {α : Type u} {R : Type v} [Zero R] [One R] :

counitCoeff 0 = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.counitCoeff_empty {α : Type u} {R : Type v} [Zero R] [One R] :

counitCoeff LRootedForest.empty = 1

theorem HopfAlgebras.LForestAlgebra.counitCoeff_ne_zero {α : Type u} {R : Type v} [Zero R] [One R] {φ : LRootedForest α} (hφ : φ ≠ 0) :

counitCoeff φ = 0

theorem HopfAlgebras.LForestAlgebra.counitCoeff_add {α : Type u} {R : Type v} [Semiring R] (φ ψ : LRootedForest α) :

counitCoeff (φ + ψ) = counitCoeff φ * counitCoeff ψ

theorem HopfAlgebras.LForestAlgebra.counitCoeff_mapLabels {α : Type u} {β : Type w} {R : Type v} [Zero R] [One R] (f : α → β) (φ : LRootedForest α) :

counitCoeff (LRootedForest.mapLabels f φ) = counitCoeff φ

theorem HopfAlgebras.LForestAlgebra.counitCoeff_erase {α : Type u} {R : Type v} [Zero R] [One R] (φ : LRootedForest α) :

ForestAlgebra.counitCoeff φ.erase = counitCoeff φ

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

LForestAlgebra α R →ₐ[R] R

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

Equations

HopfAlgebras.LForestAlgebra.counit α R = (AddMonoidAlgebra.lift R R (HopfAlgebras.LRootedForest α)) (HopfAlgebras.LForestAlgebra.counitMonoidHom✝ α R)

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.counit_ofForest {α : Type u} {R : Type v} [CommSemiring R] (φ : LRootedForest α) :

(counit α R) (ofForest φ) = counitCoeff φ

@[simp]

theorem HopfAlgebras.LForestAlgebra.counit_ofForest_zero {α : Type u} {R : Type v} [CommSemiring R] :

(counit α R) (ofForest 0) = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.counit_ofForest_ne_zero {α : Type u} {R : Type v} [CommSemiring R] {φ : LRootedForest α} (hφ : φ ≠ 0) :

(counit α R) (ofForest φ) = 0

theorem HopfAlgebras.LForestAlgebra.counit_comp_mapLabels {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) :

(counit β R).comp (mapLabels R f) = counit α R

theorem HopfAlgebras.LForestAlgebra.counit_comp_eraseLabels {α : Type u} {R : Type v} [CommSemiring R] :

(ForestAlgebra.counit R).comp (eraseLabels R) = counit α R

@[reducible, inline]

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

Type (max u v)

Algebra characters on the labelled rooted-forest algebra.

Equations

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

Instances For

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

R

Evaluate a labelled-forest character on one forest monomial.

Equations

χ.evalForest φ = χ (HopfAlgebras.LForestAlgebra.ofForest φ)

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.evalForest_zero {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) :

χ.evalForest 0 = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.evalForest_empty {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) :

χ.evalForest LRootedForest.empty = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.evalForest_add {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) (φ ψ : LRootedForest α) :

χ.evalForest (φ + ψ) = χ.evalForest φ * χ.evalForest ψ

theorem HopfAlgebras.LForestAlgebra.Character.evalForest_ofPLTree_list_perm {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) {ts us : List (PLTree α)} (h : ts.Perm us) :

χ.evalForest ↑(List.map LRootedTree.ofPLTree ts) = χ.evalForest ↑(List.map LRootedTree.ofPLTree us)

theorem HopfAlgebras.LForestAlgebra.Character.evalForest_ofPLTree_list_forall₂_perm {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) {ts us : List (PLTree α)} (h : List.Forall₂ PLTree.Perm ts us) :

χ.evalForest ↑(List.map LRootedTree.ofPLTree ts) = χ.evalForest ↑(List.map LRootedTree.ofPLTree us)

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

χ = ψ

theorem HopfAlgebras.LForestAlgebra.Character.ext_iff {α : Type u} {R : Type v} [CommSemiring R] {χ ψ : Character α R} :

χ = ψ ↔ ∀ (φ : LRootedForest α), χ.evalForest φ = ψ.evalForest φ

theorem HopfAlgebras.LForestAlgebra.Character.ext_tree {α : Type u} {R : Type v} [CommSemiring R] {χ ψ : Character α R} (h : ∀ (τ : LRootedTree α), χ.evalForest (LRootedForest.singleton τ) = ψ.evalForest (LRootedForest.singleton τ)) :

χ = ψ

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.map_ofForest_zero {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) :

χ (ofForest 0) = 1

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.map_ofForest_empty {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) :

χ (ofForest LRootedForest.empty) = 1

theorem HopfAlgebras.LForestAlgebra.Character.map_ofForest_add {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) (φ ψ : LRootedForest α) :

χ (ofForest (φ + ψ)) = χ (ofForest φ) * χ (ofForest ψ)

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

Pull a labelled-forest character back along a relabelling map.

Equations

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

Instances For

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

Pull an unlabelled forest character back by forgetting labels.

Equations

HopfAlgebras.LForestAlgebra.Character.comapEraseLabels χ = AlgHom.comp χ (HopfAlgebras.LForestAlgebra.eraseLabels R)

Instances For

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

ForestAlgebra.Character R

Pull a labelled-forest character back along constant labelling.

Equations

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

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.comapMapLabels_evalForest {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (χ : Character β R) (φ : LRootedForest α) :

(comapMapLabels f χ).evalForest φ = χ.evalForest (LRootedForest.mapLabels f φ)

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.comapEraseLabels_evalForest {α : Type u} {R : Type v} [CommSemiring R] (χ : ForestAlgebra.Character R) (φ : LRootedForest α) :

(comapEraseLabels χ).evalForest φ = χ (ForestAlgebra.ofForest φ.erase)

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.comapConstLabel_evalForest {α : Type u} {R : Type v} [CommSemiring R] (a : α) (χ : Character α R) (φ : RootedForest) :

(comapConstLabel a χ).evalForest φ = χ.evalForest (LRootedForest.constLabel a φ)

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.comapMapLabels_id {α : Type u} {R : Type v} [CommSemiring R] (χ : Character α R) :

comapMapLabels (fun (a : α) => a) χ = χ

theorem HopfAlgebras.LForestAlgebra.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.LForestAlgebra.Character.comapEraseLabels_comapMapLabels {α : Type u} {β : Type w} {R : Type v} [CommSemiring R] (f : α → β) (χ : ForestAlgebra.Character R) :

comapMapLabels f (comapEraseLabels χ) = comapEraseLabels χ

theorem HopfAlgebras.LForestAlgebra.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.LForestAlgebra.Character.comapConstLabel_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (a : α) (χ : ForestAlgebra.Character R) :

comapConstLabel a (comapEraseLabels χ) = χ

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

comapMapLabels f (counit β R) = counit α R

theorem HopfAlgebras.LForestAlgebra.Character.comapEraseLabels_counit {α : Type u} {R : Type v} [CommSemiring R] :

comapEraseLabels (ForestAlgebra.counit R) = counit α R

theorem HopfAlgebras.LForestAlgebra.Character.comapConstLabel_counit {α : Type u} {R : Type v} [CommSemiring R] (a : α) :

comapConstLabel a (counit α R) = ForestAlgebra.counit R

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

A labelled forest character whose values only depend on the unlabelled forest.

Equations

χ.LabelInvariant = ∀ (φ ψ : HopfAlgebras.LRootedForest α), φ.erase = ψ.erase → χ.evalForest φ = χ.evalForest ψ

Instances For

theorem HopfAlgebras.LForestAlgebra.Character.LabelInvariant.evalForest_eq {α : Type u} {R : Type v} [CommSemiring R] {χ : Character α R} (h : χ.LabelInvariant) {φ ψ : LRootedForest α} (hφψ : φ.erase = ψ.erase) :

χ.evalForest φ = χ.evalForest ψ

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariant_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] (χ : ForestAlgebra.Character R) :

(comapEraseLabels χ).LabelInvariant

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariant_counit {α : Type u} {R : Type v} [CommSemiring R] :

LabelInvariant (counit α R)

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

(Character.comapMapLabels f χ).LabelInvariant

theorem HopfAlgebras.LForestAlgebra.Character.LabelInvariant.comapConstLabel_eq {α : Type u} {R : Type v} [CommSemiring R] {χ : Character α R} (h : χ.LabelInvariant) (x y : α) :

comapConstLabel x χ = comapConstLabel y χ

theorem HopfAlgebras.LForestAlgebra.Character.LabelInvariant.comapEraseLabels_comapConstLabel {α : Type u} {R : Type v} [CommSemiring R] {χ : Character α R} (h : χ.LabelInvariant) (x : α) :

comapEraseLabels (comapConstLabel x χ) = χ

noncomputable def HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] :

ForestAlgebra.Character R ≃ { χ : Character α R // χ.LabelInvariant }

Unlabelled forest characters are equivalent to label-invariant labelled characters.

Equations

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

Instances For

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv_apply {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] (χ : ForestAlgebra.Character R) :

↑(labelInvariantEquiv χ) = comapEraseLabels χ

@[simp]

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv_symm_apply {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] (χ : { χ : Character α R // χ.LabelInvariant }) :

labelInvariantEquiv.symm χ = comapConstLabel (Classical.choice ⋯) ↑χ

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv_counit {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] :

labelInvariantEquiv (ForestAlgebra.counit R) = ⟨counit α R, ⋯⟩

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariantEquiv_symm_counit {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] :

labelInvariantEquiv.symm ⟨counit α R, ⋯⟩ = ForestAlgebra.counit R

theorem HopfAlgebras.LForestAlgebra.Character.labelInvariant_iff_exists_comapEraseLabels {α : Type u} {R : Type v} [CommSemiring R] [Nonempty α] (χ : Character α R) :

χ.LabelInvariant ↔ ∃ (ψ : ForestAlgebra.Character R), comapEraseLabels ψ = χ