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]

source

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.

Instances For

source

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)

source

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

source

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

Instances For

source

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} (f : x.f = y.f) :

x = y

source

@[simp]

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

source

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 := ⋯ }

Instances For

source

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 := ⋯ } }

source

def CategoryTheory.Monad.Algebra.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {P Q 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 := ⋯ }

Instances For

source

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)

source

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

f = g

source

@[simp]

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

CategoryTheory.Monad.Algebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

source

@[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

source

@[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

source

@[simp]

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

(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f

source

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 ⋯ ⋯ ⋯

source

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

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 := ⋯ }

Instances For

source

@[simp]

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

(CategoryTheory.Monad.Algebra.isoMk h w).inv.f = h.inv

source

@[simp]

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

(CategoryTheory.Monad.Algebra.isoMk h w).hom.f = h.hom

source

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 := ⋯ }

Instances For

source

@[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

source

@[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

source

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 := ⋯ }

Instances For

source

@[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

source

@[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

source

@[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

source

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 }

source

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.

Instances For

source

@[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 := ⋯ }

source

@[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 := ⋯ }

source

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

source

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

T.forget.ReflectsIsomorphisms

Equations

⋯ = ⋯

source

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

T.forget.Faithful

Equations

⋯ = ⋯

source

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

source

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

source

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

T.forget.IsRightAdjoint

Equations

⋯ = ⋯

source

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

Instances For

source

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHom_obj_a {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ 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

source

@[simp]

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

((CategoryTheory.Monad.algebraFunctorOfMonadHom h).obj A).A = A.A

source

@[simp]

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

((CategoryTheory.Monad.algebraFunctorOfMonadHom h).map f).f = f.f

source

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.

Instances For

source

@[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

source

@[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

source

def CategoryTheory.Monad.algebraFunctorOfMonadHomComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ 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.

Instances For

source

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomComp_hom_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ 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

source

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomComp_inv_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ 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

source

def CategoryTheory.Monad.algebraFunctorOfMonadHomEq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f 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.

Instances For

source

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomEq_inv_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f 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

source

@[simp]

theorem CategoryTheory.Monad.algebraFunctorOfMonadHomEq_hom_app_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f 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

source

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

Instances For

source

@[simp]

theorem CategoryTheory.Monad.algebraEquivOfIsoMonads_unitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ 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

source

@[simp]

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

(CategoryTheory.Monad.algebraEquivOfIsoMonads h).inverse = CategoryTheory.Monad.algebraFunctorOfMonadHom h.hom

source

@[simp]

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

(CategoryTheory.Monad.algebraEquivOfIsoMonads h).functor = CategoryTheory.Monad.algebraFunctorOfMonadHom h.inv

source

@[simp]

theorem CategoryTheory.Monad.algebraEquivOfIsoMonads_counitIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T₁ 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

source

@[simp]

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

(CategoryTheory.Monad.algebraFunctorOfMonadHom h).comp T₁.forget = T₂.forget

source

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.

Instances For

source

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)

source

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

source

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

Instances For

source

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} (f : x.f = y.f) :

x = y

source

@[simp]

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

source

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 := ⋯ }

Instances For

source

def CategoryTheory.Comonad.Coalgebra.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {P Q 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 := ⋯ }

Instances For

source

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)

source

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

f = g

source

@[simp]

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

CategoryTheory.Comonad.Coalgebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

source

@[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

source

@[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

source

@[simp]

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

(CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f

source

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 ⋯ ⋯ ⋯

source

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

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 := ⋯ }

Instances For

source

@[simp]

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

(CategoryTheory.Comonad.Coalgebra.isoMk h w).hom.f = h.hom

source

@[simp]

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

(CategoryTheory.Comonad.Coalgebra.isoMk h w).inv.f = h.inv

source

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 := ⋯ }

Instances For

source

@[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

source

@[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

source

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 := ⋯ }