Algebras of endofunctors #
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
CategoryTheory.Endofunctor.Algebra
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
:
Type (max u v)
- a : C
carrier of the algebra
- str : F.obj s.a ⟶ s.a
structure morphism of the algebra
An algebra of an endofunctor; str stands for "structure morphism"
Instances For
theorem
CategoryTheory.Endofunctor.Algebra.Hom.ext_iff
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
{A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (x y : CategoryTheory.Endofunctor.Algebra.Hom A₀ A₁), x = y ↔ x.f = y.f
theorem
CategoryTheory.Endofunctor.Algebra.Hom.ext
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
{A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} (x y : CategoryTheory.Endofunctor.Algebra.Hom A₀ A₁), x.f = y.f → x = y
structure
CategoryTheory.Endofunctor.Algebra.Hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(A₀ : CategoryTheory.Endofunctor.Algebra F)
(A₁ : CategoryTheory.Endofunctor.Algebra F)
:
Type v
- f : A₀.a ⟶ A₁.a
underlying morphism between the carriers
- h : CategoryTheory.CategoryStruct.comp (F.map s.f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str s.f
compatibility condition
A morphism between algebras of endofunctor F
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.Hom.h_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A₀ : CategoryTheory.Endofunctor.Algebra F}
{A₁ : CategoryTheory.Endofunctor.Algebra F}
(self : CategoryTheory.Endofunctor.Algebra.Hom A₀ A₁)
{Z : C}
(h : A₁.a ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (F.map self.f) (CategoryTheory.CategoryStruct.comp A₁.str h) = CategoryTheory.CategoryStruct.comp A₀.str (CategoryTheory.CategoryStruct.comp self.f h)
def
CategoryTheory.Endofunctor.Algebra.Hom.id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(A : CategoryTheory.Endofunctor.Algebra F)
:
The identity morphism of an algebra of endofunctor F
Instances For
instance
CategoryTheory.Endofunctor.Algebra.Hom.instInhabitedHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(A : CategoryTheory.Endofunctor.Algebra F)
:
def
CategoryTheory.Endofunctor.Algebra.Hom.comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A₀ : CategoryTheory.Endofunctor.Algebra F}
{A₁ : CategoryTheory.Endofunctor.Algebra F}
{A₂ : CategoryTheory.Endofunctor.Algebra F}
(f : CategoryTheory.Endofunctor.Algebra.Hom A₀ A₁)
(g : CategoryTheory.Endofunctor.Algebra.Hom A₁ A₂)
:
The composition of morphisms between algebras of endofunctor F
Instances For
theorem
CategoryTheory.Endofunctor.Algebra.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A : CategoryTheory.Endofunctor.Algebra F}
{B : CategoryTheory.Endofunctor.Algebra F}
{f : A ⟶ B}
{g : A ⟶ B}
(w : autoParam (f.f = g.f) _auto✝)
:
f = g
@[simp]
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.id_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(A : CategoryTheory.Endofunctor.Algebra F)
:
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.comp_eq_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A₀ : CategoryTheory.Endofunctor.Algebra F}
{A₁ : CategoryTheory.Endofunctor.Algebra F}
{A₂ : CategoryTheory.Endofunctor.Algebra F}
(f : A₀ ⟶ A₁)
(g : A₁ ⟶ A₂)
:
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.comp_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A₀ : CategoryTheory.Endofunctor.Algebra F}
{A₁ : CategoryTheory.Endofunctor.Algebra F}
{A₂ : CategoryTheory.Endofunctor.Algebra F}
(f : A₀ ⟶ A₁)
(g : A₁ ⟶ A₂)
:
(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
instance
CategoryTheory.Endofunctor.Algebra.instCategoryAlgebra
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
:
Algebras of an endofunctor F form a category
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.isoMk_inv_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A₀ : CategoryTheory.Endofunctor.Algebra F}
{A₁ : CategoryTheory.Endofunctor.Algebra F}
(h : A₀.a ≅ A₁.a)
(w : autoParam (CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str h.hom)
_auto✝)
:
(CategoryTheory.Endofunctor.Algebra.isoMk h).inv.f = h.inv
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.isoMk_hom_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A₀ : CategoryTheory.Endofunctor.Algebra F}
{A₁ : CategoryTheory.Endofunctor.Algebra F}
(h : A₀.a ≅ A₁.a)
(w : autoParam (CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str h.hom)
_auto✝)
:
(CategoryTheory.Endofunctor.Algebra.isoMk h).hom.f = h.hom
def
CategoryTheory.Endofunctor.Algebra.isoMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A₀ : CategoryTheory.Endofunctor.Algebra F}
{A₁ : CategoryTheory.Endofunctor.Algebra F}
(h : A₀.a ≅ A₁.a)
(w : autoParam (CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str h.hom)
_auto✝)
:
A₀ ≅ A₁
To construct an isomorphism of algebras, it suffices to give an isomorphism of the As which commutes with the structure morphisms.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.forget_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
:
∀ {X Y : CategoryTheory.Endofunctor.Algebra F} (self : CategoryTheory.Endofunctor.Algebra.Hom X Y),
(CategoryTheory.Endofunctor.Algebra.forget F).map self = self.f
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.forget_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
(A : CategoryTheory.Endofunctor.Algebra F)
:
(CategoryTheory.Endofunctor.Algebra.forget F).obj A = A.a
def
CategoryTheory.Endofunctor.Algebra.forget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
:
The forgetful functor from the category of algebras, forgetting the algebraic structure.
Instances For
theorem
CategoryTheory.Endofunctor.Algebra.iso_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A₀ : CategoryTheory.Endofunctor.Algebra F}
{A₁ : CategoryTheory.Endofunctor.Algebra F}
(f : A₀ ⟶ A₁)
[CategoryTheory.IsIso f.f]
:
An algebra morphism with an underlying isomorphism hom in C is an algebra isomorphism.
theorem
CategoryTheory.Endofunctor.Algebra.epi_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{X : CategoryTheory.Endofunctor.Algebra F}
{Y : CategoryTheory.Endofunctor.Algebra F}
(f : X ⟶ Y)
[h : CategoryTheory.Epi f.f]
:
An algebra morphism with an underlying epimorphism hom in C is an algebra epimorphism.
theorem
CategoryTheory.Endofunctor.Algebra.mono_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{X : CategoryTheory.Endofunctor.Algebra F}
{Y : CategoryTheory.Endofunctor.Algebra F}
(f : X ⟶ Y)
[h : CategoryTheory.Mono f.f]
:
An algebra morphism with an underlying monomorphism hom in C is an algebra monomorphism.
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_obj_str
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : G ⟶ F)
(A : CategoryTheory.Endofunctor.Algebra F)
:
((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).obj A).str = CategoryTheory.CategoryStruct.comp (α.app A.a) A.str
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_map_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : G ⟶ F)
:
∀ {X Y : CategoryTheory.Endofunctor.Algebra F} (f : X ⟶ Y),
((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).map f).f = f.f
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_obj_a
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : G ⟶ F)
(A : CategoryTheory.Endofunctor.Algebra F)
:
((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).obj A).a = A.a
def
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : G ⟶ F)
:
From a natural transformation α : G → F we get a functor from
algebras of F to algebras of G.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTransId_hom_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(X : CategoryTheory.Endofunctor.Algebra F)
:
(CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.hom.app X).f = CategoryTheory.CategoryStruct.id X.a
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTransId_inv_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(X : CategoryTheory.Endofunctor.Algebra F)
:
(CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.inv.app X).f = CategoryTheory.CategoryStruct.id X.a
def
CategoryTheory.Endofunctor.Algebra.functorOfNatTransId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
:
The identity transformation induces the identity endofunctor on the category of algebras.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp_hom_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₀ : CategoryTheory.Functor C C}
{F₁ : CategoryTheory.Functor C C}
{F₂ : CategoryTheory.Functor C C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂)
(X : CategoryTheory.Endofunctor.Algebra F₂)
:
((CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α β).hom.app X).f = CategoryTheory.CategoryStruct.id X.a
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp_inv_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₀ : CategoryTheory.Functor C C}
{F₁ : CategoryTheory.Functor C C}
{F₂ : CategoryTheory.Functor C C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂)
(X : CategoryTheory.Endofunctor.Algebra F₂)
:
((CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α β).inv.app X).f = CategoryTheory.CategoryStruct.id X.a
def
CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₀ : CategoryTheory.Functor C C}
{F₁ : CategoryTheory.Functor C C}
{F₂ : CategoryTheory.Functor C C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂)
:
A composition of natural transformations gives the composition of corresponding functors.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq_hom_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
{α : F ⟶ G}
{β : F ⟶ G}
(h : α = β)
(X : CategoryTheory.Endofunctor.Algebra G)
:
((CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h).hom.app X).f = CategoryTheory.CategoryStruct.id X.a
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq_inv_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
{α : F ⟶ G}
{β : F ⟶ G}
(h : α = β)
(X : CategoryTheory.Endofunctor.Algebra G)
:
((CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq h).inv.app X).f = CategoryTheory.CategoryStruct.id X.a
def
CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
{α : F ⟶ G}
{β : 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.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.equivOfNatIso_inverse
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ≅ G)
:
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.equivOfNatIso_counitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ≅ G)
:
(CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).counitIso = (CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α.inv α.hom).symm ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq
(_ : CategoryTheory.CategoryStruct.comp α.inv α.hom = CategoryTheory.CategoryStruct.id G) ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransId
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.equivOfNatIso_unitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ≅ G)
:
(CategoryTheory.Endofunctor.Algebra.equivOfNatIso α).unitIso = CategoryTheory.Endofunctor.Algebra.functorOfNatTransId.symm ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq
(_ : CategoryTheory.CategoryStruct.id F = CategoryTheory.CategoryStruct.comp α.hom α.inv) ≪≫ CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α.hom α.inv
@[simp]
theorem
CategoryTheory.Endofunctor.Algebra.equivOfNatIso_functor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ≅ G)
:
def
CategoryTheory.Endofunctor.Algebra.equivOfNatIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor 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.
Instances For
def
CategoryTheory.Endofunctor.Algebra.Initial.strInv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A : CategoryTheory.Endofunctor.Algebra F}
(h : CategoryTheory.Limits.IsInitial A)
:
A.a ⟶ F.obj A.a
The inverse of the structure map of an initial algebra
Instances For
theorem
CategoryTheory.Endofunctor.Algebra.Initial.left_inv'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A : CategoryTheory.Endofunctor.Algebra F}
(h : CategoryTheory.Limits.IsInitial A)
:
theorem
CategoryTheory.Endofunctor.Algebra.Initial.left_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A : CategoryTheory.Endofunctor.Algebra F}
(h : CategoryTheory.Limits.IsInitial A)
:
theorem
CategoryTheory.Endofunctor.Algebra.Initial.right_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A : CategoryTheory.Endofunctor.Algebra F}
(h : CategoryTheory.Limits.IsInitial A)
:
theorem
CategoryTheory.Endofunctor.Algebra.Initial.str_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A : CategoryTheory.Endofunctor.Algebra F}
(h : CategoryTheory.Limits.IsInitial A)
:
CategoryTheory.IsIso A.str
The structure map of the initial algebra is an isomorphism, hence endofunctors preserve their initial algebras
structure
CategoryTheory.Endofunctor.Coalgebra
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
:
Type (max u v)
- V : C
carrier of the coalgebra
- str : s.V ⟶ F.obj s.V
structure morphism of the coalgebra
A coalgebra of an endofunctor; str stands for "structure morphism"
Instances For
theorem
CategoryTheory.Endofunctor.Coalgebra.Hom.ext
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
{V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (x y : CategoryTheory.Endofunctor.Coalgebra.Hom V₀ V₁),
x.f = y.f → x = y
theorem
CategoryTheory.Endofunctor.Coalgebra.Hom.ext_iff
{C : Type u}
:
∀ {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C}
{V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} (x y : CategoryTheory.Endofunctor.Coalgebra.Hom V₀ V₁),
x = y ↔ x.f = y.f
structure
CategoryTheory.Endofunctor.Coalgebra.Hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(V₀ : CategoryTheory.Endofunctor.Coalgebra F)
(V₁ : CategoryTheory.Endofunctor.Coalgebra F)
:
Type v
- f : V₀.V ⟶ V₁.V
underlying morphism between two carriers
- h : CategoryTheory.CategoryStruct.comp V₀.str (F.map s.f) = CategoryTheory.CategoryStruct.comp s.f V₁.str
compatibility condition
A morphism between coalgebras of an endofunctor F
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.Hom.h_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{V₀ : CategoryTheory.Endofunctor.Coalgebra F}
{V₁ : CategoryTheory.Endofunctor.Coalgebra F}
(self : CategoryTheory.Endofunctor.Coalgebra.Hom V₀ V₁)
{Z : C}
(h : F.obj V₁.V ⟶ Z)
:
CategoryTheory.CategoryStruct.comp V₀.str (CategoryTheory.CategoryStruct.comp (F.map self.f) h) = CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp V₁.str h)
def
CategoryTheory.Endofunctor.Coalgebra.Hom.id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(V : CategoryTheory.Endofunctor.Coalgebra F)
:
The identity morphism of an algebra of endofunctor F
Instances For
instance
CategoryTheory.Endofunctor.Coalgebra.Hom.instInhabitedHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(V : CategoryTheory.Endofunctor.Coalgebra F)
:
def
CategoryTheory.Endofunctor.Coalgebra.Hom.comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{V₀ : CategoryTheory.Endofunctor.Coalgebra F}
{V₁ : CategoryTheory.Endofunctor.Coalgebra F}
{V₂ : CategoryTheory.Endofunctor.Coalgebra F}
(f : CategoryTheory.Endofunctor.Coalgebra.Hom V₀ V₁)
(g : CategoryTheory.Endofunctor.Coalgebra.Hom V₁ V₂)
:
The composition of morphisms between algebras of endofunctor F
Instances For
theorem
CategoryTheory.Endofunctor.Coalgebra.ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{A : CategoryTheory.Endofunctor.Coalgebra F}
{B : CategoryTheory.Endofunctor.Coalgebra F}
{f : A ⟶ B}
{g : A ⟶ B}
(w : autoParam (f.f = g.f) _auto✝)
:
f = g
@[simp]
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.id_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(V : CategoryTheory.Endofunctor.Coalgebra F)
:
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.comp_eq_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{V₀ : CategoryTheory.Endofunctor.Coalgebra F}
{V₁ : CategoryTheory.Endofunctor.Coalgebra F}
{V₂ : CategoryTheory.Endofunctor.Coalgebra F}
(f : V₀ ⟶ V₁)
(g : V₁ ⟶ V₂)
:
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.comp_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{V₀ : CategoryTheory.Endofunctor.Coalgebra F}
{V₁ : CategoryTheory.Endofunctor.Coalgebra F}
{V₂ : CategoryTheory.Endofunctor.Coalgebra F}
(f : V₀ ⟶ V₁)
(g : V₁ ⟶ V₂)
:
(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
instance
CategoryTheory.Endofunctor.Coalgebra.instCategoryCoalgebra
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
:
Coalgebras of an endofunctor F form a category
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.isoMk_inv_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{V₀ : CategoryTheory.Endofunctor.Coalgebra F}
{V₁ : CategoryTheory.Endofunctor.Coalgebra F}
(h : V₀.V ≅ V₁.V)
(w : autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom V₁.str)
_auto✝)
:
(CategoryTheory.Endofunctor.Coalgebra.isoMk h).inv.f = h.inv
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.isoMk_hom_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{V₀ : CategoryTheory.Endofunctor.Coalgebra F}
{V₁ : CategoryTheory.Endofunctor.Coalgebra F}
(h : V₀.V ≅ V₁.V)
(w : autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom V₁.str)
_auto✝)
:
(CategoryTheory.Endofunctor.Coalgebra.isoMk h).hom.f = h.hom
def
CategoryTheory.Endofunctor.Coalgebra.isoMk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{V₀ : CategoryTheory.Endofunctor.Coalgebra F}
{V₁ : CategoryTheory.Endofunctor.Coalgebra F}
(h : V₀.V ≅ V₁.V)
(w : autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom V₁.str)
_auto✝)
:
V₀ ≅ V₁
To construct an isomorphism of coalgebras, it suffices to give an isomorphism of the Vs which commutes with the structure morphisms.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.forget_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
:
∀ {X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y),
(CategoryTheory.Endofunctor.Coalgebra.forget F).map f = f.f
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.forget_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
(A : CategoryTheory.Endofunctor.Coalgebra F)
:
(CategoryTheory.Endofunctor.Coalgebra.forget F).obj A = A.V
def
CategoryTheory.Endofunctor.Coalgebra.forget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(F : CategoryTheory.Functor C C)
:
The forgetful functor from the category of coalgebras, forgetting the coalgebraic structure.
Instances For
theorem
CategoryTheory.Endofunctor.Coalgebra.iso_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{V₀ : CategoryTheory.Endofunctor.Coalgebra F}
{V₁ : CategoryTheory.Endofunctor.Coalgebra F}
(f : V₀ ⟶ V₁)
[CategoryTheory.IsIso f.f]
:
A coalgebra morphism with an underlying isomorphism hom in C is a coalgebra isomorphism.
theorem
CategoryTheory.Endofunctor.Coalgebra.epi_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{X : CategoryTheory.Endofunctor.Coalgebra F}
{Y : CategoryTheory.Endofunctor.Coalgebra F}
(f : X ⟶ Y)
[h : CategoryTheory.Epi f.f]
:
An algebra morphism with an underlying epimorphism hom in C is an algebra epimorphism.
theorem
CategoryTheory.Endofunctor.Coalgebra.mono_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{X : CategoryTheory.Endofunctor.Coalgebra F}
{Y : CategoryTheory.Endofunctor.Coalgebra F}
(f : X ⟶ Y)
[h : CategoryTheory.Mono f.f]
:
An algebra morphism with an underlying monomorphism hom in C is an algebra monomorphism.
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_map_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ⟶ G)
:
∀ {X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y),
((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).map f).f = f.f
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_obj_V
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ⟶ G)
(V : CategoryTheory.Endofunctor.Coalgebra F)
:
((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).obj V).V = V.V
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_obj_str
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ⟶ G)
(V : CategoryTheory.Endofunctor.Coalgebra F)
:
((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α).obj V).str = CategoryTheory.CategoryStruct.comp V.str (α.app V.V)
def
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ⟶ G)
:
From a natural transformation α : F → G we get a functor from
coalgebras of F to coalgebras of G.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId_inv_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(X : CategoryTheory.Endofunctor.Coalgebra F)
:
(CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.inv.app X).f = CategoryTheory.CategoryStruct.id X.V
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId_hom_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
(X : CategoryTheory.Endofunctor.Coalgebra F)
:
(CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.hom.app X).f = CategoryTheory.CategoryStruct.id X.V
def
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
:
The identity transformation induces the identity endofunctor on the category of coalgebras.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp_hom_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₀ : CategoryTheory.Functor C C}
{F₁ : CategoryTheory.Functor C C}
{F₂ : CategoryTheory.Functor C C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂)
(X : CategoryTheory.Endofunctor.Coalgebra F₀)
:
((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α β).hom.app X).f = CategoryTheory.CategoryStruct.id X.V
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp_inv_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₀ : CategoryTheory.Functor C C}
{F₁ : CategoryTheory.Functor C C}
{F₂ : CategoryTheory.Functor C C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂)
(X : CategoryTheory.Endofunctor.Coalgebra F₀)
:
((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α β).inv.app X).f = CategoryTheory.CategoryStruct.id X.V
def
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F₀ : CategoryTheory.Functor C C}
{F₁ : CategoryTheory.Functor C C}
{F₂ : CategoryTheory.Functor C C}
(α : F₀ ⟶ F₁)
(β : F₁ ⟶ F₂)
:
A composition of natural transformations gives the composition of corresponding functors.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq_hom_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
{α : F ⟶ G}
{β : F ⟶ G}
(h : α = β)
(X : CategoryTheory.Endofunctor.Coalgebra F)
:
((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq h).hom.app X).f = CategoryTheory.CategoryStruct.id X.V
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq_inv_app_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
{α : F ⟶ G}
{β : F ⟶ G}
(h : α = β)
(X : CategoryTheory.Endofunctor.Coalgebra F)
:
((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq h).inv.app X).f = CategoryTheory.CategoryStruct.id X.V
def
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
{α : F ⟶ G}
{β : 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.
Instances For
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_unitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ≅ G)
:
(CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).unitIso = CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId.symm ≪≫ CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq
(_ : CategoryTheory.CategoryStruct.id F = CategoryTheory.CategoryStruct.comp α.hom α.inv) ≪≫ CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α.hom α.inv
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_inverse
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ≅ G)
:
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_functor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ≅ G)
:
@[simp]
theorem
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_counitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(α : F ≅ G)
:
(CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).counitIso = (CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp α.inv α.hom).symm ≪≫ CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq
(_ : CategoryTheory.CategoryStruct.comp α.inv α.hom = CategoryTheory.CategoryStruct.id G) ≪≫ CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId
def
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor 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.
Instances For
theorem
CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(adj : F ⊣ G)
(A₁ : CategoryTheory.Endofunctor.Algebra F)
(A₂ : CategoryTheory.Endofunctor.Algebra F)
(f : A₁ ⟶ A₂)
:
CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Adjunction.homEquiv adj A₁.a A₁.a) A₁.str) (G.map f.f) = CategoryTheory.CategoryStruct.comp f.f (↑(CategoryTheory.Adjunction.homEquiv adj A₂.a A₂.a) A₂.str)
theorem
CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor C C}
(adj : F ⊣ G)
(V₁ : CategoryTheory.Endofunctor.Coalgebra G)
(V₂ : CategoryTheory.Endofunctor.Coalgebra G)
(f : V₁ ⟶ V₂)
:
CategoryTheory.CategoryStruct.comp (F.map f.f) (↑(CategoryTheory.Adjunction.homEquiv adj V₂.V V₂.V).symm V₂.str) = CategoryTheory.CategoryStruct.comp (↑(CategoryTheory.Adjunction.homEquiv adj V₁.V V₁.V).symm V₁.str) f.f
def
CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor 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.
Instances For
def
CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor 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.
Instances For
def
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor 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.
Instances For
def
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor 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.
Instances For
def
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor C C}
{G : CategoryTheory.Functor 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.