Eilenberg-Moore (co)algebras for a (co)monad

This file defines Eilenberg-Moore (co)algebras for a (co)monad, and provides the category instance for them.

Further it defines the adjoint pair of free and forgetful functors, respectively from and to the original category, as well as the adjoint pair of forgetful and cofree functors, respectively from and to the original category.

References

• [Riehl, Category theory in context, Section 5.2.4][riehl2017]

structure CategoryTheory.Monad.Algebra {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : Type (max u₁ v₁)

• A : C

  The underlying object associated to an algebra.

• a : T.obj s.A ⟶ s.A

  The structure morphism associated to an algebra.

• unit : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T).app s.A) s.a = CategoryTheory.CategoryStruct.id s.A

  The unit axiom associated to an algebra.

• assoc : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T).app s.A) s.a = CategoryTheory.CategoryStruct.comp (T.map s.a) s.a

  The associativity axiom associated to an algebra.

An Eilenberg-Moore algebra for a monad T. cf Definition 5.2.3 in [Riehl][riehl2017].

theorem CategoryTheory.Monad.Algebra.unit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : CategoryTheory.Monad.Algebra T) {Z : C} (h : self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.η T).app self.A) (CategoryTheory.CategoryStruct.comp self.a h) = h

theorem CategoryTheory.Monad.Algebra.assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : CategoryTheory.Monad.Algebra T) {Z : C} (h : self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Monad.μ T).app self.A) (CategoryTheory.CategoryStruct.comp self.a h) = CategoryTheory.CategoryStruct.comp (T.map self.a) (CategoryTheory.CategoryStruct.comp self.a h)

theorem CategoryTheory.Monad.Algebra.Hom.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : CategoryTheory.Monad.Algebra T} (x y : CategoryTheory.Monad.Algebra.Hom A B), x = y ↔ x.f = y.f

theorem CategoryTheory.Monad.Algebra.Hom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : CategoryTheory.Monad.Algebra T} (x y : CategoryTheory.Monad.Algebra.Hom A B), x.f = y.f → x = y

structure CategoryTheory.Monad.Algebra.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : CategoryTheory.Monad.Algebra T) (B : CategoryTheory.Monad.Algebra T) : Type v₁

• f : A.A ⟶ B.A

  The underlying morphism associated to a morphism of algebras.

• h : CategoryTheory.CategoryStruct.comp (T.map s.f) B.a = CategoryTheory.CategoryStruct.comp A.a s.f

  Compatibility with the structure morphism, for a morphism of algebras.

A morphism of Eilenberg–Moore algebras for the monad T.

@[simp]

theorem CategoryTheory.Monad.Algebra.Hom.h_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : CategoryTheory.Monad.Algebra T} {B : CategoryTheory.Monad.Algebra T} (self : CategoryTheory.Monad.Algebra.Hom A B) {Z : C} (h : B.A ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.map self.f) (CategoryTheory.CategoryStruct.comp B.a h) = CategoryTheory.CategoryStruct.comp A.a (CategoryTheory.CategoryStruct.comp self.f h)

def CategoryTheory.Monad.Algebra.Hom.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : CategoryTheory.Monad.Algebra T) : CategoryTheory.Monad.Algebra.Hom A A

The identity homomorphism for an Eilenberg–Moore algebra.

instance CategoryTheory.Monad.Algebra.Hom.instInhabitedHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : CategoryTheory.Monad.Algebra T) : Inhabited (CategoryTheory.Monad.Algebra.Hom A A)

def CategoryTheory.Monad.Algebra.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {P : CategoryTheory.Monad.Algebra T} {Q : CategoryTheory.Monad.Algebra T} {R : CategoryTheory.Monad.Algebra T} (f : CategoryTheory.Monad.Algebra.Hom P Q) (g : CategoryTheory.Monad.Algebra.Hom Q R) : CategoryTheory.Monad.Algebra.Hom P R

Composition of Eilenberg–Moore algebra homomorphisms.

instance CategoryTheory.Monad.Algebra.instCategoryStructAlgebra {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} : CategoryTheory.CategoryStruct.{v₁, max u₁ v₁} (CategoryTheory.Monad.Algebra T)

theorem CategoryTheory.Monad.Algebra.Hom.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T) (Y : CategoryTheory.Monad.Algebra T) (f : X ⟶ Y) (g : X ⟶ Y) (h : f.f = g.f) : f = g

