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 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} [Category.{v, u} C] (F : Functor C C) : Type (max u v)

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

• a : C

  carrier of the algebra

• str : F.obj self.a ⟶ self.a

  structure morphism of the algebra

instance CategoryTheory.Endofunctor.instInhabitedAlgebraId {C : Type u} [Category.{v, u} C] [Inhabited C] : Inhabited (Algebra (Functor.id C))

structure CategoryTheory.Endofunctor.Algebra.Hom {C : Type u} [Category.{v, u} C] {F : Functor C C} (A₀ A₁ : Algebra F) : Type v

A morphism between algebras of endofunctor F

• f : A₀.a ⟶ A₁.a

  underlying morphism between the carriers

• h : CategoryStruct.comp (F.map self.f) A₁.str = CategoryStruct.comp A₀.str self.f

  compatibility condition

theorem CategoryTheory.Endofunctor.Algebra.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {F : Functor C C} {A₀ A₁ : Algebra F} {x y : A₀.Hom A₁} (f : x.f = y.f) : x = y

theorem CategoryTheory.Endofunctor.Algebra.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {F : Functor C C} {A₀ A₁ : Algebra F} {x y : A₀.Hom A₁} : x = y ↔ x.f = y.f

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.Hom.h_assoc {C : Type u} [Category.{v, u} C] {F : Functor C C} {A₀ A₁ : Algebra F} (self : A₀.Hom A₁) {Z : C} (h : A₁.a ⟶ Z) : CategoryStruct.comp (F.map self.f) (CategoryStruct.comp A₁.str h) = CategoryStruct.comp A₀.str (CategoryStruct.comp self.f h)

def CategoryTheory.Endofunctor.Algebra.Hom.id {C : Type u} [Category.{v, u} C] {F : Functor C C} (A : Algebra F) : A.Hom A

The identity morphism of an algebra of endofunctor F

instance CategoryTheory.Endofunctor.Algebra.Hom.instInhabited {C : Type u} [Category.{v, u} C] {F : Functor C C} (A : Algebra F) : Inhabited (A.Hom A)

def CategoryTheory.Endofunctor.Algebra.Hom.comp {C : Type u} [Category.{v, u} C] {F : Functor C C} {A₀ A₁ A₂ : Algebra F} (f : A₀.Hom A₁) (g : A₁.Hom A₂) : A₀.Hom A₂

The composition of morphisms between algebras of endofunctor F

instance CategoryTheory.Endofunctor.Algebra.instCategoryStruct {C : Type u} [Category.{v, u} C] (F : Functor C C) : CategoryStruct.{v, max u v} (Algebra F)

theorem CategoryTheory.Endofunctor.Algebra.ext {C : Type u} [Category.{v, u} C] {F : Functor C C} {A B : Algebra F} {f g : A ⟶ B} (w : f.f = g.f := by cat_disch) : f = g

theorem CategoryTheory.Endofunctor.Algebra.ext_iff {C : Type u} [Category.{v, u} C] {F : Functor C C} {A B : Algebra F} {f g : A ⟶ B} : f = g ↔ autoParam (f.f = g.f) _auto✝

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.id_eq_id {C : Type u} [Category.{v, u} C] {F : Functor C C} (A : Algebra F) : Hom.id A = CategoryStruct.id A

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.id_f {C : Type u} [Category.{v, u} C] {F : Functor C C} (A : Algebra F) : (CategoryStruct.id A).f = CategoryStruct.id A.a

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.comp_eq_comp {C : Type u} [Category.{v, u} C] {F : Functor C C} {A₀ A₁ A₂ : Algebra F} (f : A₀ ⟶ A₁) (g : A₁ ⟶ A₂) : Hom.comp f g = CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.comp_f {C : Type u} [Category.{v, u} C] {F : Functor C C} {A₀ A₁ A₂ : Algebra F} (f : A₀ ⟶ A₁) (g : A₁ ⟶ A₂) : (CategoryStruct.comp f g).f = CategoryStruct.comp f.f g.f

