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.
An algebra of an endofunctor; str
stands for "structure morphism"
Instances for category_theory.endofunctor.algebra
- category_theory.endofunctor.algebra.has_sizeof_inst
- category_theory.endofunctor.algebra.inhabited
- category_theory.endofunctor.algebra.category_theory.category_struct
- category_theory.endofunctor.algebra.category_theory.category
Equations
- category_theory.endofunctor.algebra.inhabited = {default := {A := inhabited.default _inst_2, str := 𝟙 ((𝟭 C).obj inhabited.default)}}
A morphism between algebras of endofunctor F
Instances for category_theory.endofunctor.algebra.hom
- category_theory.endofunctor.algebra.hom.has_sizeof_inst
- category_theory.endofunctor.algebra.hom.inhabited
The identity morphism of an algebra of endofunctor F
The composition of morphisms between algebras of endofunctor F
Algebras of an endofunctor F
form a category
To construct an isomorphism of algebras, it suffices to give an isomorphism of the As which commutes with the structure morphisms.
Equations
- category_theory.endofunctor.algebra.iso_mk h w = {hom := {f := h.hom, h' := w}, inv := {f := h.inv, h' := _}, hom_inv_id' := _, inv_hom_id' := _}
The forgetful functor from the category of algebras, forgetting the algebraic structure.
Equations
- category_theory.endofunctor.algebra.forget F = {obj := λ (A : category_theory.endofunctor.algebra F), A.A, map := λ (A B : category_theory.endofunctor.algebra F) (f : A ⟶ B), f.f, map_id' := _, map_comp' := _}
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
.
The identity transformation induces the identity endofunctor on the category of algebras.
Equations
- category_theory.endofunctor.algebra.functor_of_nat_trans_id = category_theory.nat_iso.of_components (λ (X : category_theory.endofunctor.algebra F), category_theory.endofunctor.algebra.iso_mk (category_theory.iso.refl ((category_theory.endofunctor.algebra.functor_of_nat_trans (𝟙 F)).obj X).A) _) category_theory.endofunctor.algebra.functor_of_nat_trans_id._proof_2
A composition of natural transformations gives the composition of corresponding functors.
Equations
- category_theory.endofunctor.algebra.functor_of_nat_trans_comp α β = category_theory.nat_iso.of_components (λ (X : category_theory.endofunctor.algebra F₂), category_theory.endofunctor.algebra.iso_mk (category_theory.iso.refl ((category_theory.endofunctor.algebra.functor_of_nat_trans (α ≫ β)).obj X).A) _) _
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
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
- category_theory.endofunctor.algebra.equiv_of_nat_iso α = {functor := category_theory.endofunctor.algebra.functor_of_nat_trans α.inv, inverse := category_theory.endofunctor.algebra.functor_of_nat_trans α.hom, unit_iso := category_theory.endofunctor.algebra.functor_of_nat_trans_id.symm ≪≫ category_theory.endofunctor.algebra.functor_of_nat_trans_eq _ ≪≫ category_theory.endofunctor.algebra.functor_of_nat_trans_comp α.hom α.inv, counit_iso := (category_theory.endofunctor.algebra.functor_of_nat_trans_comp α.inv α.hom).symm ≪≫ category_theory.endofunctor.algebra.functor_of_nat_trans_eq _ ≪≫ category_theory.endofunctor.algebra.functor_of_nat_trans_id, functor_unit_iso_comp' := _}
The inverse of the structure map of an initial algebra
The structure map of the inital algebra is an isomorphism, hence endofunctors preserve their initial algebras