# mathlibdocumentation

category_theory.endofunctor.algebra

# Algebras of endofunctors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines (co)algebras of an endofunctor, and provides the category instance for them. It also defines the forgetful functor from the category of (co)algebras. It is shown that the structure map of the initial algebra of an endofunctor is an isomorphism. Furthermore, it is shown that for an adjunction `F ⊣ G` the category of algebras over `F` is equivalent to the category of coalgebras over `G`.

## TODO #

• Prove the dual result about the structure map of the terminal coalgebra of an endofunctor.
• Prove that if the countable infinite product over the powers of the endofunctor exists, then algebras over the endofunctor coincide with algebras over the free monad on the endofunctor.
structure category_theory.endofunctor.algebra {C : Type u} (F : C C) :
Type (max u v)

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

Instances for `category_theory.endofunctor.algebra`
@[ext]

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} {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} {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'
def category_theory.endofunctor.algebra.hom.id {C : Type u} {F : C C}  :
A.hom A

The identity morphism of an algebra of endofunctor `F`

Equations
@[protected, instance]
Equations
def category_theory.endofunctor.algebra.hom.comp {C : Type u} {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
@[protected, instance]
Equations
@[simp]
theorem category_theory.endofunctor.algebra.id_eq_id {C : Type u} {F : C C}  :
@[simp]
theorem category_theory.endofunctor.algebra.id_f {C : Type u} {F : C C}  :
(𝟙 A).f = 𝟙 A.A
@[simp]
theorem category_theory.endofunctor.algebra.comp_eq_comp {C : Type u} {F : C C} {A₀ A₁ A₂ : category_theory.endofunctor.algebra F} (f : A₀ A₁) (g : A₁ A₂) :
@[simp]
theorem category_theory.endofunctor.algebra.comp_f {C : Type u} {F : C C} {A₀ A₁ A₂ : category_theory.endofunctor.algebra F} (f : A₀ A₁) (g : A₁ A₂) :
(f g).f = f.f g.f
@[protected, instance]

Algebras of an endofunctor `F` form a category

Equations
@[simp]
theorem category_theory.endofunctor.algebra.iso_mk_hom_f {C : Type u} {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) :
@[simp]
theorem category_theory.endofunctor.algebra.iso_mk_inv_f {C : Type u} {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) :
def category_theory.endofunctor.algebra.iso_mk {C : Type u} {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
@[simp]

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

Equations
Instances for `category_theory.endofunctor.algebra.forget`
@[simp]
theorem category_theory.endofunctor.algebra.forget_map {C : Type u} (F : C C) (f : A B) :
theorem category_theory.endofunctor.algebra.iso_of_iso {C : Type u} {F : C C} {A₀ A₁ : category_theory.endofunctor.algebra F} (f : A₀ A₁)  :

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

@[protected, instance]
@[protected, instance]
theorem category_theory.endofunctor.algebra.epi_of_epi {C : Type u} {F : C C} (f : X Y) [h : category_theory.epi f.f] :

An algebra morphism with an underlying epimorphism hom in `C` is an algebra epimorphism.

theorem category_theory.endofunctor.algebra.mono_of_mono {C : Type u} {F : C C} (f : X Y) [h : category_theory.mono f.f] :

An algebra morphism with an underlying monomorphism hom in `C` is an algebra monomorphism.

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

Equations
@[simp]
theorem category_theory.endofunctor.algebra.functor_of_nat_trans_obj_str {C : Type u} {F G : C C} (α : G F)  :
= α.app A.A A.str
@[simp]
theorem category_theory.endofunctor.algebra.functor_of_nat_trans_obj_A {C : Type u} {F G : C C} (α : G F)  :
@[simp]
theorem category_theory.endofunctor.algebra.functor_of_nat_trans_map_f {C : Type u} {F G : C C} (α : G F) (A₀ A₁ : category_theory.endofunctor.algebra F) (f : A₀ A₁) :
@[simp]

The identity transformation induces the identity endofunctor on the category of algebras.

Equations
@[simp]
@[simp]
theorem category_theory.endofunctor.algebra.functor_of_nat_trans_comp_hom_app_f {C : Type u} {F₀ F₁ F₂ : C C} (α : F₀ F₁) (β : F₁ F₂)  :
@[simp]
theorem category_theory.endofunctor.algebra.functor_of_nat_trans_comp_inv_app_f {C : Type u} {F₀ F₁ F₂ : C C} (α : F₀ F₁) (β : F₁ F₂)  :
def category_theory.endofunctor.algebra.functor_of_nat_trans_comp {C : Type u} {F₀ F₁ F₂ : C C} (α : F₀ F₁) (β : F₁ F₂) :

A composition of natural transformations gives the composition of corresponding functors.

Equations
def category_theory.endofunctor.algebra.functor_of_nat_trans_eq {C : Type u} {F G : C C} {α β : F G} (h : α = β) :

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]
theorem category_theory.endofunctor.algebra.functor_of_nat_trans_eq_hom_app_f {C : Type u} {F G : C C} {α β : F G} (h : α = β)  :
@[simp]
theorem category_theory.endofunctor.algebra.functor_of_nat_trans_eq_inv_app_f {C : Type u} {F G : C C} {α β : F G} (h : α = β)  :
@[simp]
def category_theory.endofunctor.algebra.equiv_of_nat_iso {C : Type u} {F G : C C} (α : F G) :

Naturally isomorphic endofunctors give equivalent categories of algebras. Furthermore, they are equivalent as categories over `C`, that is, we have `equiv_of_nat_iso h ⋙ forget = forget`.

Equations
@[simp]
@[simp]
@[simp]
@[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

structure category_theory.endofunctor.coalgebra {C : Type u} (F : C C) :
Type (max u v)

A coalgebra of an endofunctor; `str` stands for "structure morphism"

Instances for `category_theory.endofunctor.coalgebra`
@[protected, instance]
Equations
theorem category_theory.endofunctor.coalgebra.hom.ext {C : Type u} {_inst_1 : category_theory.category C} {F : C C} {V₀ V₁ : category_theory.endofunctor.coalgebra F} (x y : V₀.hom V₁) (h : x.f = y.f) :
x = y
theorem category_theory.endofunctor.coalgebra.hom.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {F : C C} {V₀ V₁ : category_theory.endofunctor.coalgebra F} (x y : V₀.hom V₁) :
x = y x.f = y.f
@[ext]

A morphism between coalgebras of an endofunctor `F`

Instances for `category_theory.endofunctor.coalgebra.hom`
@[simp]
theorem category_theory.endofunctor.coalgebra.hom.h {C : Type u} {F : C C} {V₀ V₁ : category_theory.endofunctor.coalgebra F} (self : V₀.hom V₁) :
V₀.str F.map self.f = self.f V₁.str
@[simp]
theorem category_theory.endofunctor.coalgebra.hom.h_assoc {C : Type u} {F : C C} {V₀ V₁ : category_theory.endofunctor.coalgebra F} (self : V₀.hom V₁) {X' : C} (f' : F.obj V₁.V X') :
V₀.str F.map self.f f' = self.f V₁.str f'

The identity morphism of an algebra of endofunctor `F`

Equations
@[protected, instance]
Equations
def category_theory.endofunctor.coalgebra.hom.comp {C : Type u} {F : C C} {V₀ V₁ V₂ : category_theory.endofunctor.coalgebra F} (f : V₀.hom V₁) (g : V₁.hom V₂) :
V₀.hom V₂

The composition of morphisms between algebras of endofunctor `F`

Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem category_theory.endofunctor.coalgebra.id_f {C : Type u} {F : C C}  :
(𝟙 V).f = 𝟙 V.V
@[simp]
theorem category_theory.endofunctor.coalgebra.comp_eq_comp {C : Type u} {F : C C} {V₀ V₁ V₂ : category_theory.endofunctor.coalgebra F} (f : V₀ V₁) (g : V₁ V₂) :
@[simp]
theorem category_theory.endofunctor.coalgebra.comp_f {C : Type u} {F : C C} {V₀ V₁ V₂ : category_theory.endofunctor.coalgebra F} (f : V₀ V₁) (g : V₁ V₂) :
(f g).f = f.f g.f
@[protected, instance]

Coalgebras of an endofunctor `F` form a category

Equations
@[simp]
theorem category_theory.endofunctor.coalgebra.iso_mk_hom_f {C : Type u} {F : C C} {V₀ V₁ : category_theory.endofunctor.coalgebra F} (h : V₀.V V₁.V) (w : V₀.str F.map h.hom = h.hom V₁.str) :
def category_theory.endofunctor.coalgebra.iso_mk {C : Type u} {F : C C} {V₀ V₁ : category_theory.endofunctor.coalgebra F} (h : V₀.V V₁.V) (w : V₀.str F.map h.hom = h.hom V₁.str) :
V₀ V₁

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

Equations
@[simp]
theorem category_theory.endofunctor.coalgebra.iso_mk_inv_f {C : Type u} {F : C C} {V₀ V₁ : category_theory.endofunctor.coalgebra F} (h : V₀.V V₁.V) (w : V₀.str F.map h.hom = h.hom V₁.str) :
@[simp]
@[simp]
theorem category_theory.endofunctor.coalgebra.forget_map {C : Type u} (F : C C) (f : A B) :

The forgetful functor from the category of coalgebras, forgetting the coalgebraic structure.

Equations
Instances for `category_theory.endofunctor.coalgebra.forget`
theorem category_theory.endofunctor.coalgebra.iso_of_iso {C : Type u} {F : C C} {V₀ V₁ : category_theory.endofunctor.coalgebra F} (f : V₀ V₁)  :

A coalgebra morphism with an underlying isomorphism hom in `C` is a coalgebra isomorphism.

@[protected, instance]
@[protected, instance]
theorem category_theory.endofunctor.coalgebra.epi_of_epi {C : Type u} {F : C C} (f : X Y) [h : category_theory.epi f.f] :

An algebra morphism with an underlying epimorphism hom in `C` is an algebra epimorphism.

theorem category_theory.endofunctor.coalgebra.mono_of_mono {C : Type u} {F : C C} (f : X Y) [h : category_theory.mono f.f] :

An algebra morphism with an underlying monomorphism hom in `C` is an algebra monomorphism.

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

Equations
@[simp]
theorem category_theory.endofunctor.coalgebra.functor_of_nat_trans_obj_str {C : Type u} {F G : C C} (α : F G)  :
= V.str α.app V.V
@[simp]
@[simp]
theorem category_theory.endofunctor.coalgebra.functor_of_nat_trans_map_f {C : Type u} {F G : C C} (α : F G) (V₀ V₁ : category_theory.endofunctor.coalgebra F) (f : V₀ V₁) :
@[simp]

The identity transformation induces the identity endofunctor on the category of coalgebras.

Equations
@[simp]
@[simp]
theorem category_theory.endofunctor.coalgebra.functor_of_nat_trans_comp_hom_app_f {C : Type u} {F₀ F₁ F₂ : C C} (α : F₀ F₁) (β : F₁ F₂)  :
def category_theory.endofunctor.coalgebra.functor_of_nat_trans_comp {C : Type u} {F₀ F₁ F₂ : C C} (α : F₀ F₁) (β : F₁ F₂) :

A composition of natural transformations gives the composition of corresponding functors.

Equations
@[simp]
theorem category_theory.endofunctor.coalgebra.functor_of_nat_trans_comp_inv_app_f {C : Type u} {F₀ F₁ F₂ : C C} (α : F₀ F₁) (β : F₁ F₂)  :
def category_theory.endofunctor.coalgebra.functor_of_nat_trans_eq {C : Type u} {F G : C C} {α β : F G} (h : α = β) :

If `α` and `β` are two equal natural transformations, then the functors of coalgebras 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]
theorem category_theory.endofunctor.coalgebra.functor_of_nat_trans_eq_inv_app_f {C : Type u} {F G : C C} {α β : F G} (h : α = β)  :
@[simp]
theorem category_theory.endofunctor.coalgebra.functor_of_nat_trans_eq_hom_app_f {C : Type u} {F G : C C} {α β : F G} (h : α = β)  :
def category_theory.endofunctor.coalgebra.equiv_of_nat_iso {C : Type u} {F G : C C} (α : F G) :

Naturally isomorphic endofunctors give equivalent categories of coalgebras. Furthermore, they are equivalent as categories over `C`, that is, we have `equiv_of_nat_iso h ⋙ forget = forget`.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
theorem category_theory.endofunctor.adjunction.algebra.hom_equiv_naturality_str {C : Type u} {F G : C C} (adj : F G) (A₁ A₂ : category_theory.endofunctor.algebra F) (f : A₁ A₂) :
(adj.hom_equiv A₁.A A₁.A) A₁.str G.map f.f = f.f (adj.hom_equiv A₂.A A₂.A) A₂.str
theorem category_theory.endofunctor.adjunction.coalgebra.hom_equiv_naturality_str_symm {C : Type u} {F G : C C} (adj : F G) (V₁ V₂ : category_theory.endofunctor.coalgebra G) (f : V₁ V₂) :
F.map f.f ((adj.hom_equiv V₂.V V₂.V).symm) V₂.str = ((adj.hom_equiv V₁.V V₁.V).symm) V₁.str f.f

Given an adjunction `F ⊣ G`, the functor that associates to an algebra over `F` a coalgebra over `G` defined via adjunction applied to the structure map.

Equations

Given an adjunction `F ⊣ G`, the functor that associates to a coalgebra over `G` an algebra over `F` defined via adjunction applied to the structure map.

Equations

Given an adjunction, assigning to an algebra over the left adjoint a coalgebra over its right adjoint and going back is isomorphic to the identity functor.

Equations

Given an adjunction, assigning to a coalgebra over the right adjoint an algebra over the left adjoint and going back is isomorphic to the identity functor.

Equations

If `F` is left adjoint to `G`, then the category of algebras over `F` is equivalent to the category of coalgebras over `G`.

Equations