instance CategoryTheory.Endofunctor.Algebra.instCategory {C : Type u} [Category.{v, u} C] (F : Functor C C) : Category.{v, max u v} (Algebra F)

Algebras of an endofunctor F form a category

def CategoryTheory.Endofunctor.Algebra.isoMk {C : Type u} [Category.{v, u} C] {F : Functor C C} {A₀ A₁ : Algebra F} (h : A₀.a ≅ A₁.a) (w : CategoryStruct.comp (F.map h.hom) A₁.str = CategoryStruct.comp A₀.str h.hom := by cat_disch) : A₀ ≅ A₁

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

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.isoMk_hom_f {C : Type u} [Category.{v, u} C] {F : Functor C C} {A₀ A₁ : Algebra F} (h : A₀.a ≅ A₁.a) (w : CategoryStruct.comp (F.map h.hom) A₁.str = CategoryStruct.comp A₀.str h.hom := by cat_disch) : (isoMk h w).hom.f = h.hom

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.isoMk_inv_f {C : Type u} [Category.{v, u} C] {F : Functor C C} {A₀ A₁ : Algebra F} (h : A₀.a ≅ A₁.a) (w : CategoryStruct.comp (F.map h.hom) A₁.str = CategoryStruct.comp A₀.str h.hom := by cat_disch) : (isoMk h w).inv.f = h.inv

def CategoryTheory.Endofunctor.Algebra.forget {C : Type u} [Category.{v, u} C] (F : Functor C C) : Functor (Algebra F) C

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

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.forget_map {C : Type u} [Category.{v, u} C] (F : Functor C C) {X✝ Y✝ : Algebra F} (self : X✝.Hom Y✝) : (forget F).map self = self.f

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.forget_obj {C : Type u} [Category.{v, u} C] (F : Functor C C) (A : Algebra F) : (forget F).obj A = A.a

theorem CategoryTheory.Endofunctor.Algebra.iso_of_iso {C : Type u} [Category.{v, u} C] {F : Functor C C} {A₀ A₁ : Algebra F} (f : A₀ ⟶ A₁) [IsIso f.f] : IsIso f

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

instance CategoryTheory.Endofunctor.Algebra.forget_reflects_iso {C : Type u} [Category.{v, u} C] {F : Functor C C} : (forget F).ReflectsIsomorphisms

instance CategoryTheory.Endofunctor.Algebra.forget_faithful {C : Type u} [Category.{v, u} C] {F : Functor C C} : (forget F).Faithful

theorem CategoryTheory.Endofunctor.Algebra.epi_of_epi {C : Type u} [Category.{v, u} C] {F : Functor C C} {X Y : Algebra F} (f : X ⟶ Y) [h : Epi f.f] : Epi 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} [Category.{v, u} C] {F : Functor C C} {X Y : Algebra F} (f : X ⟶ Y) [h : Mono f.f] : Mono f

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

def CategoryTheory.Endofunctor.Algebra.functorOfNatTrans {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : G ⟶ F) : Functor (Algebra F) (Algebra G)

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

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_obj_a {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : G ⟶ F) (A : Algebra F) : ((functorOfNatTrans α).obj A).a = A.a

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_obj_str {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : G ⟶ F) (A : Algebra F) : ((functorOfNatTrans α).obj A).str = CategoryStruct.comp (α.app A.a) A.str

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_map_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : G ⟶ F) {X✝ Y✝ : Algebra F} (f : X✝ ⟶ Y✝) : ((functorOfNatTrans α).map f).f = f.f

def CategoryTheory.Endofunctor.Algebra.functorOfNatTransId {C : Type u} [Category.{v, u} C] {F : Functor C C} : functorOfNatTrans (CategoryStruct.id F) ≅ Functor.id (Algebra F)

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

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTransId_hom_app_f {C : Type u} [Category.{v, u} C] {F : Functor C C} (X : Algebra F) : (functorOfNatTransId.hom.app X).f = CategoryStruct.id X.a

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTransId_inv_app_f {C : Type u} [Category.{v, u} C] {F : Functor C C} (X : Algebra F) : (functorOfNatTransId.inv.app X).f = CategoryStruct.id X.a

def CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp {C : Type u} [Category.{v, u} C] {F₀ F₁ F₂ : Functor C C} (α : F₀ ⟶ F₁) (β : F₁ ⟶ F₂) : functorOfNatTrans (CategoryStruct.comp α β) ≅ (functorOfNatTrans β).comp (functorOfNatTrans α)

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

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp_hom_app_f {C : Type u} [Category.{v, u} C] {F₀ F₁ F₂ : Functor C C} (α : F₀ ⟶ F₁) (β : F₁ ⟶ F₂) (X : Algebra F₂) : ((functorOfNatTransComp α β).hom.app X).f = CategoryStruct.id X.a

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp_inv_app_f {C : Type u} [Category.{v, u} C] {F₀ F₁ F₂ : Functor C C} (α : F₀ ⟶ F₁) (β : F₁ ⟶ F₂) (X : Algebra F₂) : ((functorOfNatTransComp α β).inv.app X).f = CategoryStruct.id X.a

def CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq {C : Type u} [Category.{v, u} C] {F G : Functor C C} {α β : F ⟶ G} (h : α = β) : functorOfNatTrans α ≅ functorOfNatTrans β

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.

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq_inv_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} {α β : F ⟶ G} (h : α = β) (X : Algebra G) : ((functorOfNatTransEq h).inv.app X).f = CategoryStruct.id X.a

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq_hom_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} {α β : F ⟶ G} (h : α = β) (X : Algebra G) : ((functorOfNatTransEq h).hom.app X).f = CategoryStruct.id X.a