@[simp]

theorem CategoryTheory.Monad.Algebra.comp_eq_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : CategoryTheory.Monad.Algebra T} {A' : CategoryTheory.Monad.Algebra T} {A'' : CategoryTheory.Monad.Algebra T} (f : A ⟶ A') (g : A' ⟶ A'') : CategoryTheory.Monad.Algebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.Monad.Algebra.id_eq_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : CategoryTheory.Monad.Algebra T) : CategoryTheory.Monad.Algebra.Hom.id A = CategoryTheory.CategoryStruct.id A

@[simp]

theorem CategoryTheory.Monad.Algebra.id_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (A : CategoryTheory.Monad.Algebra T) : (CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.A

@[simp]

theorem CategoryTheory.Monad.Algebra.comp_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : CategoryTheory.Monad.Algebra T} {A' : CategoryTheory.Monad.Algebra T} {A'' : CategoryTheory.Monad.Algebra T} (f : A ⟶ A') (g : A' ⟶ A'') : (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f

instance CategoryTheory.Monad.Algebra.eilenbergMoore {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} : CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Monad.Algebra T)

The category of Eilenberg-Moore algebras for a monad. cf Definition 5.2.4 in [Riehl][riehl2017].

@[simp]

theorem CategoryTheory.Monad.Algebra.isoMk_hom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : CategoryTheory.Monad.Algebra T} {B : CategoryTheory.Monad.Algebra T} (h : A.A ≅ B.A) (w : autoParam (CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom) _auto✝) : (CategoryTheory.Monad.Algebra.isoMk h).hom.f = h.hom

@[simp]

theorem CategoryTheory.Monad.Algebra.isoMk_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : CategoryTheory.Monad.Algebra T} {B : CategoryTheory.Monad.Algebra T} (h : A.A ≅ B.A) (w : autoParam (CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom) _auto✝) : (CategoryTheory.Monad.Algebra.isoMk h).inv.f = h.inv

def CategoryTheory.Monad.Algebra.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : CategoryTheory.Monad.Algebra T} {B : CategoryTheory.Monad.Algebra T} (h : A.A ≅ B.A) (w : autoParam (CategoryTheory.CategoryStruct.comp (T.map h.hom) B.a = CategoryTheory.CategoryStruct.comp A.a h.hom) _auto✝) : A ≅ B

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

@[simp]

theorem CategoryTheory.Monad.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : ∀ {X Y : CategoryTheory.Monad.Algebra T} (f : X ⟶ Y), (CategoryTheory.Monad.forget T).map f = f.f

@[simp]

theorem CategoryTheory.Monad.forget_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (A : CategoryTheory.Monad.Algebra T) : (CategoryTheory.Monad.forget T).obj A = A.A

def CategoryTheory.Monad.forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor (CategoryTheory.Monad.Algebra T) C

The forgetful functor from the Eilenberg-Moore category, forgetting the algebraic structure.

@[simp]

theorem CategoryTheory.Monad.free_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : ∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Monad.free T).map f).f = T.map f

@[simp]

theorem CategoryTheory.Monad.free_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : ((CategoryTheory.Monad.free T).obj X).a = (CategoryTheory.Monad.μ T).app X

@[simp]

theorem CategoryTheory.Monad.free_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C) : ((CategoryTheory.Monad.free T).obj X).A = T.obj X

def CategoryTheory.Monad.free {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Functor C (CategoryTheory.Monad.Algebra T)

The free functor from the Eilenberg-Moore category, constructing an algebra for any object.

instance CategoryTheory.Monad.instInhabitedAlgebra {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) [Inhabited C] : Inhabited (CategoryTheory.Monad.Algebra T)

@[simp]

theorem CategoryTheory.Monad.adj_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : (CategoryTheory.Monad.adj T).unit = CategoryTheory.NatTrans.mk fun X => (CategoryTheory.Monad.η T).app X

@[simp]

theorem CategoryTheory.Monad.adj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : (CategoryTheory.Monad.adj T).counit = CategoryTheory.NatTrans.mk fun Y => CategoryTheory.Monad.Algebra.Hom.mk Y.a

def CategoryTheory.Monad.adj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Monad.free T ⊣ CategoryTheory.Monad.forget T

The adjunction between the free and forgetful constructions for Eilenberg-Moore algebras for a monad. cf Lemma 5.2.8 of [Riehl][riehl2017].

theorem CategoryTheory.Monad.algebra_iso_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {A : CategoryTheory.Monad.Algebra T} {B : CategoryTheory.Monad.Algebra T} (f : A ⟶ B) [CategoryTheory.IsIso f.f] : CategoryTheory.IsIso f

Given an algebra morphism whose carrier part is an isomorphism, we get an algebra isomorphism.

instance CategoryTheory.Monad.forget_reflects_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Monad.forget T)

