category_theory.monad.algebra

structure category_theory.monad.algebra {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

Type (max u₁ v₁)

A : C
a : ↑T.obj self.A ⟶ self.A
unit' : T.η.app self.A ≫ self.a = 𝟙 self.A . "obviously"
assoc' : T.μ.app self.A ≫ self.a = ↑T.map self.a ≫ self.a . "obviously"

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

Instances for category_theory.monad.algebra

category_theory.monad.algebra.has_sizeof_inst
category_theory.monad.algebra.category_theory.category_struct
category_theory.monad.algebra.EilenbergMoore
category_theory.monad.algebra.inhabited
category_theory.monad.algebra_preadditive

theorem category_theory.monad.algebra.unit {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (self : T.algebra) :

T.η.app self.A ≫ self.a = 𝟙 self.A

source

theorem category_theory.monad.algebra.assoc {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (self : T.algebra) :

T.μ.app self.A ≫ self.a = ↑T.map self.a ≫ self.a

source

theorem category_theory.monad.algebra.unit_assoc {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (self : T.algebra) {X' : C} (f' : self.A ⟶ X') :

T.η.app self.A ≫ self.a ≫ f' = f'

source

theorem category_theory.monad.algebra.assoc_assoc {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (self : T.algebra) {X' : C} (f' : self.A ⟶ X') :

T.μ.app self.A ≫ self.a ≫ f' = ↑T.map self.a ≫ self.a ≫ f'

source

@[ext]

structure category_theory.monad.algebra.hom {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (A B : T.algebra) :

Type v₁

f : A.A ⟶ B.A
h' : ↑T.map self.f ≫ B.a = A.a ≫ self.f . "obviously"

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

Instances for category_theory.monad.algebra.hom

category_theory.monad.algebra.hom.has_sizeof_inst
category_theory.monad.algebra.hom.inhabited

source

theorem category_theory.monad.algebra.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {T : category_theory.monad C} {A B : T.algebra} (x y : A.hom B) (h : x.f = y.f) :

x = y

source

theorem category_theory.monad.algebra.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {T : category_theory.monad C} {A B : T.algebra} (x y : A.hom B) :

x = y ↔ x.f = y.f

source

@[simp]

theorem category_theory.monad.algebra.hom.h {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A B : T.algebra} (self : A.hom B) :

↑T.map self.f ≫ B.a = A.a ≫ self.f

source

@[simp]

theorem category_theory.monad.algebra.hom.h_assoc {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A B : T.algebra} (self : A.hom B) {X' : C} (f' : B.A ⟶ X') :

↑T.map self.f ≫ B.a ≫ f' = A.a ≫ self.f ≫ f'

source

def category_theory.monad.algebra.hom.id {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (A : T.algebra) :

A.hom A

The identity homomorphism for an Eilenberg–Moore algebra.

Equations

category_theory.monad.algebra.hom.id A = {f := 𝟙 A.A, h' := _}

source

@[protected, instance]

def category_theory.monad.algebra.hom.inhabited {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (A : T.algebra) :

inhabited (A.hom A)

Equations

category_theory.monad.algebra.hom.inhabited A = {default := {f := 𝟙 A.A, h' := _}}

source

def category_theory.monad.algebra.hom.comp {C : Type u₁} [category_theory.category C] {T : category_theory.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 := f.f ≫ g.f, h' := _}

source

@[protected, instance]

def category_theory.monad.algebra.category_theory.category_struct {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} :

category_theory.category_struct T.algebra

Equations

category_theory.monad.algebra.category_theory.category_struct = {to_quiver := {hom := category_theory.monad.algebra.hom T}, id := category_theory.monad.algebra.hom.id T, comp := category_theory.monad.algebra.hom.comp T}

source

@[simp]

theorem category_theory.monad.algebra.comp_eq_comp {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A A' A'' : T.algebra} (f : A ⟶ A') (g : A' ⟶ A'') :

category_theory.monad.algebra.hom.comp f g = f ≫ g

source

@[simp]

theorem category_theory.monad.algebra.id_eq_id {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (A : T.algebra) :

category_theory.monad.algebra.hom.id A = 𝟙 A

source

@[simp]

theorem category_theory.monad.algebra.id_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} (A : T.algebra) :

(𝟙 A).f = 𝟙 A.A

source

@[simp]

theorem category_theory.monad.algebra.comp_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A A' A'' : T.algebra} (f : A ⟶ A') (g : A' ⟶ A'') :

(f ≫ g).f = f.f ≫ g.f

source

@[protected, instance]

def category_theory.monad.algebra.EilenbergMoore {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} :

category_theory.category T.algebra

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

Equations

category_theory.monad.algebra.EilenbergMoore = {to_category_struct := category_theory.monad.algebra.category_theory.category_struct T, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

theorem category_theory.monad.algebra.iso_mk_hom_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A B : T.algebra} (h : A.A ≅ B.A) (w : ↑T.map h.hom ≫ B.a = A.a ≫ h.hom) :

(category_theory.monad.algebra.iso_mk h w).hom.f = h.hom

source

def category_theory.monad.algebra.iso_mk {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A B : T.algebra} (h : A.A ≅ B.A) (w : ↑T.map h.hom ≫ B.a = A.a ≫ h.hom) :

A ≅ B

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

Equations

category_theory.monad.algebra.iso_mk h w = {hom := {f := h.hom, h' := w}, inv := {f := h.inv, h' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.monad.algebra.iso_mk_inv_f {C : Type u₁} [category_theory.category C] {T : category_theory.monad C} {A B : T.algebra} (h : A.A ≅ B.A) (w : ↑T.map h.hom ≫ B.a = A.a ≫ h.hom) :

(category_theory.monad.algebra.iso_mk h w).inv.f = h.inv

source

@[simp]

theorem category_theory.monad.forget_map {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) (A B : T.algebra) (f : A ⟶ B) :

T.forget.map f = f.f

source

@[simp]

theorem category_theory.monad.forget_obj {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) (A : T.algebra) :

T.forget.obj A = A.A

source

def category_theory.monad.forget {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

T.algebra ⥤ C

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

Equations

T.forget = {obj := λ (A : T.algebra), A.A, map := λ (A B : T.algebra) (f : A ⟶ B), f.f, map_id' := _, map_comp' := _}

Instances for category_theory.monad.forget

source

@[simp]

theorem category_theory.monad.free_obj_A {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) (X : C) :

(T.free.obj X).A = T.to_functor.obj X

source

def category_theory.monad.free {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

C ⥤ T.algebra

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

Equations

T.free = {obj := λ (X : C), {A := T.to_functor.obj X, a := T.μ.app X, unit' := _, assoc' := _}, map := λ (X Y : C) (f : X ⟶ Y), {f := T.to_functor.map f, h' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.monad.free_obj_a {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) (X : C) :

(T.free.obj X).a = T.μ.app X

source

@[simp]

theorem category_theory.monad.free_map_f {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) (X Y : C) (f : X ⟶ Y) :

(T.free.map f).f = T.to_functor.map f

source

@[protected, instance]

def category_theory.monad.algebra.inhabited {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) [inhabited C] :

inhabited T.algebra

Equations

category_theory.monad.algebra.inhabited T = {default := T.free.obj inhabited.default}

source

def category_theory.monad.adj {C : Type u₁} [category_theory.category C] (T : category_theory.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.

Equations

T.adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : C) (Y : T.algebra), {to_fun := λ (f : T.free.obj X ⟶ Y), T.η.app X ≫ f.f, inv_fun := λ (f : X ⟶ T.forget.obj Y), {f := T.to_functor.map f ≫ Y.a, h' := _}, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

source

@[simp]

theorem category_theory.monad.adj_unit {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

T.adj.unit = {app := T.η.app, naturality' := _}

source

@[simp]

theorem category_theory.monad.adj_counit {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

T.adj.counit = {app := λ (Y : T.algebra), {f := Y.a, h' := _}, naturality' := _}

source

theorem category_theory.monad.algebra_iso_of_iso {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) {A B : T.algebra} (f : A ⟶ B) [category_theory.is_iso f.f] :

category_theory.is_iso f

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

source

@[protected, instance]

def category_theory.monad.forget_reflects_iso {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

category_theory.reflects_isomorphisms T.forget

source

@[protected, instance]

def category_theory.monad.forget_faithful {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

category_theory.faithful T.forget

source

theorem category_theory.monad.algebra_epi_of_epi {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) {X Y : T.algebra} (f : X ⟶ Y) [h : category_theory.epi f.f] :

category_theory.epi f

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

source

theorem category_theory.monad.algebra_mono_of_mono {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) {X Y : T.algebra} (f : X ⟶ Y) [h : category_theory.mono f.f] :

category_theory.mono f

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

source

@[protected, instance]

def category_theory.monad.forget.category_theory.is_right_adjoint {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

category_theory.is_right_adjoint T.forget

Equations

category_theory.monad.forget.category_theory.is_right_adjoint T = {left := T.free, adj := T.adj}

source

@[simp]

theorem category_theory.monad.left_adjoint_forget {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

category_theory.left_adjoint T.forget = T.free

source

@[simp]

theorem category_theory.monad.of_right_adjoint_forget {C : Type u₁} [category_theory.category C] (T : category_theory.monad C) :

category_theory.adjunction.of_right_adjoint T.forget = T.adj

source

def category_theory.monad.algebra_functor_of_monad_hom {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₂ ⟶ T₁) :

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

category_theory.monad.algebra_functor_of_monad_hom h = {obj := λ (A : T₁.algebra), {A := A.A, a := h.to_nat_trans.app A.A ≫ A.a, unit' := _, assoc' := _}, map := λ (A₁ A₂ : T₁.algebra) (f : A₁ ⟶ A₂), {f := f.f, h' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_map_f {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₂ ⟶ T₁) (A₁ A₂ : T₁.algebra) (f : A₁ ⟶ A₂) :

((category_theory.monad.algebra_functor_of_monad_hom h).map f).f = f.f

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_obj_a {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₂ ⟶ T₁) (A : T₁.algebra) :

((category_theory.monad.algebra_functor_of_monad_hom h).obj A).a = h.to_nat_trans.app A.A ≫ A.a

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_obj_A {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₂ ⟶ T₁) (A : T₁.algebra) :

((category_theory.monad.algebra_functor_of_monad_hom h).obj A).A = A.A

source

def category_theory.monad.algebra_functor_of_monad_hom_id {C : Type u₁} [category_theory.category C] {T₁ : category_theory.monad C} :

category_theory.monad.algebra_functor_of_monad_hom (𝟙 T₁) ≅ 𝟭 T₁.algebra

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

Equations

category_theory.monad.algebra_functor_of_monad_hom_id = category_theory.nat_iso.of_components (λ (X : T₁.algebra), category_theory.monad.algebra.iso_mk (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom (𝟙 T₁)).obj X).A) _) category_theory.monad.algebra_functor_of_monad_hom_id._proof_2

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_id_inv_app_f {C : Type u₁} [category_theory.category C] {T₁ : category_theory.monad C} (X : T₁.algebra) :

(category_theory.monad.algebra_functor_of_monad_hom_id.inv.app X).f = (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom (𝟙 T₁)).obj X).A).inv

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_id_hom_app_f {C : Type u₁} [category_theory.category C] {T₁ : category_theory.monad C} (X : T₁.algebra) :

(category_theory.monad.algebra_functor_of_monad_hom_id.hom.app X).f = (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom (𝟙 T₁)).obj X).A).hom

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_comp_inv_app_f {C : Type u₁} [category_theory.category C] {T₁ T₂ T₃ : category_theory.monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) (X : T₃.algebra) :

((category_theory.monad.algebra_functor_of_monad_hom_comp f g).inv.app X).f = (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom (f ≫ g)).obj X).A).inv

source

def category_theory.monad.algebra_functor_of_monad_hom_comp {C : Type u₁} [category_theory.category C] {T₁ T₂ T₃ : category_theory.monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) :

category_theory.monad.algebra_functor_of_monad_hom (f ≫ g) ≅ category_theory.monad.algebra_functor_of_monad_hom g ⋙ category_theory.monad.algebra_functor_of_monad_hom f

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

Equations

category_theory.monad.algebra_functor_of_monad_hom_comp f g = category_theory.nat_iso.of_components (λ (X : T₃.algebra), category_theory.monad.algebra.iso_mk (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom (f ≫ g)).obj X).A) _) _

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_comp_hom_app_f {C : Type u₁} [category_theory.category C] {T₁ T₂ T₃ : category_theory.monad C} (f : T₁ ⟶ T₂) (g : T₂ ⟶ T₃) (X : T₃.algebra) :

((category_theory.monad.algebra_functor_of_monad_hom_comp f g).hom.app X).f = (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom (f ≫ g)).obj X).A).hom

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_eq_hom_app_f {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} {f g : T₁ ⟶ T₂} (h : f = g) (X : T₂.algebra) :

((category_theory.monad.algebra_functor_of_monad_hom_eq h).hom.app X).f = (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom f).obj X).A).hom

source

@[simp]

theorem category_theory.monad.algebra_functor_of_monad_hom_eq_inv_app_f {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} {f g : T₁ ⟶ T₂} (h : f = g) (X : T₂.algebra) :

((category_theory.monad.algebra_functor_of_monad_hom_eq h).inv.app X).f = (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom f).obj X).A).inv

source

def category_theory.monad.algebra_functor_of_monad_hom_eq {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} {f g : T₁ ⟶ T₂} (h : f = g) :

category_theory.monad.algebra_functor_of_monad_hom f ≅ category_theory.monad.algebra_functor_of_monad_hom 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 eq_to_iso so that the components are nicer to prove lemmas about.

Equations

category_theory.monad.algebra_functor_of_monad_hom_eq h = category_theory.nat_iso.of_components (λ (X : T₂.algebra), category_theory.monad.algebra.iso_mk (category_theory.iso.refl ((category_theory.monad.algebra_functor_of_monad_hom f).obj X).A) _) _

source

@[simp]

theorem category_theory.monad.algebra_equiv_of_iso_monads_unit_iso {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₁ ≅ T₂) :

(category_theory.monad.algebra_equiv_of_iso_monads h).unit_iso = category_theory.monad.algebra_functor_of_monad_hom_id.symm ≪≫ category_theory.monad.algebra_functor_of_monad_hom_eq _ ≪≫ category_theory.monad.algebra_functor_of_monad_hom_comp h.hom h.inv

source

@[simp]

theorem category_theory.monad.algebra_equiv_of_iso_monads_inverse {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₁ ≅ T₂) :

(category_theory.monad.algebra_equiv_of_iso_monads h).inverse = category_theory.monad.algebra_functor_of_monad_hom h.hom

source

def category_theory.monad.algebra_equiv_of_iso_monads {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.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 algebra_equiv_of_iso_monads h ⋙ forget = forget.

Equations

source

@[simp]

theorem category_theory.monad.algebra_equiv_of_iso_monads_counit_iso {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₁ ≅ T₂) :

(category_theory.monad.algebra_equiv_of_iso_monads h).counit_iso = (category_theory.monad.algebra_functor_of_monad_hom_comp h.inv h.hom).symm ≪≫ category_theory.monad.algebra_functor_of_monad_hom_eq _ ≪≫ category_theory.monad.algebra_functor_of_monad_hom_id

source

@[simp]

theorem category_theory.monad.algebra_equiv_of_iso_monads_functor {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₁ ≅ T₂) :

(category_theory.monad.algebra_equiv_of_iso_monads h).functor = category_theory.monad.algebra_functor_of_monad_hom h.inv

source

@[simp]

theorem category_theory.monad.algebra_equiv_of_iso_monads_comp_forget {C : Type u₁} [category_theory.category C] {T₁ T₂ : category_theory.monad C} (h : T₁ ⟶ T₂) :

category_theory.monad.algebra_functor_of_monad_hom h ⋙ T₁.forget = T₂.forget

source

@[nolint]

structure category_theory.comonad.coalgebra {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

Type (max u₁ v₁)

A : C
a : self.A ⟶ ↑G.obj self.A
counit' : self.a ≫ G.ε.app self.A = 𝟙 self.A . "obviously"
coassoc' : self.a ≫ G.δ.app self.A = self.a ≫ G.to_functor.map self.a . "obviously"

An Eilenberg-Moore coalgebra for a comonad T.

Instances for category_theory.comonad.coalgebra

category_theory.comonad.coalgebra.has_sizeof_inst
category_theory.comonad.coalgebra.category_theory.category_struct
category_theory.comonad.coalgebra.EilenbergMoore
category_theory.comonad.coalgebra_preadditive

source

theorem category_theory.comonad.coalgebra.counit {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (self : G.coalgebra) :

self.a ≫ G.ε.app self.A = 𝟙 self.A

source

theorem category_theory.comonad.coalgebra.coassoc {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (self : G.coalgebra) :

self.a ≫ G.δ.app self.A = self.a ≫ ↑G.map self.a

source

theorem category_theory.comonad.coalgebra.counit_assoc {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (self : G.coalgebra) {X' : C} (f' : self.A ⟶ X') :

self.a ≫ G.ε.app self.A ≫ f' = f'

source

theorem category_theory.comonad.coalgebra.coassoc_assoc {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (self : G.coalgebra) {X' : C} (f' : ↑G.obj (↑G.obj self.A) ⟶ X') :

self.a ≫ G.δ.app self.A ≫ f' = self.a ≫ ↑G.map self.a ≫ f'

source

theorem category_theory.comonad.coalgebra.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {G : category_theory.comonad C} {A B : G.coalgebra} (x y : A.hom B) :

x = y ↔ x.f = y.f

source

@[nolint, ext]

structure category_theory.comonad.coalgebra.hom {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (A B : G.coalgebra) :

Type v₁

f : A.A ⟶ B.A
h' : A.a ≫ ↑G.map self.f = self.f ≫ B.a . "obviously"

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

Instances for category_theory.comonad.coalgebra.hom

category_theory.comonad.coalgebra.hom.has_sizeof_inst

source

theorem category_theory.comonad.coalgebra.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {G : category_theory.comonad C} {A B : G.coalgebra} (x y : A.hom B) (h : x.f = y.f) :

x = y

source

@[simp]

theorem category_theory.comonad.coalgebra.hom.h {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A B : G.coalgebra} (self : A.hom B) :

A.a ≫ ↑G.map self.f = self.f ≫ B.a

source

@[simp]

theorem category_theory.comonad.coalgebra.hom.h_assoc {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A B : G.coalgebra} (self : A.hom B) {X' : C} (f' : ↑G.obj B.A ⟶ X') :

A.a ≫ ↑G.map self.f ≫ f' = self.f ≫ B.a ≫ f'

source

def category_theory.comonad.coalgebra.hom.id {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (A : G.coalgebra) :

A.hom A

The identity homomorphism for an Eilenberg–Moore coalgebra.

Equations

category_theory.comonad.coalgebra.hom.id A = {f := 𝟙 A.A, h' := _}

source

def category_theory.comonad.coalgebra.hom.comp {C : Type u₁} [category_theory.category C] {G : category_theory.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 := f.f ≫ g.f, h' := _}

source

@[protected, instance]

def category_theory.comonad.coalgebra.category_theory.category_struct {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} :

category_theory.category_struct G.coalgebra

The category of Eilenberg-Moore coalgebras for a comonad.

Equations

category_theory.comonad.coalgebra.category_theory.category_struct = {to_quiver := {hom := category_theory.comonad.coalgebra.hom G}, id := category_theory.comonad.coalgebra.hom.id G, comp := category_theory.comonad.coalgebra.hom.comp G}

source

@[simp]

theorem category_theory.comonad.coalgebra.comp_eq_comp {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A A' A'' : G.coalgebra} (f : A ⟶ A') (g : A' ⟶ A'') :

category_theory.comonad.coalgebra.hom.comp f g = f ≫ g

source

@[simp]

theorem category_theory.comonad.coalgebra.id_eq_id {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (A : G.coalgebra) :

category_theory.comonad.coalgebra.hom.id A = 𝟙 A

source

@[simp]

theorem category_theory.comonad.coalgebra.id_f {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} (A : G.coalgebra) :

(𝟙 A).f = 𝟙 A.A

source

@[simp]

theorem category_theory.comonad.coalgebra.comp_f {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A A' A'' : G.coalgebra} (f : A ⟶ A') (g : A' ⟶ A'') :

(f ≫ g).f = f.f ≫ g.f

source

@[protected, instance]

def category_theory.comonad.coalgebra.EilenbergMoore {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} :

category_theory.category G.coalgebra

The category of Eilenberg-Moore coalgebras for a comonad.

Equations

category_theory.comonad.coalgebra.EilenbergMoore = {to_category_struct := category_theory.comonad.coalgebra.category_theory.category_struct G, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

theorem category_theory.comonad.coalgebra.iso_mk_inv_f {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A B : G.coalgebra} (h : A.A ≅ B.A) (w : A.a ≫ ↑G.map h.hom = h.hom ≫ B.a) :

(category_theory.comonad.coalgebra.iso_mk h w).inv.f = h.inv

source

@[simp]

theorem category_theory.comonad.coalgebra.iso_mk_hom_f {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A B : G.coalgebra} (h : A.A ≅ B.A) (w : A.a ≫ ↑G.map h.hom = h.hom ≫ B.a) :

(category_theory.comonad.coalgebra.iso_mk h w).hom.f = h.hom

source

def category_theory.comonad.coalgebra.iso_mk {C : Type u₁} [category_theory.category C] {G : category_theory.comonad C} {A B : G.coalgebra} (h : A.A ≅ B.A) (w : A.a ≫ ↑G.map h.hom = h.hom ≫ B.a) :

A ≅ B

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

Equations

category_theory.comonad.coalgebra.iso_mk h w = {hom := {f := h.hom, h' := w}, inv := {f := h.inv, h' := _}, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.comonad.forget_map {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) (A B : G.coalgebra) (f : A ⟶ B) :

G.forget.map f = f.f

source

@[simp]

theorem category_theory.comonad.forget_obj {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) (A : G.coalgebra) :

G.forget.obj A = A.A

source

def category_theory.comonad.forget {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

G.coalgebra ⥤ C

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

Equations

G.forget = {obj := λ (A : G.coalgebra), A.A, map := λ (A B : G.coalgebra) (f : A ⟶ B), f.f, map_id' := _, map_comp' := _}

Instances for category_theory.comonad.forget

source

@[simp]

theorem category_theory.comonad.cofree_map_f {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) (X Y : C) (f : X ⟶ Y) :

(G.cofree.map f).f = G.to_functor.map f

source

@[simp]

theorem category_theory.comonad.cofree_obj_a {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) (X : C) :

(G.cofree.obj X).a = G.δ.app X

source

@[simp]

theorem category_theory.comonad.cofree_obj_A {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) (X : C) :

(G.cofree.obj X).A = G.to_functor.obj X

source

def category_theory.comonad.cofree {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

C ⥤ G.coalgebra

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

Equations

G.cofree = {obj := λ (X : C), {A := G.to_functor.obj X, a := G.δ.app X, counit' := _, coassoc' := _}, map := λ (X Y : C) (f : X ⟶ Y), {f := G.to_functor.map f, h' := _}, map_id' := _, map_comp' := _}

source

def category_theory.comonad.adj {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

G.forget ⊣ G.cofree

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

Equations

G.adj = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X : G.coalgebra) (Y : C), {to_fun := λ (f : G.forget.obj X ⟶ Y), {f := X.a ≫ G.to_functor.map f, h' := _}, inv_fun := λ (g : X ⟶ G.cofree.obj Y), g.f ≫ G.ε.app Y, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}

source

@[simp]

theorem category_theory.comonad.adj_counit {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

G.adj.counit = {app := G.ε.app, naturality' := _}

source

@[simp]

theorem category_theory.comonad.adj_unit {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

G.adj.unit = {app := λ (X : G.coalgebra), {f := X.a, h' := _}, naturality' := _}

source

theorem category_theory.comonad.coalgebra_iso_of_iso {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) {A B : G.coalgebra} (f : A ⟶ B) [category_theory.is_iso f.f] :

category_theory.is_iso f

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

source

@[protected, instance]

def category_theory.comonad.forget_reflects_iso {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

category_theory.reflects_isomorphisms G.forget

source

@[protected, instance]

def category_theory.comonad.forget_faithful {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

category_theory.faithful G.forget

source

theorem category_theory.comonad.algebra_epi_of_epi {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) {X Y : G.coalgebra} (f : X ⟶ Y) [h : category_theory.epi f.f] :

category_theory.epi f

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

source

theorem category_theory.comonad.algebra_mono_of_mono {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) {X Y : G.coalgebra} (f : X ⟶ Y) [h : category_theory.mono f.f] :

category_theory.mono f

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

source

@[protected, instance]

def category_theory.comonad.forget.category_theory.is_left_adjoint {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

category_theory.is_left_adjoint G.forget

Equations

category_theory.comonad.forget.category_theory.is_left_adjoint G = {right := G.cofree, adj := G.adj}

source

@[simp]

theorem category_theory.comonad.right_adjoint_forget {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

category_theory.right_adjoint G.forget = G.cofree

source

@[simp]

theorem category_theory.comonad.of_left_adjoint_forget {C : Type u₁} [category_theory.category C] (G : category_theory.comonad C) :

category_theory.adjunction.of_left_adjoint G.forget = G.adj

mathlib documentation

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

References #