feat(category_theory): comonads and coalgebras (#2134)

* Comonads and coalgebras

* Update docstring

* add docstrings

* Update src/category_theory/monad/algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/category_theory/monad/algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Update src/category_theory/monad/algebra.lean

Co-Authored-By: Johan Commelin <johan@commelin.net>

* make the linter happy

* revert change to nolints

* disable inhabited instance linter

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

scripts/nolints.txt

@@ -736,13 +736,6 @@ apply_nolint category_theory.monad.comparison_forget doc_blame
 -- category_theory/monad/algebra.lean
 apply_nolint category_theory.monad.algebra has_inhabited_instance
 apply_nolint category_theory.monad.algebra.hom doc_blame has_inhabited_instance
-apply_nolint category_theory.monad.algebra.hom.comp doc_blame
-apply_nolint category_theory.monad.algebra.hom.id doc_blame
-apply_nolint category_theory.monad.forget doc_blame
-apply_nolint category_theory.monad.free doc_blame
-
--- category_theory/monad/basic.lean
-apply_nolint category_theory.monad doc_blame
 
 -- category_theory/monad/limits.lean
 apply_nolint category_theory.has_limits_of_reflective doc_blame

src/category_theory/monad/algebra.lean

@@ -1,17 +1,18 @@
 /-
 Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Bhavik Mehta
 -/
 import category_theory.monad.basic
 import category_theory.adjunction.basic
 
 /-!
-# Eilenberg-Moore algebras for a monad
+# Eilenberg-Moore (co)algebras for a (co)monad
 
-This file defines Eilenberg-Moore algebras for a monad, and provides the category instance for them.
+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.
+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]
@@ -41,6 +42,7 @@ restate_axiom algebra.assoc'
 namespace algebra
 variables {T : C ⥤ C} [monad.{v₁} T]
 