instance CategoryTheory.Monad.forget_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Faithful (CategoryTheory.Monad.forget T)

theorem CategoryTheory.Monad.algebra_epi_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X : CategoryTheory.Monad.Algebra T} {Y : CategoryTheory.Monad.Algebra T} (f : X ⟶ Y) [h : CategoryTheory.Epi f.f] : CategoryTheory.Epi f

Given an algebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.

theorem CategoryTheory.Monad.algebra_mono_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X : CategoryTheory.Monad.Algebra T} {Y : CategoryTheory.Monad.Algebra T} (f : X ⟶ Y) [h : CategoryTheory.Mono f.f] : CategoryTheory.Mono f

Given an algebra morphism whose carrier part is a monomorphism, we get an algebra monomorphism.

instance CategoryTheory.Monad.instIsRightAdjointAlgebraEilenbergMooreForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.IsRightAdjoint (CategoryTheory.Monad.forget T)

@[simp]

theorem CategoryTheory.Monad.leftAdjoint_forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.leftAdjoint (CategoryTheory.Monad.forget T) = CategoryTheory.Monad.free T

@[simp]

theorem CategoryTheory.Monad.ofRightAdjoint_forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : CategoryTheory.Adjunction.ofRightAdjoint (CategoryTheory.Monad.forget T) = CategoryTheory.Monad.adj T

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHom_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁) : ∀ {X Y : CategoryTheory.Monad.Algebra T₁} (f : X ⟶ Y), ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).map f).f = f.f

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁) (A : CategoryTheory.Monad.Algebra T₁) : ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).a = CategoryTheory.CategoryStruct.comp (h.app A.A) A.a

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁) (A : CategoryTheory.Monad.Algebra T₁) : ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).A = A.A

def CategoryTheory.Monad.algebraFunctorOfMonadHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₂ ⟶ T₁) : CategoryTheory.Functor (CategoryTheory.Monad.Algebra T₁) (CategoryTheory.Monad.Algebra T₂)

Given a monad morphism from T₂ to T₁, we get a functor from the algebras of T₁ to algebras of T₂.

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomId_inv_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T₁) : (CategoryTheory.Monad.algebraFunctorOfMonadHomId.inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).inv

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomId_hom_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : CategoryTheory.Monad.Algebra T₁) : (CategoryTheory.Monad.algebraFunctorOfMonadHomId.hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).hom

def CategoryTheory.Monad.algebraFunctorOfMonadHomId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} : CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁) ≅ CategoryTheory.Functor.id (CategoryTheory.Monad.Algebra T₁)

The identity monad morphism induces the identity functor from the category of algebras to itself.

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomComp_hom_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} {T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) (X : CategoryTheory.Monad.Algebra T₃) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomComp f g).hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g)).obj X).A).hom

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomComp_inv_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} {T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) (X : CategoryTheory.Monad.Algebra T₃) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomComp f g).inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g)).obj X).A).inv

def CategoryTheory.Monad.algebraFunctorOfMonadHomComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} {T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) : CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.Functor.comp (CategoryTheory.Monad.algebraFunctorOfMonadHom g) (CategoryTheory.Monad.algebraFunctorOfMonadHom f)

A composition of monad morphisms gives the composition of corresponding functors.

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomEq_hom_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} {f : T₁ ⟶ T₂} {g : T₁ ⟶ T₂} (h : f = g) (X : CategoryTheory.Monad.Algebra T₂) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).hom

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomEq_inv_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} {f : T₁ ⟶ T₂} {g : T₁ ⟶ T₂} (h : f = g) (X : CategoryTheory.Monad.Algebra T₂) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).inv

