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
- 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
@[protected, instance]
def
category_theory.endofunctor.algebra.inhabited
{C : Type u}
[category_theory.category C]
[inhabited C] :
Equations
- category_theory.endofunctor.algebra.inhabited = {default := {A := inhabited.default _inst_2, str := 𝟙 ((𝟭 C).obj inhabited.default)}}
@[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
- category_theory.endofunctor.algebra.hom.has_sizeof_inst
- category_theory.endofunctor.algebra.hom.inhabited
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₁) :
@[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₁) :
def
category_theory.endofunctor.algebra.hom.id
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(A : category_theory.endofunctor.algebra F) :
A.hom A
The identity morphism of an algebra of endofunctor F
@[protected, instance]
def
category_theory.endofunctor.algebra.hom.inhabited
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(A : category_theory.endofunctor.algebra F) :
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
@[protected, instance]
def
category_theory.endofunctor.algebra.category_theory.category_struct
{C : Type u}
[category_theory.category C]
(F : C ⥤ C) :
@[simp]
theorem
category_theory.endofunctor.algebra.id_eq_id
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(A : category_theory.endofunctor.algebra F) :
@[simp]
theorem
category_theory.endofunctor.algebra.id_f
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(A : category_theory.endofunctor.algebra F) :
@[simp]
theorem
category_theory.endofunctor.algebra.comp_eq_comp
{C : Type u}
[category_theory.category C]
{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}
[category_theory.category C]
{F : C ⥤ C}
{A₀ A₁ A₂ : category_theory.endofunctor.algebra F}
(f : A₀ ⟶ A₁)
(g : A₁ ⟶ A₂) :
@[protected, instance]
def
category_theory.endofunctor.algebra.category_theory.category
{C : Type u}
[category_theory.category C]
(F : C ⥤ C) :
Algebras of an endofunctor F form a category
@[simp]
theorem
category_theory.endofunctor.algebra.iso_mk_hom_f
{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) :
@[simp]
theorem
category_theory.endofunctor.algebra.iso_mk_inv_f
{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) :
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
- 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' := _}
@[simp]
theorem
category_theory.endofunctor.algebra.forget_obj
{C : Type u}
[category_theory.category C]
(F : C ⥤ C)
(A : category_theory.endofunctor.algebra F) :
def
category_theory.endofunctor.algebra.forget
{C : Type u}
[category_theory.category C]
(F : C ⥤ C) :
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
@[simp]
theorem
category_theory.endofunctor.algebra.forget_map
{C : Type u}
[category_theory.category C]
(F : C ⥤ C)
(A B : category_theory.endofunctor.algebra F)
(f : A ⟶ B) :
theorem
category_theory.endofunctor.algebra.iso_of_iso
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{A₀ A₁ : category_theory.endofunctor.algebra F}
(f : A₀ ⟶ A₁)
[category_theory.is_iso f.f] :
An algebra morphism with an underlying isomorphism hom in C is an algebra isomorphism.
@[protected, instance]
def
category_theory.endofunctor.algebra.forget_reflects_iso
{C : Type u}
[category_theory.category C]
{F : C ⥤ C} :
@[protected, instance]
def
category_theory.endofunctor.algebra.forget_faithful
{C : Type u}
[category_theory.category C]
{F : C ⥤ C} :
def
category_theory.endofunctor.algebra.functor_of_nat_trans
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : G ⟶ F) :
From a natural transformation α : G → F we get a functor from
algebras of F to algebras of G.
@[simp]
theorem
category_theory.endofunctor.algebra.functor_of_nat_trans_obj_str
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : G ⟶ F)
(A : category_theory.endofunctor.algebra F) :
@[simp]
theorem
category_theory.endofunctor.algebra.functor_of_nat_trans_obj_A
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : G ⟶ F)
(A : category_theory.endofunctor.algebra F) :
@[simp]
theorem
category_theory.endofunctor.algebra.functor_of_nat_trans_map_f
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : G ⟶ F)
(A₀ A₁ : category_theory.endofunctor.algebra F)
(f : A₀ ⟶ A₁) :
@[simp]
theorem
category_theory.endofunctor.algebra.functor_of_nat_trans_id_inv_app_f
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(X : category_theory.endofunctor.algebra F) :
def
category_theory.endofunctor.algebra.functor_of_nat_trans_id
{C : Type u}
[category_theory.category C]
{F : C ⥤ C} :
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
@[simp]
theorem
category_theory.endofunctor.algebra.functor_of_nat_trans_id_hom_app_f
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(X : category_theory.endofunctor.algebra F) :
@[simp]
theorem
category_theory.endofunctor.algebra.functor_of_nat_trans_comp_hom_app_f
{C : Type u}
[category_theory.category C]
{F₀ F₁ F₂ : C ⥤ C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂)
(X : category_theory.endofunctor.algebra F₂) :
@[simp]
theorem
category_theory.endofunctor.algebra.functor_of_nat_trans_comp_inv_app_f
{C : Type u}
[category_theory.category C]
{F₀ F₁ F₂ : C ⥤ C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂)
(X : category_theory.endofunctor.algebra F₂) :
def
category_theory.endofunctor.algebra.functor_of_nat_trans_comp
{C : Type u}
[category_theory.category C]
{F₀ F₁ F₂ : C ⥤ C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂) :
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) _) _
def
category_theory.endofunctor.algebra.functor_of_nat_trans_eq
{C : Type u}
[category_theory.category C]
{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}
[category_theory.category C]
{F G : C ⥤ C}
{α β : F ⟶ G}
(h : α = β)
(X : category_theory.endofunctor.algebra G) :
@[simp]
theorem
category_theory.endofunctor.algebra.functor_of_nat_trans_eq_inv_app_f
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
{α β : F ⟶ G}
(h : α = β)
(X : category_theory.endofunctor.algebra G) :
@[simp]
theorem
category_theory.endofunctor.algebra.equiv_of_nat_iso_counit_iso
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ≅ G) :
def
category_theory.endofunctor.algebra.equiv_of_nat_iso
{C : Type u}
[category_theory.category C]
{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
- 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' := _}
@[simp]
theorem
category_theory.endofunctor.algebra.equiv_of_nat_iso_inverse
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ≅ G) :
@[simp]
theorem
category_theory.endofunctor.algebra.equiv_of_nat_iso_unit_iso
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ≅ G) :
@[simp]
theorem
category_theory.endofunctor.algebra.equiv_of_nat_iso_functor
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ≅ G) :
@[simp]
def
category_theory.endofunctor.algebra.initial.str_inv
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{A : category_theory.endofunctor.algebra F}
(h : category_theory.limits.is_initial A) :
The inverse of the structure map of an initial algebra
theorem
category_theory.endofunctor.algebra.initial.left_inv'
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{A : category_theory.endofunctor.algebra F}
(h : category_theory.limits.is_initial A) :
theorem
category_theory.endofunctor.algebra.initial.left_inv
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{A : category_theory.endofunctor.algebra F}
(h : category_theory.limits.is_initial A) :
theorem
category_theory.endofunctor.algebra.initial.right_inv
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{A : category_theory.endofunctor.algebra F}
(h : category_theory.limits.is_initial A) :
theorem
category_theory.endofunctor.algebra.initial.str_is_iso
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{A : category_theory.endofunctor.algebra F}
(h : category_theory.limits.is_initial A) :
The structure map of the inital algebra is an isomorphism, hence endofunctors preserve their initial algebras