+/-- A morphism of Eilenberg–Moore algebras for the monad `T`. -/
 @[ext] structure hom (A B : algebra T) :=
 (f : A.A ⟶ B.A)
 (h' : T.map f ≫ B.a = A.a ≫ f . obviously)
@@ -50,9 +52,11 @@ attribute [simp] hom.h
 
 namespace hom
 
+/-- The identity homomorphism for an Eilenberg–Moore algebra. -/
 @[simps] def id (A : algebra T) : hom A A :=
 { f := 𝟙 A.A }
 
+/-- Composition of Eilenberg–Moore algebra homomorphisms. -/
 @[simps] def comp {P Q R : algebra T} (f : hom P Q) (g : hom Q R) : hom P R :=
 { f := f.f ≫ g.f,
   h' := by rw [functor.map_comp, category.assoc, g.h, ←category.assoc, f.h, category.assoc] }
@@ -70,10 +74,12 @@ end algebra
 
 variables (T : C ⥤ C) [monad.{v₁} T]
 
+/-- The forgetful functor from the Eilenberg-Moore category, forgetting the algebraic structure. -/
 @[simps] def forget : algebra T ⥤ C :=
 { obj := λ A, A.A,
   map := λ A B f, f.f }
 
+/-- The free functor from the Eilenberg-Moore category, constructing an algebra for any object. -/
 @[simps] def free : C ⥤ algebra T :=
 { obj := λ X,
   { A := T.obj X,
@@ -112,4 +118,94 @@ adjunction.mk_of_hom_equiv
 
 end monad
 
+namespace comonad
+
+/-- An Eilenberg-Moore coalgebra for a comonad `T`. -/
+@[nolint has_inhabited_instance]
+structure coalgebra (G : C ⥤ C) [comonad.{v₁} G] : Type (max u₁ v₁) :=
+(A : C)
+(a : A ⟶ G.obj A)
+(counit' : a ≫ (ε_ G).app A = 𝟙 A . obviously)
+(coassoc' : (a ≫ (δ_ G).app A) = (a ≫ G.map a) . obviously)
+
+restate_axiom coalgebra.counit'
+restate_axiom coalgebra.coassoc'
+
+namespace coalgebra
+variables {G : C ⥤ C} [comonad.{v₁} G]
+
+/-- A morphism of Eilenberg-Moore coalgebras for the comonad `G`. -/
+@[ext, nolint has_inhabited_instance] structure hom (A B : coalgebra G) :=
+(f : A.A ⟶ B.A)
+(h' : A.a ≫ G.map f = f ≫ B.a . obviously)
+
+restate_axiom hom.h'
+attribute [simp] hom.h
+
+namespace hom
+
+/-- The identity homomorphism for an Eilenberg–Moore coalgebra. -/
+@[simps] def id (A : coalgebra G) : hom A A :=
+{ f := 𝟙 A.A }
+
+/-- Composition of Eilenberg–Moore coalgebra homomorphisms. -/
+@[simps] def comp {P Q R : coalgebra G} (f : hom P Q) (g : hom Q R) : hom P R :=
+{ f := f.f ≫ g.f,
+  h' := by rw [functor.map_comp, ← category.assoc, f.h, category.assoc, g.h, category.assoc] }
+
+end hom
+
+/-- The category of Eilenberg-Moore coalgebras for a comonad. -/
+@[simps] instance EilenbergMoore : category (coalgebra G) :=
+{ hom := hom,
+  id := hom.id,
+  comp := @hom.comp _ _ _ _ }
+
+end coalgebra
+
+variables (G : C ⥤ C) [comonad.{v₁} G]
+
+/-- The forgetful functor from the Eilenberg-Moore category, forgetting the coalgebraic structure. -/
+@[simps] def forget : coalgebra G ⥤ C :=
+{ obj := λ A, A.A,
+  map := λ A B f, f.f }
+
+/-- The cofree functor from the Eilenberg-Moore category, constructing a coalgebra for any object. -/
+@[simps] def cofree : C ⥤ coalgebra G :=
+{ obj := λ X,
+  { A := G.obj X,
+    a := (δ_ G).app X,
+    coassoc' := (comonad.coassoc G _).symm },
+  map := λ X Y f,
+  { f := G.map f,
+    h' := by erw (δ_ G).naturality; refl} }
+
+/--
+The adjunction between the cofree and forgetful constructions for Eilenberg-Moore coalgebras
+for a comonad.
+-/
+def adj : forget G ⊣ cofree G :=
+adjunction.mk_of_hom_equiv
+{ hom_equiv := λ X Y,
+  { to_fun := λ f,
+    { f := X.a ≫ G.map f,
+      h' := by { rw [functor.map_comp, ← category.assoc, ← coalgebra.coassoc], simp } },
+    inv_fun := λ g, g.f ≫ (ε_ G).app Y,
+    left_inv := λ f,
+    begin
+      dsimp,
+      rw [category.assoc, (ε_ G).naturality,
+          functor.id_map, ← category.assoc, X.counit, id_comp],
+    end,
+    right_inv := λ g,
+    begin
+      ext1, dsimp,
+      rw [functor.map_comp, ← category.assoc, coalgebra.hom.h, assoc,
+          cofree_obj_a, comonad.right_counit],
+      dsimp, simp
+    end
+    }}
+
+end comonad
+
 end category_theory

src/category_theory/monad/basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Bhavik Mehta
 -/
 import category_theory.functor_category
 
@@ -13,6 +13,13 @@ universes v₁ u₁ -- declare the `v`'s first; see `category_theory.category` f
 variables {C : Type u₁} [𝒞 : category.{v₁} C]
 include 𝒞
 
+/--
+The data of a monad on C consists of an endofunctor T together with natural transformations
+η : 𝟭 C ⟶ T and μ : T ⋙ T ⟶ T satisfying three equations:
+- T μ_X ≫ μ_X = μ_(TX) ≫ μ_X (associativity)
+- η_(TX) ≫ μ_X = 1_X (left unit)
+- Tη_X ≫ μ_X = 1_X (right unit)
+-/
 class monad (T : C ⥤ C) :=
 (η : 𝟭 _ ⟶ T)
 (μ : T ⋙ T ⟶ T)
@@ -28,4 +35,26 @@ attribute [simp] monad.left_unit monad.right_unit
 notation `η_` := monad.η
 notation `μ_` := monad.μ
 
+/--
+The data of a comonad on C consists of an endofunctor G together with natural transformations
+ε : G ⟶ 𝟭 C and δ : G ⟶ G ⋙ G satisfying three equations:
+- δ_X ≫ G δ_X = δ_X ≫ δ_(GX) (coassociativity)
+- δ_X ≫ ε_(GX) = 1_X (left counit)
+- δ_X ≫ G ε_X = 1_X (right counit)
+-/
+class comonad (G : C ⥤ C) :=
+(ε : G ⟶ 𝟭 _)
+(δ : G ⟶ (G ⋙ G))
+(coassoc' : ∀ X : C, nat_trans.app δ _ ≫ G.map (δ.app X) = δ.app _ ≫ δ.app _ . obviously)
+(left_counit' : ∀ X : C, δ.app X ≫ ε.app (G.obj X) = 𝟙 _ . obviously)
+(right_counit' : ∀ X : C, δ.app X ≫ G.map (ε.app X) = 𝟙 _ . obviously)
+
+restate_axiom comonad.coassoc'
+restate_axiom comonad.left_counit'
+restate_axiom comonad.right_counit'
+attribute [simp] comonad.left_counit comonad.right_counit
+
+notation `ε_` := comonad.ε
+notation `δ_` := comonad.δ
+
 end category_theory