def CategoryTheory.Monad.algebraFunctorOfMonadHomEq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} {f : T₁ ⟶ T₂} {g : T₁ ⟶ T₂} (h : f = g) : CategoryTheory.Monad.algebraFunctorOfMonadHom f ≅ CategoryTheory.Monad.algebraFunctorOfMonadHom g

If f and g are two equal morphisms of monads, then the functors of algebras induced by them are isomorphic. We define it like this as opposed to using eqToIso so that the components are nicer to prove lemmas about.

@[simp]

theorem CategoryTheory.Monad.algebraEquivOfIsoMonads_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : (CategoryTheory.Monad.algebraEquivOfIsoMonads h).functor = CategoryTheory.Monad.algebraFunctorOfMonadHom h.inv

@[simp]

theorem CategoryTheory.Monad.algebraEquivOfIsoMonads_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : (CategoryTheory.Monad.algebraEquivOfIsoMonads h).unitIso = CategoryTheory.Monad.algebraFunctorOfMonadHomId.symm ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomEq (_ : CategoryTheory.CategoryStruct.id T₁ = CategoryTheory.CategoryStruct.comp h.hom h.inv) ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomComp h.hom h.inv

@[simp]

theorem CategoryTheory.Monad.algebraEquivOfIsoMonads_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : (CategoryTheory.Monad.algebraEquivOfIsoMonads h).inverse = CategoryTheory.Monad.algebraFunctorOfMonadHom h.hom

@[simp]

theorem CategoryTheory.Monad.algebraEquivOfIsoMonads_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : (CategoryTheory.Monad.algebraEquivOfIsoMonads h).counitIso = (CategoryTheory.Monad.algebraFunctorOfMonadHomComp h.inv h.hom).symm ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomEq (_ : CategoryTheory.CategoryStruct.comp h.inv h.hom = CategoryTheory.CategoryStruct.id T₂) ≪≫ CategoryTheory.Monad.algebraFunctorOfMonadHomId

def CategoryTheory.Monad.algebraEquivOfIsoMonads {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂) : CategoryTheory.Monad.Algebra T₁ ≌ CategoryTheory.Monad.Algebra T₂

Isomorphic monads give equivalent categories of algebras. Furthermore, they are equivalent as categories over C, that is, we have algebraEquivOfIsoMonads h ⋙ forget = forget.

@[simp]

theorem CategoryTheory.Monad.algebra_equiv_of_iso_monads_comp_forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} {T₂ : CategoryTheory.Monad C} (h : T₁ ⟶ T₂) : CategoryTheory.Functor.comp (CategoryTheory.Monad.algebraFunctorOfMonadHom h) (CategoryTheory.Monad.forget T₁) = CategoryTheory.Monad.forget T₂

structure CategoryTheory.Comonad.Coalgebra {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : Type (max u₁ v₁)

• A : C

  The underlying object associated to a coalgebra.

• a : s.A ⟶ G.obj s.A

  The structure morphism associated to a coalgebra.

• counit : CategoryTheory.CategoryStruct.comp s.a ((CategoryTheory.Comonad.ε G).app s.A) = CategoryTheory.CategoryStruct.id s.A

  The counit axiom associated to a coalgebra.

• coassoc : CategoryTheory.CategoryStruct.comp s.a ((CategoryTheory.Comonad.δ G).app s.A) = CategoryTheory.CategoryStruct.comp s.a (G.map s.a)

  The coassociativity axiom associated to a coalgebra.

An Eilenberg-Moore coalgebra for a comonad T.

theorem CategoryTheory.Comonad.Coalgebra.coassoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : CategoryTheory.Comonad.Coalgebra G) {Z : C} (h : (CategoryTheory.Functor.comp G.toFunctor G.toFunctor).obj self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.δ G).app self.A) h) = CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (G.map self.a) h)

theorem CategoryTheory.Comonad.Coalgebra.counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : CategoryTheory.Comonad.Coalgebra G) {Z : C} (h : (CategoryTheory.Functor.id C).obj self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comonad.ε G).app self.A) h) = h

theorem CategoryTheory.Comonad.Coalgebra.Hom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : CategoryTheory.Comonad.Coalgebra G} (x y : CategoryTheory.Comonad.Coalgebra.Hom A B), x.f = y.f → x = y

theorem CategoryTheory.Comonad.Coalgebra.Hom.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : CategoryTheory.Comonad.Coalgebra G} (x y : CategoryTheory.Comonad.Coalgebra.Hom A B), x = y ↔ x.f = y.f

