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₁)

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

• A : C

  The underlying object associated to an algebra.

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

  The structure morphism associated to an algebra.

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

  The unit axiom associated to an algebra.

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

  The associativity axiom associated to an algebra.

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

The unit axiom associated to an algebra.

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

The associativity axiom associated to an algebra.

theorem CategoryTheory.Monad.Algebra.assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) {Z : C} (h : self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp (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.unit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra) {Z : C} (h : self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.η.app self.A) (CategoryTheory.CategoryStruct.comp self.a h) = h

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

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

• f : A.A ⟶ B.A

  The underlying morphism associated to a morphism of algebras.

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

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

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Monad.Algebra.Hom.h_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : T.Algebra} {B : T.Algebra} (self : A.Hom 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 : T.Algebra) : A.Hom A

The identity homomorphism for an Eilenberg–Moore algebra.

Equations

• CategoryTheory.Monad.Algebra.Hom.id A = { f := CategoryTheory.CategoryStruct.id A.A, h := ⋯ }

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

Equations

• CategoryTheory.Monad.Algebra.Hom.instInhabited A = { default := { f := CategoryTheory.CategoryStruct.id A.A, h := ⋯ } }

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

Composition of Eilenberg–Moore algebra homomorphisms.

Equations

• f.comp g = { f := CategoryTheory.CategoryStruct.comp f.f g.f, h := ⋯ }

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

Equations

• CategoryTheory.Monad.Algebra.instCategoryStruct = CategoryTheory.CategoryStruct.mk CategoryTheory.Monad.Algebra.Hom.id (@CategoryTheory.Monad.Algebra.Hom.comp C inst T)

theorem CategoryTheory.Monad.Algebra.Hom.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra) (Y : T.Algebra) (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 : T.Algebra} {A' : T.Algebra} {A'' : T.Algebra} (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 : T.Algebra) : 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 : T.Algebra) : (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 : T.Algebra} {A' : T.Algebra} {A'' : T.Algebra} (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₁} T.Algebra

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

Equations

• CategoryTheory.Monad.Algebra.eilenbergMoore = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def CategoryTheory.Monad.Algebra.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : T.Algebra} {B : T.Algebra} (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.

Equations

• CategoryTheory.Monad.Algebra.isoMk h w = { hom := { f := h.hom, h := ⋯ }, inv := { f := h.inv, h := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Monad.Algebra.isoMk_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : T.Algebra} {B : T.Algebra} (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 w).inv.f = h.inv

@[simp]

theorem CategoryTheory.Monad.Algebra.isoMk_hom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A : T.Algebra} {B : T.Algebra} (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 w).hom.f = h.hom

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

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

Equations

• T.forget = { obj := fun (A : T.Algebra) => A.A, map := fun {X Y : T.Algebra} (f : X ⟶ Y) => f.f, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• T.free = { obj := fun (X : C) => { A := T.obj X, a := T.μ.app X, unit := ⋯, assoc := ⋯ }, map := fun {X Y : C} (f : X ⟶ Y) => { f := T.map f, h := ⋯ }, map_id := ⋯, map_comp := ⋯ }

@[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), (T.free.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) : (T.free.obj X).a = T.μ.app X

@[simp]

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

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

Equations

• T.instInhabitedAlgebra = { default := T.free.obj default }

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Monad.adj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.adj.counit = { app := fun (Y : T.Algebra) => { f := Y.a, h := ⋯ }, naturality := ⋯ }

@[simp]

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

theorem CategoryTheory.Monad.algebra_iso_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {A : T.Algebra} {B : T.Algebra} (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) : T.forget.ReflectsIsomorphisms

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Monad.algebra_epi_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X : T.Algebra} {Y : T.Algebra} (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 : T.Algebra} {Y : T.Algebra} (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.instIsRightAdjointAlgebraForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) : T.forget.IsRightAdjoint

Equations

• ⋯ = ⋯

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 T₁.Algebra T₂.Algebra

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : T₁.Algebra) : ((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 : T₁.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).A = A.A

@[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 : T₁.Algebra} (f : X ⟶ Y), ((CategoryTheory.Monad.algebraFunctorOfMonadHom h).map f).f = f.f

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 T₁.Algebra

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomId_inv_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : T₁.Algebra) : (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 : T₁.Algebra) : (CategoryTheory.Monad.algebraFunctorOfMonadHomId.hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).hom

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.Monad.algebraFunctorOfMonadHom g).comp (CategoryTheory.Monad.algebraFunctorOfMonadHom f)

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

Equations

• One or more equations did not get rendered due to their size.

