lint(category_theory/monad): doc-strings (#4428)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/monad/adjunction.lean

@@ -33,6 +33,13 @@ end adjunction
 
 namespace monad
 
+/--
+Gven any adjunction `L ⊣ R`, there is a comparison functor `category_theory.monad.comparison R`
+sending objects `Y : D` to Eilenberg-Moore algebras for `L ⋙ R` with underlying object `R.obj X`.
+
+We later show that this is full when `R` is full, faithful when `R` is faithful,
+and essentially surjective when `R` is reflective.
+-/
 -- We can't use `@[simps]` here because it can't cope with `let` statements.
 def comparison [is_right_adjoint R] : D ⥤ algebra ((left_adjoint R) ⋙ R) :=
 let h : _ ⊣ R := is_right_adjoint.adj in
@@ -49,6 +56,9 @@ let h : _ ⊣ R := is_right_adjoint.adj in
 @[simp] lemma comparison_obj_a [is_right_adjoint R] (X) :
   ((comparison R).obj X).a = R.map (is_right_adjoint.adj.counit.app X) := rfl
 
+/--
+The underlying object of `(monad.comparison R).obj X` is just `R.obj X`.
+-/
 def comparison_forget [is_right_adjoint R] : comparison R ⋙ forget ((left_adjoint R) ⋙ R) ≅ R :=
 { hom := { app := λ X, 𝟙 _, },
   inv := { app := λ X, 𝟙 _, } }
@@ -97,7 +107,7 @@ let h : L ⊣ R := (is_right_adjoint.adj) in
     refl
   end }
 
-instance comparison_ess_surj [reflective R]: ess_surj (monad.comparison R) :=
+instance comparison_ess_surj [reflective R] : ess_surj (monad.comparison R) :=
 let L := left_adjoint R in
 let h : L ⊣ R := is_right_adjoint.adj in
 { obj_preimage := λ X, L.obj X.A,

src/category_theory/monad/algebra.lean

@@ -10,7 +10,9 @@ import category_theory.reflects_isomorphisms
 /-!
 # 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.
+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.
@@ -56,6 +58,8 @@ namespace hom
 @[simps] def id (A : algebra T) : hom A A :=
 { f := 𝟙 A.A }
 
+instance (A : algebra T) : inhabited (hom A A) := ⟨{ f := 𝟙 _ }⟩
+
 /-- 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,
@@ -89,6 +93,9 @@ variables (T : C ⥤ C) [monad T]
   { f := T.map f,
     h' := by erw (μ_ T).naturality } }
 
+instance [inhabited C] : inhabited (algebra T) :=
+⟨(free T).obj (default C)⟩
+
 /-- The adjunction between the free and forgetful constructions for Eilenberg-Moore algebras for a monad.
     cf Lemma 5.2.8 of [Riehl][riehl2017]. -/
 def adj : free T ⊣ forget T :=
@@ -223,7 +230,7 @@ adjunction.mk_of_hom_equiv
       dsimp, simp
     end
     }}
-    
+
 instance forget_faithful : faithful (forget G) := {}
 
 end comonad