structure CategoryTheory.Comonad.Coalgebra.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : CategoryTheory.Comonad.Coalgebra G) (B : CategoryTheory.Comonad.Coalgebra G) : Type v₁

• f : A.A ⟶ B.A

  The underlying morphism associated to a morphism of coalgebras.

• h : CategoryTheory.CategoryStruct.comp A.a (G.map s.f) = CategoryTheory.CategoryStruct.comp s.f B.a

  Compatibility with the structure morphism, for a morphism of coalgebras.

A morphism of Eilenberg-Moore coalgebras for the comonad G.

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.Hom.h_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : CategoryTheory.Comonad.Coalgebra G} {B : CategoryTheory.Comonad.Coalgebra G} (self : CategoryTheory.Comonad.Coalgebra.Hom A B) {Z : C} (h : G.obj B.A ⟶ Z) : CategoryTheory.CategoryStruct.comp A.a (CategoryTheory.CategoryStruct.comp (G.map self.f) h) = CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp B.a h)

def CategoryTheory.Comonad.Coalgebra.Hom.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : CategoryTheory.Comonad.Coalgebra G) : CategoryTheory.Comonad.Coalgebra.Hom A A

The identity homomorphism for an Eilenberg–Moore coalgebra.

def CategoryTheory.Comonad.Coalgebra.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {P : CategoryTheory.Comonad.Coalgebra G} {Q : CategoryTheory.Comonad.Coalgebra G} {R : CategoryTheory.Comonad.Coalgebra G} (f : CategoryTheory.Comonad.Coalgebra.Hom P Q) (g : CategoryTheory.Comonad.Coalgebra.Hom Q R) : CategoryTheory.Comonad.Coalgebra.Hom P R

Composition of Eilenberg–Moore coalgebra homomorphisms.

instance CategoryTheory.Comonad.Coalgebra.instCategoryStructCoalgebra {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} : CategoryTheory.CategoryStruct.{v₁, max u₁ v₁} (CategoryTheory.Comonad.Coalgebra G)

The category of Eilenberg-Moore coalgebras for a comonad.

theorem CategoryTheory.Comonad.Coalgebra.Hom.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (X : CategoryTheory.Comonad.Coalgebra G) (Y : CategoryTheory.Comonad.Coalgebra G) (f : X ⟶ Y) (g : X ⟶ Y) (h : f.f = g.f) : f = g

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.comp_eq_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : CategoryTheory.Comonad.Coalgebra G} {A' : CategoryTheory.Comonad.Coalgebra G} {A'' : CategoryTheory.Comonad.Coalgebra G} (f : A ⟶ A') (g : A' ⟶ A'') : CategoryTheory.Comonad.Coalgebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.id_eq_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : CategoryTheory.Comonad.Coalgebra G) : CategoryTheory.Comonad.Coalgebra.Hom.id A = CategoryTheory.CategoryStruct.id A

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.id_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : CategoryTheory.Comonad.Coalgebra G) : (CategoryTheory.CategoryStruct.id A).f = CategoryTheory.CategoryStruct.id A.A

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.comp_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : CategoryTheory.Comonad.Coalgebra G} {A' : CategoryTheory.Comonad.Coalgebra G} {A'' : CategoryTheory.Comonad.Coalgebra G} (f : A ⟶ A') (g : A' ⟶ A'') : (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f

instance CategoryTheory.Comonad.Coalgebra.eilenbergMoore {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} : CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Comonad.Coalgebra G)

The category of Eilenberg-Moore coalgebras for a comonad.

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.isoMk_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : CategoryTheory.Comonad.Coalgebra G} {B : CategoryTheory.Comonad.Coalgebra G} (h : A.A ≅ B.A) (w : autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a) _auto✝) : (CategoryTheory.Comonad.Coalgebra.isoMk h).inv.f = h.inv

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.isoMk_hom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : CategoryTheory.Comonad.Coalgebra G} {B : CategoryTheory.Comonad.Coalgebra G} (h : A.A ≅ B.A) (w : autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a) _auto✝) : (CategoryTheory.Comonad.Coalgebra.isoMk h).hom.f = h.hom

