feat(category_theory/monad/limits): forgetful creates colimits (#2138)

* forgetful creates colimits

* tidy up proofs

* add docs

* suggestions from review

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: b-mehta

src/category_theory/monad/limits.lean

@@ -62,7 +62,8 @@ variables (D : J ⥤ algebra T) [has_limit.{v₁} (D ⋙ forget T)]
 end forget_creates_limits
 
 -- Theorem 5.6.5 from [Riehl][riehl2017]
-def forget_creates_limits (D : J ⥤ algebra T) [has_limit.{v₁} (D ⋙ forget T)] : has_limit D :=
+/-- The forgetful functor from the Eilenberg-Moore category creates limits. -/
+def forget_creates_limits (D : J ⥤ algebra T) [has_limit (D ⋙ forget T)] : has_limit D :=
 { cone :=
   { X := forget_creates_limits.cone_point D,
     π :=
@@ -82,6 +83,118 @@ def forget_creates_limits (D : J ⥤ algebra T) [has_limit.{v₁} (D ⋙ forget
       end },
     uniq' := λ s m w, by { ext1, ext1, simpa using congr_arg algebra.hom.f (w j) } } }
 
+namespace forget_creates_colimits
+-- Let's hide the implementation details in a namespace
+variables (D : J ⥤ algebra T)
+-- We have a diagram D of shape J in the category of algebras, and we assume that its image
+-- D ⋙ forget T under the forgetful functor has a colimit (written L).
+
+-- We'll construct a colimiting coalgebra for D, whose carrier will also be L.
+-- To do this, we must find a map TL ⟶ L. Since T preserves colimits, TL is also a colimit.
+-- In particular, it is a colimit for the diagram `(D ⋙ forget T) ⋙ T`
+-- so to construct a map TL ⟶ L it suffices to show that L is the apex of a cocone for this diagram.
+-- In other words, we need a natural transformation from const L to `(D ⋙ forget T) ⋙ T`.
+-- But we already know that L is the apex of a cocone for the diagram `D ⋙ forget T`, so it
+-- suffices to give a natural transformation `((D ⋙ forget T) ⋙ T) ⟶ (D ⋙ forget T)`:
+
+/--
+The natural transformation given by the algebra structure maps, used to construct a cocone `c` with
+apex `colimit (D ⋙ forget T)`.
+ -/
+@[simps] def γ : ((D ⋙ forget T) ⋙ T) ⟶ (D ⋙ forget T) := { app := λ j, (D.obj j).a }
+
+variable [has_colimit.{v₁} (D ⋙ forget T)]
+/--
+A cocone for the diagram `(D ⋙ forget T) ⋙ T` found by composing the natural transformation `γ`
+with the colimiting cocone for `D ⋙ forget T`.
+-/
+@[simps]
+def c : cocone ((D ⋙ forget T) ⋙ T) :=
+{ X := colimit (D ⋙ forget T),
+  ι := γ D ≫ (colimit.cocone (D ⋙ forget T)).ι }
+
+variable [preserves_colimits_of_shape J T]
+
+/--
+Define the map `λ : TL ⟶ L`, which will serve as the structure of the coalgebra on `L`, and
+we will show is the colimiting object. We use the cocone constructed by `c` and the fact that
+`T` preserves colimits to produce this morphism.
+-/
+@[reducible]
+def lambda : (functor.map_cocone T (colimit.cocone (D ⋙ forget T))).X ⟶ colimit (D ⋙ forget T) :=
+(preserves_colimit.preserves T (colimit.is_colimit (D ⋙ forget T))).desc (c D)
+
+/-- The key property defining the map `λ : TL ⟶ L`. -/
+lemma commuting (j : J) :
+T.map (colimit.ι (D ⋙ forget T) j) ≫ lambda D = (D.obj j).a ≫ colimit.ι (D ⋙ forget T) j :=
+is_colimit.fac (preserves_colimit.preserves T (colimit.is_colimit (D ⋙ forget T))) (c D) j
+
+/--
+Construct the colimiting algebra from the map `λ : TL ⟶ L` given by `lambda`. We are required to
+show it satisfies the two algebra laws, which follow from the algebra laws for the image of `D` and
+our `commuting` lemma.
+-/
+@[simps] def cocone_point :
+algebra T :=
+{ A := colimit (D ⋙ forget T),
+  a := lambda D,
+  unit' :=
+  begin
+    ext1,
+    erw [comp_id, ← category.assoc, (η_ T).naturality, category.assoc, commuting, ← category.assoc],
+    erw algebra.unit, apply id_comp
+  end,
+  assoc' :=
+  begin
+    apply is_colimit.hom_ext (preserves_colimit.preserves T (preserves_colimit.preserves T (colimit.is_colimit (D ⋙ forget T)))),
+    intro j,
+    erw [← category.assoc, nat_trans.naturality (μ_ T), ← functor.map_cocone_ι, category.assoc,
+         is_colimit.fac _ (c D) j],
+    rw ← category.assoc,
+    erw [← functor.map_comp, commuting],
+    dsimp,
+    erw [← category.assoc, algebra.assoc, category.assoc, functor.map_comp, category.assoc, commuting]
+  end
+}
+
+end forget_creates_colimits
+
+-- TODO: the converse of this is true as well
+-- TODO: generalise to monadic functors, as for creating limits
+/--
+The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit
+which the monad itself preserves.
+
+The colimiting algebra itself has been constructed in `cocone_point`. We now must show it
+actually forms a cocone, and that this is colimiting.
+-/
+def forget_creates_colimits_of_monad_preserves
+  [preserves_colimits_of_shape J T] (D : J ⥤ algebra T) [has_colimit (D ⋙ forget T)] :
+has_colimit D :=
+{ cocone :=
+  { X := forget_creates_colimits.cocone_point D,
+    ι :=
+    { app := λ j, { f := colimit.ι (D ⋙ forget T) j,
+                    h' := forget_creates_colimits.commuting _ _ },
+      naturality' := λ A B f, by { ext1, dsimp, erw [comp_id, colimit.w (D ⋙ forget T)] } } },
+  is_colimit :=
+  { desc := λ s,
+    { f := colimit.desc _ ((forget T).map_cocone s),
+      h' :=
+      begin
+        dsimp,
+        apply is_colimit.hom_ext (preserves_colimit.preserves T (colimit.is_colimit (D ⋙ forget T))),
+        intro j,
+        rw ← category.assoc, erw ← functor.map_comp,
+        erw colimit.ι_desc,
+        rw ← category.assoc, erw forget_creates_colimits.commuting,
+        rw category.assoc, rw colimit.ι_desc,
+        apply algebra.hom.h
+      end },
+    uniq' := λ s m J, by { ext1, ext1, simpa using congr_arg algebra.hom.f (J j) }
+  }
+}
+
 end monad
 
 variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₁} [𝒟 : category.{v₁} D]
@@ -100,6 +213,7 @@ instance comp_comparison_has_limit
   has_limit (F ⋙ monad.comparison R) :=
 monad.forget_creates_limits (F ⋙ monad.comparison R)
 
+/-- Any monadic functor creates limits. -/
 def monadic_creates_limits (F : J ⥤ D) (R : D ⥤ C) [monadic_right_adjoint R] [has_limit.{v₁} (F ⋙ R)] :
   has_limit F :=
 adjunction.has_limit_of_comp_equivalence _ (monad.comparison R)