@[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 : T₃.Algebra) : ((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 : T₃.Algebra) : ((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.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.

Equations

• One or more equations did not get rendered due to their size.

@[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 : T₂.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).inv.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).inv

@[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 : T₂.Algebra) : ((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).hom.app X).f = (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).hom

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

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

Equations

• One or more equations did not get rendered due to their size.

@[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.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_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_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.Monad.algebraFunctorOfMonadHomId

@[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.Monad.algebraFunctorOfMonadHom h).comp T₁.forget = T₂.forget

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

An Eilenberg-Moore coalgebra for a comonad T.

• A : C

  The underlying object associated to a coalgebra.

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

  The structure morphism associated to a coalgebra.

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

  The counit axiom associated to a coalgebra.

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

  The coassociativity axiom associated to a coalgebra.

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

The counit axiom associated to a coalgebra.

theorem CategoryTheory.Comonad.Coalgebra.coassoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) : CategoryTheory.CategoryStruct.comp self.a (G.δ.app self.A) = CategoryTheory.CategoryStruct.comp self.a (G.map self.a)

The coassociativity axiom associated to a coalgebra.

theorem CategoryTheory.Comonad.Coalgebra.coassoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (self : G.Coalgebra) {Z : C} (h : G.obj (G.obj self.A) ⟶ Z) : CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (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 : G.Coalgebra) {Z : C} (h : self.A ⟶ Z) : CategoryTheory.CategoryStruct.comp self.a (CategoryTheory.CategoryStruct.comp (G.ε.app self.A) h) = h

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

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

• f : A.A ⟶ B.A

  The underlying morphism associated to a morphism of coalgebras.

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

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

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

@[simp]

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

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

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.Hom.h_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : G.Coalgebra} {B : G.Coalgebra} (self : A.Hom 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 : G.Coalgebra) : A.Hom A

The identity homomorphism for an Eilenberg–Moore coalgebra.

Equations

• CategoryTheory.Comonad.Coalgebra.Hom.id A = { f := CategoryTheory.CategoryStruct.id A.A, h := ⋯ }

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

Composition of Eilenberg–Moore coalgebra homomorphisms.

Equations

• f.comp g = { f := CategoryTheory.CategoryStruct.comp f.f g.f, h := ⋯ }

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

The category of Eilenberg-Moore coalgebras for a comonad.

Equations

• CategoryTheory.Comonad.Coalgebra.instCategoryStruct = CategoryTheory.CategoryStruct.mk CategoryTheory.Comonad.Coalgebra.Hom.id (@CategoryTheory.Comonad.Coalgebra.Hom.comp C inst G)

theorem CategoryTheory.Comonad.Coalgebra.Hom.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (X : G.Coalgebra) (Y : G.Coalgebra) (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 : G.Coalgebra} {A' : G.Coalgebra} {A'' : G.Coalgebra} (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 : G.Coalgebra) : 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 : G.Coalgebra) : (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 : G.Coalgebra} {A' : G.Coalgebra} {A'' : G.Coalgebra} (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₁} G.Coalgebra

The category of Eilenberg-Moore coalgebras for a comonad.

Equations

• CategoryTheory.Comonad.Coalgebra.eilenbergMoore = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def CategoryTheory.Comonad.Coalgebra.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : G.Coalgebra} {B : G.Coalgebra} (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.

Equations

• CategoryTheory.Comonad.Coalgebra.isoMk h w = { hom := { f := h.hom, h := ⋯ }, inv := { f := h.inv, h := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.isoMk_hom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : G.Coalgebra} {B : G.Coalgebra} (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 w).hom.f = h.hom

@[simp]

theorem CategoryTheory.Comonad.Coalgebra.isoMk_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A : G.Coalgebra} {B : G.Coalgebra} (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 w).inv.f = h.inv

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

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

Equations

• G.forget = { obj := fun (A : G.Coalgebra) => A.A, map := fun {X Y : G.Coalgebra} (f : X ⟶ Y) => f.f, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

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

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

Equations

• G.cofree = { obj := fun (X : C) => { A := G.obj X, a := G.δ.app X, counit := ⋯, coassoc := ⋯ }, map := fun {X Y : C} (f : X ⟶ Y) => { f := G.map f, h := ⋯ }, map_id := ⋯, map_comp := ⋯ }

@[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), (G.cofree.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) : (G.cofree.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) : (G.cofree.obj X).a = G.δ.app X

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem CategoryTheory.Comonad.adj_unit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.adj.unit = { app := fun (X : G.Coalgebra) => { f := X.a, h := ⋯ }, naturality := ⋯ }

theorem CategoryTheory.Comonad.coalgebra_iso_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {A : G.Coalgebra} {B : G.Coalgebra} (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) : G.forget.ReflectsIsomorphisms

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Comonad.algebra_epi_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X : G.Coalgebra} {Y : G.Coalgebra} (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 : G.Coalgebra} {Y : G.Coalgebra} (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.instIsLeftAdjointCoalgebraForget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) : G.forget.IsLeftAdjoint

Equations

• ⋯ = ⋯