def CategoryTheory.Comonad.Coalgebra.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : CategoryTheory.Comonad.Coalgebra G} {B : CategoryTheory.Comonad.Coalgebra G} (h : A.A ≅ B.A) (w : autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map h.hom) = CategoryTheory.CategoryStruct.comp h.hom B.a) _auto✝) : A ≅ B

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

@[simp]

theorem CategoryTheory.Comonad.forget_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (A : CategoryTheory.Comonad.Coalgebra G) : (CategoryTheory.Comonad.forget G).obj A = A.A

@[simp]

theorem CategoryTheory.Comonad.forget_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : ∀ {X Y : CategoryTheory.Comonad.Coalgebra G} (f : X ⟶ Y), (CategoryTheory.Comonad.forget G).map f = f.f

def CategoryTheory.Comonad.forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.Functor (CategoryTheory.Comonad.Coalgebra G) C

The forgetful functor from the Eilenberg-Moore category, forgetting the coalgebraic structure.

@[simp]

theorem CategoryTheory.Comonad.cofree_map_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : ∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Comonad.cofree G).map f).f = G.map f

@[simp]

theorem CategoryTheory.Comonad.cofree_obj_A {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) : ((CategoryTheory.Comonad.cofree G).obj X).A = G.obj X

@[simp]

theorem CategoryTheory.Comonad.cofree_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C) : ((CategoryTheory.Comonad.cofree G).obj X).a = (CategoryTheory.Comonad.δ G).app X

def CategoryTheory.Comonad.cofree {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.Functor C (CategoryTheory.Comonad.Coalgebra G)

The cofree functor from the Eilenberg-Moore category, constructing a coalgebra for any object.

@[simp]

theorem CategoryTheory.Comonad.adj_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : (CategoryTheory.Comonad.adj G).unit = CategoryTheory.NatTrans.mk fun X => CategoryTheory.Comonad.Coalgebra.Hom.mk X.a

@[simp]

theorem CategoryTheory.Comonad.adj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : (CategoryTheory.Comonad.adj G).counit = CategoryTheory.NatTrans.mk fun Y => (CategoryTheory.Comonad.ε G).app Y

def CategoryTheory.Comonad.adj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.Comonad.forget G ⊣ CategoryTheory.Comonad.cofree G

The adjunction between the cofree and forgetful constructions for Eilenberg-Moore coalgebras for a comonad.

theorem CategoryTheory.Comonad.coalgebra_iso_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {A : CategoryTheory.Comonad.Coalgebra G} {B : CategoryTheory.Comonad.Coalgebra G} (f : A ⟶ B) [CategoryTheory.IsIso f.f] : CategoryTheory.IsIso f

Given a coalgebra morphism whose carrier part is an isomorphism, we get a coalgebra isomorphism.

instance CategoryTheory.Comonad.forget_reflects_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.ReflectsIsomorphisms (CategoryTheory.Comonad.forget G)

instance CategoryTheory.Comonad.forget_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.Faithful (CategoryTheory.Comonad.forget G)

theorem CategoryTheory.Comonad.algebra_epi_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X : CategoryTheory.Comonad.Coalgebra G} {Y : CategoryTheory.Comonad.Coalgebra G} (f : X ⟶ Y) [h : CategoryTheory.Epi f.f] : CategoryTheory.Epi f

Given a coalgebra morphism whose carrier part is an epimorphism, we get an algebra epimorphism.

theorem CategoryTheory.Comonad.algebra_mono_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X : CategoryTheory.Comonad.Coalgebra G} {Y : CategoryTheory.Comonad.Coalgebra G} (f : X ⟶ Y) [h : CategoryTheory.Mono f.f] : CategoryTheory.Mono f

Given a coalgebra morphism whose carrier part is a monomorphism, we get an algebra monomorphism.

instance CategoryTheory.Comonad.instIsLeftAdjointCoalgebraEilenbergMooreForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.IsLeftAdjoint (CategoryTheory.Comonad.forget G)

@[simp]

theorem CategoryTheory.Comonad.rightAdjoint_forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.rightAdjoint (CategoryTheory.Comonad.forget G) = CategoryTheory.Comonad.cofree G

@[simp]

theorem CategoryTheory.Comonad.ofLeftAdjoint_forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : CategoryTheory.Adjunction.ofLeftAdjoint (CategoryTheory.Comonad.forget G) = CategoryTheory.Comonad.adj G