chore(category_theory/monad): comonadic adjunction (#5770)

Defines comonadic adjunctions dual to what's already there



Co-authored-by: Oliver Nash <oliver.nash@gmail.com>
Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com>
Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: tb65536 <tb65536@uw.edu>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mohamed Al-Fahim <malfahim8@gmail.com>
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

src/category_theory/monad/adjunction.lean

@@ -12,7 +12,7 @@ open category
 universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
 
 variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
-variables (R : D ⥤ C)
+variables (L : C ⥤ D) (R : D ⥤ C)
 
 namespace adjunction
 
@@ -23,6 +23,13 @@ instance monad (R : D ⥤ C) [is_right_adjoint R] : monad (left_adjoint R ⋙ R)
   assoc' := λ X, by { dsimp, rw [←R.map_comp], simp },
   right_unit' := λ X, by { dsimp, rw [←R.map_comp], simp } }
 
+@[simps]
+instance comonad (L : C ⥤ D) [is_left_adjoint L] : comonad (right_adjoint L ⋙ L) :=
+{ ε := (of_left_adjoint L).counit,
+  δ := whisker_right (whisker_left (right_adjoint L) (of_left_adjoint L).unit) L,
+  coassoc' := λ X, by { dsimp, rw ← L.map_comp, simp },
+  right_counit' := λ X, by { dsimp, rw ← L.map_comp, simp } }
+
 end adjunction
 
 namespace monad
@@ -54,16 +61,53 @@ def comparison_forget [is_right_adjoint R] : comparison R ⋙ forget (left_adjoi
 
 end monad
 
-/-- A right adjoint functor `R : D ⥤ C` is *monadic* if the comparison function `monad.comparison R` from `D` to the
-category of Eilenberg-Moore algebras for the adjunction is an equivalence. -/
+namespace comonad
+
+/--
+Gven any adjunction `L ⊣ R`, there is a comparison functor `category_theory.comonad.comparison L`
+sending objects `X : C` to Eilenberg-Moore coalgebras for `L ⋙ R` with underlying object 
+`L.obj X`.
+-/
+@[simps]
+def comparison [is_left_adjoint L] : C ⥤ coalgebra (right_adjoint L ⋙ L) :=
+{ obj := λ X,
+  { A := L.obj X,
+    a := L.map ((adjunction.of_left_adjoint L).unit.app X),
+    coassoc' := by { dsimp, rw [← L.map_comp, ← adjunction.unit_naturality, L.map_comp], refl } },
+  map := λ X Y f,
+  { f := L.map f,
+    h' := by { dsimp, rw ← L.map_comp, simp } } }
+
+/--
+The underlying object of `(comonad.comparison L).obj X` is just `L.obj X`.
+-/
+@[simps]
+def comparison_forget [is_left_adjoint L] : comparison L ⋙ forget (right_adjoint L ⋙ L) ≅ L :=
+{ hom := { app := λ X, 𝟙 _, },
+  inv := { app := λ X, 𝟙 _, } }
+
+end comonad
+
+/--
+A right adjoint functor `R : D ⥤ C` is *monadic* if the comparison functor `monad.comparison R`
+from `D` to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.
+-/
 class monadic_right_adjoint (R : D ⥤ C) extends is_right_adjoint R :=
 (eqv : is_equivalence (monad.comparison R))
 
+/--
+A left adjoint functor `L : C ⥤ D` is *comonadic* if the comparison functor `comonad.comparison L`
+from `C` to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.
+-/
+class comonadic_left_adjoint (L : C ⥤ D) extends is_left_adjoint L :=
+(eqv : is_equivalence (comonad.comparison L))
+
 -- TODO: This holds more generally for idempotent adjunctions, not just reflective adjunctions.
 instance μ_iso_of_reflective [reflective R] : is_iso (μ_ (left_adjoint R ⋙ R)) :=
 by { dsimp [adjunction.monad], apply_instance }
 
 attribute [instance] monadic_right_adjoint.eqv
+attribute [instance] comonadic_left_adjoint.eqv
 
 namespace reflective