mathlib documentation

category_theory.endofunctor.algebra

Algebras of endofunctors #

This file defines algebras of an endofunctor, and provides the category instance for them. This extends to Eilenberg-Moore (co)algebras for a (co)monad. It also defines the forgetful functor from the category of algebras. It is shown that the structure map of the initial algebra of an endofunctor is an isomorphism.

structure category_theory.endofunctor.algebra {C : Type u} [category_theory.category C] (F : C C) :
Type (max u v)

An algebra of an endofunctor; str stands for "structure morphism"

Instances for category_theory.endofunctor.algebra
@[ext]
structure category_theory.endofunctor.algebra.hom {C : Type u} [category_theory.category C] {F : C C} (A₀ A₁ : category_theory.endofunctor.algebra F) :
Type v

A morphism between algebras of endofunctor F

Instances for category_theory.endofunctor.algebra.hom
theorem category_theory.endofunctor.algebra.hom.ext {C : Type u} {_inst_1 : category_theory.category C} {F : C C} {A₀ A₁ : category_theory.endofunctor.algebra F} (x y : A₀.hom A₁) (h : x.f = y.f) :
x = y
theorem category_theory.endofunctor.algebra.hom.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {F : C C} {A₀ A₁ : category_theory.endofunctor.algebra F} (x y : A₀.hom A₁) :
x = y x.f = y.f
@[simp]
theorem category_theory.endofunctor.algebra.hom.h {C : Type u} [category_theory.category C] {F : C C} {A₀ A₁ : category_theory.endofunctor.algebra F} (self : A₀.hom A₁) :
F.map self.f A₁.str = A₀.str self.f
@[simp]
theorem category_theory.endofunctor.algebra.hom.h_assoc {C : Type u} [category_theory.category C] {F : C C} {A₀ A₁ : category_theory.endofunctor.algebra F} (self : A₀.hom A₁) {X' : C} (f' : A₁.A X') :
F.map self.f A₁.str f' = A₀.str self.f f'

The identity morphism of an algebra of endofunctor F

Equations
def category_theory.endofunctor.algebra.hom.comp {C : Type u} [category_theory.category C] {F : C C} {A₀ A₁ A₂ : category_theory.endofunctor.algebra F} (f : A₀.hom A₁) (g : A₁.hom A₂) :
A₀.hom A₂

The composition of morphisms between algebras of endofunctor F

Equations
@[simp]
@[simp]
theorem category_theory.endofunctor.algebra.comp_f {C : Type u} [category_theory.category C] {F : C C} {A₀ A₁ A₂ : category_theory.endofunctor.algebra F} (f : A₀ A₁) (g : A₁ A₂) :
(f g).f = f.f g.f
@[simp]
@[simp]
def category_theory.endofunctor.algebra.iso_mk {C : Type u} [category_theory.category C] {F : C C} {A₀ A₁ : category_theory.endofunctor.algebra F} (h : A₀.A A₁.A) (w : F.map h.hom A₁.str = A₀.str h.hom) :
A₀ A₁

To construct an isomorphism of algebras, it suffices to give an isomorphism of the As which commutes with the structure morphisms.

Equations

The forgetful functor from the category of algebras, forgetting the algebraic structure.

Equations
Instances for category_theory.endofunctor.algebra.forget

An algebra morphism with an underlying isomorphism hom in C is an algebra isomorphism.

From a natural transformation α : G → F we get a functor from algebras of F to algebras of G.

Equations

If α and β are two equal natural transformations, then the functors of algebras induced by them are isomorphic. We define it like this as opposed to using eq_to_iso so that the components are nicer to prove lemmas about.

Equations
@[simp]

The inverse of the structure map of an initial algebra

Equations

The structure map of the inital algebra is an isomorphism, hence endofunctors preserve their initial algebras