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}
[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
- category_theory.endofunctor.algebra_preadditive
@[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]
@[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
- 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]
@[protected, instance]
def
category_theory.endofunctor.algebra.forget_faithful
{C : Type u}
[category_theory.category C]
{F : C ⥤ C} :
theorem
category_theory.endofunctor.algebra.epi_of_epi
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{X Y : category_theory.endofunctor.algebra F}
(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}
[category_theory.category C]
{F : C ⥤ C}
{X Y : category_theory.endofunctor.algebra F}
(f : X ⟶ Y)
[h : category_theory.mono f.f] :
An algebra morphism with an underlying monomorphism hom in C is an algebra monomorphism.
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
structure
category_theory.endofunctor.coalgebra
{C : Type u}
[category_theory.category C]
(F : C ⥤ C) :
Type (max u v)
A coalgebra of an endofunctor; str stands for "structure morphism"
Instances for category_theory.endofunctor.coalgebra
- category_theory.endofunctor.coalgebra.has_sizeof_inst
- category_theory.endofunctor.coalgebra.inhabited
- category_theory.endofunctor.coalgebra.category_theory.category_struct
- category_theory.endofunctor.coalgebra.category_theory.category
- category_theory.endofunctor.coalgebra_preadditive
@[protected, instance]
def
category_theory.endofunctor.coalgebra.inhabited
{C : Type u}
[category_theory.category C]
[inhabited C] :
Equations
- category_theory.endofunctor.coalgebra.inhabited = {default := {V := inhabited.default _inst_2, str := 𝟙 inhabited.default}}
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₁) :
@[ext]
structure
category_theory.endofunctor.coalgebra.hom
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(V₀ V₁ : category_theory.endofunctor.coalgebra F) :
Type v
A morphism between coalgebras of an endofunctor F
Instances for category_theory.endofunctor.coalgebra.hom
- category_theory.endofunctor.coalgebra.hom.has_sizeof_inst
- category_theory.endofunctor.coalgebra.hom.inhabited
@[simp]
theorem
category_theory.endofunctor.coalgebra.hom.h
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{V₀ V₁ : category_theory.endofunctor.coalgebra F}
(self : V₀.hom V₁) :
def
category_theory.endofunctor.coalgebra.hom.id
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(V : category_theory.endofunctor.coalgebra F) :
V.hom V
The identity morphism of an algebra of endofunctor F
@[protected, instance]
def
category_theory.endofunctor.coalgebra.hom.inhabited
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(V : category_theory.endofunctor.coalgebra F) :
def
category_theory.endofunctor.coalgebra.hom.comp
{C : Type u}
[category_theory.category C]
{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
@[protected, instance]
def
category_theory.endofunctor.coalgebra.category_theory.category_struct
{C : Type u}
[category_theory.category C]
(F : C ⥤ C) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.id_eq_id
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(V : category_theory.endofunctor.coalgebra F) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.id_f
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(V : category_theory.endofunctor.coalgebra F) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.comp_eq_comp
{C : Type u}
[category_theory.category C]
{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}
[category_theory.category C]
{F : C ⥤ C}
{V₀ V₁ V₂ : category_theory.endofunctor.coalgebra F}
(f : V₀ ⟶ V₁)
(g : V₁ ⟶ V₂) :
@[protected, instance]
def
category_theory.endofunctor.coalgebra.category_theory.category
{C : Type u}
[category_theory.category C]
(F : C ⥤ C) :
Coalgebras of an endofunctor F form a category
@[simp]
def
category_theory.endofunctor.coalgebra.iso_mk
{C : Type u}
[category_theory.category C]
{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
- category_theory.endofunctor.coalgebra.iso_mk h w = {hom := {f := h.hom, h' := w}, inv := {f := h.inv, h' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
@[simp]
theorem
category_theory.endofunctor.coalgebra.forget_obj
{C : Type u}
[category_theory.category C]
(F : C ⥤ C)
(A : category_theory.endofunctor.coalgebra F) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.forget_map
{C : Type u}
[category_theory.category C]
(F : C ⥤ C)
(A B : category_theory.endofunctor.coalgebra F)
(f : A ⟶ B) :
def
category_theory.endofunctor.coalgebra.forget
{C : Type u}
[category_theory.category C]
(F : C ⥤ C) :
The forgetful functor from the category of coalgebras, forgetting the coalgebraic structure.
Equations
- category_theory.endofunctor.coalgebra.forget F = {obj := λ (A : category_theory.endofunctor.coalgebra F), A.V, map := λ (A B : category_theory.endofunctor.coalgebra F) (f : A ⟶ B), f.f, map_id' := _, map_comp' := _}
Instances for category_theory.endofunctor.coalgebra.forget
theorem
category_theory.endofunctor.coalgebra.iso_of_iso
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
{V₀ V₁ : category_theory.endofunctor.coalgebra F}
(f : V₀ ⟶ V₁)
[category_theory.is_iso f.f] :
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}
[category_theory.category C]
{F : C ⥤ C}
{X Y : category_theory.endofunctor.coalgebra F}
(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}
[category_theory.category C]
{F : C ⥤ C}
{X Y : category_theory.endofunctor.coalgebra F}
(f : X ⟶ Y)
[h : category_theory.mono f.f] :
An algebra morphism with an underlying monomorphism hom in C is an algebra monomorphism.
def
category_theory.endofunctor.coalgebra.functor_of_nat_trans
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ⟶ G) :
From a natural transformation α : F → G we get a functor from
coalgebras of F to coalgebras of G.
@[simp]
theorem
category_theory.endofunctor.coalgebra.functor_of_nat_trans_obj_str
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ⟶ G)
(V : category_theory.endofunctor.coalgebra F) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.functor_of_nat_trans_obj_V
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ⟶ G)
(V : category_theory.endofunctor.coalgebra F) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.functor_of_nat_trans_map_f
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ⟶ G)
(V₀ V₁ : category_theory.endofunctor.coalgebra F)
(f : V₀ ⟶ V₁) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.functor_of_nat_trans_id_inv_app_f
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(X : category_theory.endofunctor.coalgebra F) :
def
category_theory.endofunctor.coalgebra.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 coalgebras.
Equations
- category_theory.endofunctor.coalgebra.functor_of_nat_trans_id = category_theory.nat_iso.of_components (λ (X : category_theory.endofunctor.coalgebra F), category_theory.endofunctor.coalgebra.iso_mk (category_theory.iso.refl ((category_theory.endofunctor.coalgebra.functor_of_nat_trans (𝟙 F)).obj X).V) _) category_theory.endofunctor.coalgebra.functor_of_nat_trans_id._proof_2
@[simp]
theorem
category_theory.endofunctor.coalgebra.functor_of_nat_trans_id_hom_app_f
{C : Type u}
[category_theory.category C]
{F : C ⥤ C}
(X : category_theory.endofunctor.coalgebra F) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.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.coalgebra F₀) :
def
category_theory.endofunctor.coalgebra.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.coalgebra.functor_of_nat_trans_comp α β = category_theory.nat_iso.of_components (λ (X : category_theory.endofunctor.coalgebra F₀), category_theory.endofunctor.coalgebra.iso_mk (category_theory.iso.refl ((category_theory.endofunctor.coalgebra.functor_of_nat_trans (α ≫ β)).obj X).V) _) _
@[simp]
theorem
category_theory.endofunctor.coalgebra.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.coalgebra F₀) :
def
category_theory.endofunctor.coalgebra.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 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
- category_theory.endofunctor.coalgebra.functor_of_nat_trans_eq h = category_theory.nat_iso.of_components (λ (X : category_theory.endofunctor.coalgebra F), category_theory.endofunctor.coalgebra.iso_mk (category_theory.iso.refl ((category_theory.endofunctor.coalgebra.functor_of_nat_trans α).obj X).V) _) _
@[simp]
theorem
category_theory.endofunctor.coalgebra.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.coalgebra F) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.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.coalgebra F) :
def
category_theory.endofunctor.coalgebra.equiv_of_nat_iso
{C : Type u}
[category_theory.category C]
{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
- category_theory.endofunctor.coalgebra.equiv_of_nat_iso α = {functor := category_theory.endofunctor.coalgebra.functor_of_nat_trans α.hom, inverse := category_theory.endofunctor.coalgebra.functor_of_nat_trans α.inv, unit_iso := category_theory.endofunctor.coalgebra.functor_of_nat_trans_id.symm ≪≫ category_theory.endofunctor.coalgebra.functor_of_nat_trans_eq _ ≪≫ category_theory.endofunctor.coalgebra.functor_of_nat_trans_comp α.hom α.inv, counit_iso := (category_theory.endofunctor.coalgebra.functor_of_nat_trans_comp α.inv α.hom).symm ≪≫ category_theory.endofunctor.coalgebra.functor_of_nat_trans_eq _ ≪≫ category_theory.endofunctor.coalgebra.functor_of_nat_trans_id, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.endofunctor.coalgebra.equiv_of_nat_iso_unit_iso
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ≅ G) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.equiv_of_nat_iso_inverse
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ≅ G) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.equiv_of_nat_iso_functor
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ≅ G) :
@[simp]
theorem
category_theory.endofunctor.coalgebra.equiv_of_nat_iso_counit_iso
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(α : F ≅ G) :
theorem
category_theory.endofunctor.adjunction.algebra.hom_equiv_naturality_str
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(adj : F ⊣ G)
(A₁ A₂ : category_theory.endofunctor.algebra F)
(f : A₁ ⟶ A₂) :
theorem
category_theory.endofunctor.adjunction.coalgebra.hom_equiv_naturality_str_symm
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(adj : F ⊣ G)
(V₁ V₂ : category_theory.endofunctor.coalgebra G)
(f : V₁ ⟶ V₂) :
def
category_theory.endofunctor.adjunction.algebra.to_coalgebra_of
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(adj : F ⊣ G) :
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
- category_theory.endofunctor.adjunction.algebra.to_coalgebra_of adj = {obj := λ (A : category_theory.endofunctor.algebra F), {V := A.A, str := (adj.hom_equiv A.A A.A).to_fun A.str}, map := λ (A₁ A₂ : category_theory.endofunctor.algebra F) (f : A₁ ⟶ A₂), {f := f.f, h' := _}, map_id' := _, map_comp' := _}
def
category_theory.endofunctor.adjunction.coalgebra.to_algebra_of
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(adj : F ⊣ G) :
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
- category_theory.endofunctor.adjunction.coalgebra.to_algebra_of adj = {obj := λ (V : category_theory.endofunctor.coalgebra G), {A := V.V, str := (adj.hom_equiv V.V V.V).inv_fun V.str}, map := λ (V₁ V₂ : category_theory.endofunctor.coalgebra G) (f : V₁ ⟶ V₂), {f := f.f, h' := _}, map_id' := _, map_comp' := _}
def
category_theory.endofunctor.adjunction.alg_coalg_equiv.unit_iso
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(adj : F ⊣ G) :
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
- category_theory.endofunctor.adjunction.alg_coalg_equiv.unit_iso adj = {hom := {app := λ (A : category_theory.endofunctor.algebra F), {f := 𝟙 A.A, h' := _}, naturality' := _}, inv := {app := λ (A : category_theory.endofunctor.algebra F), {f := 𝟙 A.A, h' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.endofunctor.adjunction.alg_coalg_equiv.counit_iso
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(adj : F ⊣ G) :
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
- category_theory.endofunctor.adjunction.alg_coalg_equiv.counit_iso adj = {hom := {app := λ (V : category_theory.endofunctor.coalgebra G), {f := 𝟙 V.V, h' := _}, naturality' := _}, inv := {app := λ (V : category_theory.endofunctor.coalgebra G), {f := 𝟙 V.V, h' := _}, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.endofunctor.adjunction.algebra_coalgebra_equiv
{C : Type u}
[category_theory.category C]
{F G : C ⥤ C}
(adj : F ⊣ G) :
If F is left adjoint to G, then the category of algebras over F is equivalent to the
category of coalgebras over G.
Equations
- category_theory.endofunctor.adjunction.algebra_coalgebra_equiv adj = {functor := category_theory.endofunctor.adjunction.algebra.to_coalgebra_of adj, inverse := category_theory.endofunctor.adjunction.coalgebra.to_algebra_of adj, unit_iso := category_theory.endofunctor.adjunction.alg_coalg_equiv.unit_iso adj, counit_iso := category_theory.endofunctor.adjunction.alg_coalg_equiv.counit_iso adj, functor_unit_iso_comp' := _}