def CategoryTheory.Endofunctor.Algebra.equivOfNatIso {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : Algebra F ≌ Algebra 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.

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.equivOfNatIso_functor {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : (equivOfNatIso α).functor = functorOfNatTrans α.inv

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.equivOfNatIso_counitIso {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : (equivOfNatIso α).counitIso = (functorOfNatTransComp α.inv α.hom).symm ≪≫ functorOfNatTransEq ⋯ ≪≫ functorOfNatTransId

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.equivOfNatIso_unitIso {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : (equivOfNatIso α).unitIso = functorOfNatTransId.symm ≪≫ functorOfNatTransEq ⋯ ≪≫ functorOfNatTransComp α.hom α.inv

@[simp]

theorem CategoryTheory.Endofunctor.Algebra.equivOfNatIso_inverse {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : (equivOfNatIso α).inverse = functorOfNatTrans α.hom

def CategoryTheory.Endofunctor.Algebra.Initial.strInv {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Algebra F} (h : Limits.IsInitial A) : A.a ⟶ F.obj A.a

The inverse of the structure map of an initial algebra

theorem CategoryTheory.Endofunctor.Algebra.Initial.left_inv' {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Algebra F} (h : Limits.IsInitial A) : { f := CategoryStruct.comp (strInv h) A.str, h := ⋯ } = CategoryStruct.id A

theorem CategoryTheory.Endofunctor.Algebra.Initial.left_inv {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Algebra F} (h : Limits.IsInitial A) : CategoryStruct.comp (strInv h) A.str = CategoryStruct.id A.a

theorem CategoryTheory.Endofunctor.Algebra.Initial.right_inv {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Algebra F} (h : Limits.IsInitial A) : CategoryStruct.comp A.str (strInv h) = CategoryStruct.id (F.obj A.a)

theorem CategoryTheory.Endofunctor.Algebra.Initial.str_isIso {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Algebra F} (h : Limits.IsInitial A) : 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} [Category.{v, u} C] (F : Functor C C) : Type (max u v)

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

• V : C

  carrier of the coalgebra

• str : self.V ⟶ F.obj self.V

  structure morphism of the coalgebra

instance CategoryTheory.Endofunctor.instInhabitedCoalgebraId {C : Type u} [Category.{v, u} C] [Inhabited C] : Inhabited (Coalgebra (Functor.id C))

structure CategoryTheory.Endofunctor.Coalgebra.Hom {C : Type u} [Category.{v, u} C] {F : Functor C C} (V₀ V₁ : Coalgebra F) : Type v

A morphism between coalgebras of an endofunctor F

• f : V₀.V ⟶ V₁.V

  underlying morphism between two carriers

• h : CategoryStruct.comp V₀.str (F.map self.f) = CategoryStruct.comp self.f V₁.str

  compatibility condition

theorem CategoryTheory.Endofunctor.Coalgebra.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {F : Functor C C} {V₀ V₁ : Coalgebra F} {x y : V₀.Hom V₁} (f : x.f = y.f) : x = y

theorem CategoryTheory.Endofunctor.Coalgebra.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {F : Functor C C} {V₀ V₁ : Coalgebra F} {x y : V₀.Hom V₁} : x = y ↔ x.f = y.f

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.Hom.h_assoc {C : Type u} [Category.{v, u} C] {F : Functor C C} {V₀ V₁ : Coalgebra F} (self : V₀.Hom V₁) {Z : C} (h : F.obj V₁.V ⟶ Z) : CategoryStruct.comp V₀.str (CategoryStruct.comp (F.map self.f) h) = CategoryStruct.comp self.f (CategoryStruct.comp V₁.str h)

def CategoryTheory.Endofunctor.Coalgebra.Hom.id {C : Type u} [Category.{v, u} C] {F : Functor C C} (V : Coalgebra F) : V.Hom V

The identity morphism of an algebra of endofunctor F

instance CategoryTheory.Endofunctor.Coalgebra.Hom.instInhabited {C : Type u} [Category.{v, u} C] {F : Functor C C} (V : Coalgebra F) : Inhabited (V.Hom V)

def CategoryTheory.Endofunctor.Coalgebra.Hom.comp {C : Type u} [Category.{v, u} C] {F : Functor C C} {V₀ V₁ V₂ : Coalgebra F} (f : V₀.Hom V₁) (g : V₁.Hom V₂) : V₀.Hom V₂

The composition of morphisms between algebras of endofunctor F

instance CategoryTheory.Endofunctor.Coalgebra.instCategoryStruct {C : Type u} [Category.{v, u} C] (F : Functor C C) : CategoryStruct.{v, max u v} (Coalgebra F)

theorem CategoryTheory.Endofunctor.Coalgebra.ext {C : Type u} [Category.{v, u} C] {F : Functor C C} {A B : Coalgebra F} {f g : A ⟶ B} (w : f.f = g.f := by cat_disch) : f = g

theorem CategoryTheory.Endofunctor.Coalgebra.ext_iff {C : Type u} [Category.{v, u} C] {F : Functor C C} {A B : Coalgebra F} {f g : A ⟶ B} : f = g ↔ autoParam (f.f = g.f) _auto✝

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.id_eq_id {C : Type u} [Category.{v, u} C] {F : Functor C C} (V : Coalgebra F) : Hom.id V = CategoryStruct.id V

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.id_f {C : Type u} [Category.{v, u} C] {F : Functor C C} (V : Coalgebra F) : (CategoryStruct.id V).f = CategoryStruct.id V.V

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.comp_eq_comp {C : Type u} [Category.{v, u} C] {F : Functor C C} {V₀ V₁ V₂ : Coalgebra F} (f : V₀ ⟶ V₁) (g : V₁ ⟶ V₂) : Hom.comp f g = CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.comp_f {C : Type u} [Category.{v, u} C] {F : Functor C C} {V₀ V₁ V₂ : Coalgebra F} (f : V₀ ⟶ V₁) (g : V₁ ⟶ V₂) : (CategoryStruct.comp f g).f = CategoryStruct.comp f.f g.f

instance CategoryTheory.Endofunctor.Coalgebra.instCategory {C : Type u} [Category.{v, u} C] (F : Functor C C) : Category.{v, max u v} (Coalgebra F)

Coalgebras of an endofunctor F form a category

def CategoryTheory.Endofunctor.Coalgebra.isoMk {C : Type u} [Category.{v, u} C] {F : Functor C C} {V₀ V₁ : Coalgebra F} (h : V₀.V ≅ V₁.V) (w : CategoryStruct.comp V₀.str (F.map h.hom) = CategoryStruct.comp h.hom V₁.str := by cat_disch) : V₀ ≅ V₁

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

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.isoMk_inv_f {C : Type u} [Category.{v, u} C] {F : Functor C C} {V₀ V₁ : Coalgebra F} (h : V₀.V ≅ V₁.V) (w : CategoryStruct.comp V₀.str (F.map h.hom) = CategoryStruct.comp h.hom V₁.str := by cat_disch) : (isoMk h w).inv.f = h.inv

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.isoMk_hom_f {C : Type u} [Category.{v, u} C] {F : Functor C C} {V₀ V₁ : Coalgebra F} (h : V₀.V ≅ V₁.V) (w : CategoryStruct.comp V₀.str (F.map h.hom) = CategoryStruct.comp h.hom V₁.str := by cat_disch) : (isoMk h w).hom.f = h.hom

def CategoryTheory.Endofunctor.Coalgebra.forget {C : Type u} [Category.{v, u} C] (F : Functor C C) : Functor (Coalgebra F) C

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

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.forget_obj {C : Type u} [Category.{v, u} C] (F : Functor C C) (A : Coalgebra F) : (forget F).obj A = A.V

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.forget_map {C : Type u} [Category.{v, u} C] (F : Functor C C) {X✝ Y✝ : Coalgebra F} (f : X✝ ⟶ Y✝) : (forget F).map f = f.f

theorem CategoryTheory.Endofunctor.Coalgebra.iso_of_iso {C : Type u} [Category.{v, u} C] {F : Functor C C} {V₀ V₁ : Coalgebra F} (f : V₀ ⟶ V₁) [IsIso f.f] : IsIso f

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

instance CategoryTheory.Endofunctor.Coalgebra.forget_reflects_iso {C : Type u} [Category.{v, u} C] {F : Functor C C} : (forget F).ReflectsIsomorphisms

instance CategoryTheory.Endofunctor.Coalgebra.forget_faithful {C : Type u} [Category.{v, u} C] {F : Functor C C} : (forget F).Faithful

theorem CategoryTheory.Endofunctor.Coalgebra.epi_of_epi {C : Type u} [Category.{v, u} C] {F : Functor C C} {X Y : Coalgebra F} (f : X ⟶ Y) [h : Epi f.f] : Epi 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} [Category.{v, u} C] {F : Functor C C} {X Y : Coalgebra F} (f : X ⟶ Y) [h : Mono f.f] : Mono f

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

def CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ⟶ G) : Functor (Coalgebra F) (Coalgebra G)

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

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_obj_str {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ⟶ G) (V : Coalgebra F) : ((functorOfNatTrans α).obj V).str = CategoryStruct.comp V.str (α.app V.V)

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_map_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ⟶ G) {X✝ Y✝ : Coalgebra F} (f : X✝ ⟶ Y✝) : ((functorOfNatTrans α).map f).f = f.f

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans_obj_V {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ⟶ G) (V : Coalgebra F) : ((functorOfNatTrans α).obj V).V = V.V

def CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId {C : Type u} [Category.{v, u} C] {F : Functor C C} : functorOfNatTrans (CategoryStruct.id F) ≅ Functor.id (Coalgebra F)

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

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId_hom_app_f {C : Type u} [Category.{v, u} C] {F : Functor C C} (X : Coalgebra F) : (functorOfNatTransId.hom.app X).f = CategoryStruct.id X.V

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId_inv_app_f {C : Type u} [Category.{v, u} C] {F : Functor C C} (X : Coalgebra F) : (functorOfNatTransId.inv.app X).f = CategoryStruct.id X.V

def CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp {C : Type u} [Category.{v, u} C] {F₀ F₁ F₂ : Functor C C} (α : F₀ ⟶ F₁) (β : F₁ ⟶ F₂) : functorOfNatTrans (CategoryStruct.comp α β) ≅ (functorOfNatTrans α).comp (functorOfNatTrans β)

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

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp_hom_app_f {C : Type u} [Category.{v, u} C] {F₀ F₁ F₂ : Functor C C} (α : F₀ ⟶ F₁) (β : F₁ ⟶ F₂) (X : Coalgebra F₀) : ((functorOfNatTransComp α β).hom.app X).f = CategoryStruct.id X.V

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp_inv_app_f {C : Type u} [Category.{v, u} C] {F₀ F₁ F₂ : Functor C C} (α : F₀ ⟶ F₁) (β : F₁ ⟶ F₂) (X : Coalgebra F₀) : ((functorOfNatTransComp α β).inv.app X).f = CategoryStruct.id X.V

def CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq {C : Type u} [Category.{v, u} C] {F G : Functor C C} {α β : F ⟶ G} (h : α = β) : functorOfNatTrans α ≅ functorOfNatTrans β

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.

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq_inv_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} {α β : F ⟶ G} (h : α = β) (X : Coalgebra F) : ((functorOfNatTransEq h).inv.app X).f = CategoryStruct.id X.V

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq_hom_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} {α β : F ⟶ G} (h : α = β) (X : Coalgebra F) : ((functorOfNatTransEq h).hom.app X).f = CategoryStruct.id X.V

def CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : Coalgebra F ≌ Coalgebra 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.

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_functor {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : (equivOfNatIso α).functor = functorOfNatTrans α.hom

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_inverse {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : (equivOfNatIso α).inverse = functorOfNatTrans α.inv

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_unitIso {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : (equivOfNatIso α).unitIso = functorOfNatTransId.symm ≪≫ functorOfNatTransEq ⋯ ≪≫ functorOfNatTransComp α.hom α.inv

@[simp]

theorem CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_counitIso {C : Type u} [Category.{v, u} C] {F G : Functor C C} (α : F ≅ G) : (equivOfNatIso α).counitIso = (functorOfNatTransComp α.inv α.hom).symm ≪≫ functorOfNatTransEq ⋯ ≪≫ functorOfNatTransId

def CategoryTheory.Endofunctor.Coalgebra.Terminal.strInv {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Coalgebra F} (h : Limits.IsTerminal A) : F.obj A.V ⟶ A.V

The inverse of the structure map of an terminal coalgebra

theorem CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv' {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Coalgebra F} (h : Limits.IsTerminal A) : { f := CategoryStruct.comp A.str (strInv h), h := ⋯ } = CategoryStruct.id A

theorem CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Coalgebra F} (h : Limits.IsTerminal A) : CategoryStruct.comp A.str (strInv h) = CategoryStruct.id A.V

theorem CategoryTheory.Endofunctor.Coalgebra.Terminal.left_inv {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Coalgebra F} (h : Limits.IsTerminal A) : CategoryStruct.comp (strInv h) A.str = CategoryStruct.id (F.obj A.V)

theorem CategoryTheory.Endofunctor.Coalgebra.Terminal.str_isIso {C : Type u} [Category.{v, u} C] {F : Functor C C} {A : Coalgebra F} (h : Limits.IsTerminal A) : IsIso A.str

The structure map of the terminal coalgebra is an isomorphism, hence endofunctors preserve their terminal coalgebras

theorem CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (A₁ A₂ : Algebra F) (f : A₁ ⟶ A₂) : CategoryStruct.comp ((adj.homEquiv A₁.a A₁.a) A₁.str) (G.map f.f) = CategoryStruct.comp f.f ((adj.homEquiv A₂.a A₂.a) A₂.str)

theorem CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (V₁ V₂ : Coalgebra G) (f : V₁ ⟶ V₂) : CategoryStruct.comp (F.map f.f) ((adj.homEquiv V₂.V V₂.V).symm V₂.str) = CategoryStruct.comp ((adj.homEquiv V₁.V V₁.V).symm V₁.str) f.f

def CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) : Functor (Algebra F) (Coalgebra 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.

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_map_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) {X✝ Y✝ : Algebra F} (f : X✝ ⟶ Y✝) : ((toCoalgebraOf adj).map f).f = f.f

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_V {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (A : Algebra F) : ((toCoalgebraOf adj).obj A).V = A.a

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_str {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (A : Algebra F) : ((toCoalgebraOf adj).obj A).str = (adj.homEquiv A.a A.a) A.str

def CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) : Functor (Coalgebra G) (Algebra F)

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.

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_a {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (V : Coalgebra G) : ((toAlgebraOf adj).obj V).a = V.V

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) {X✝ Y✝ : Coalgebra G} (f : X✝ ⟶ Y✝) : ((toAlgebraOf adj).map f).f = f.f

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_obj_str {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (V : Coalgebra G) : ((toAlgebraOf adj).obj V).str = (adj.homEquiv V.V V.V).symm V.str

def CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) : Functor.id (Algebra F) ≅ (Algebra.toCoalgebraOf adj).comp (Coalgebra.toAlgebraOf adj)

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.

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_hom_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (X : Algebra F) : ((unitIso adj).hom.app X).f = CategoryStruct.id X.a

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso_inv_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (X : Algebra F) : ((unitIso adj).inv.app X).f = CategoryStruct.id X.a

def CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) : (Coalgebra.toAlgebraOf adj).comp (Algebra.toCoalgebraOf adj) ≅ Functor.id (Coalgebra 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.

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_hom_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (X : Coalgebra G) : ((counitIso adj).hom.app X).f = CategoryStruct.id X.V

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_inv_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (X : Coalgebra G) : ((counitIso adj).inv.app X).f = CategoryStruct.id X.V

def CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) : Algebra F ≌ Coalgebra G

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

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (X : Coalgebra G) : ((algebraCoalgebraEquiv adj).counitIso.inv.app X).f = CategoryStruct.id X.V

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_a {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (V : Coalgebra G) : ((algebraCoalgebraEquiv adj).inverse.obj V).a = V.V

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_map_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) {X✝ Y✝ : Coalgebra G} (f : X✝ ⟶ Y✝) : ((algebraCoalgebraEquiv adj).inverse.map f).f = f.f

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_inverse_obj_str {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (V : Coalgebra G) : ((algebraCoalgebraEquiv adj).inverse.obj V).str = (adj.homEquiv V.V V.V).symm V.str

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (X : Coalgebra G) : ((algebraCoalgebraEquiv adj).counitIso.hom.app X).f = CategoryStruct.id X.V

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (X : Algebra F) : ((algebraCoalgebraEquiv adj).unitIso.hom.app X).f = CategoryStruct.id X.a

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_str {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (A : Algebra F) : ((algebraCoalgebraEquiv adj).functor.obj A).str = (adj.homEquiv A.a A.a) A.str

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_map_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) {X✝ Y✝ : Algebra F} (f : X✝ ⟶ Y✝) : ((algebraCoalgebraEquiv adj).functor.map f).f = f.f

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (X : Algebra F) : ((algebraCoalgebraEquiv adj).unitIso.inv.app X).f = CategoryStruct.id X.a

@[simp]

theorem CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_functor_obj_V {C : Type u} [Category.{v, u} C] {F G : Functor C C} (adj : F ⊣ G) (A : Algebra F) : ((algebraCoalgebraEquiv adj).functor.obj A).V = A.a