chore(category_theory/monad/algebra): lint and golf (#8160)

Adds a module docstring and golfs some proofs, including removing `erw`.

src/category_theory/monad/algebra.lean

@@ -48,7 +48,7 @@ variables {T : monad C}
 /-- 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)
+(h' : (T : C ⥤ C).map f ≫ B.a = A.a ≫ f . obviously)
 
 restate_axiom hom.h'
 attribute [simp, reassoc] hom.h
@@ -90,7 +90,8 @@ To construct an isomorphism of algebras, it suffices to give an isomorphism of t
 commutes with the structure morphisms.
 -/
 @[simps]
-def iso_mk {A B : algebra T} (h : A.A ≅ B.A) (w : T.map h.hom ≫ B.a = A.a ≫ h.hom) : A ≅ B :=
+def iso_mk {A B : algebra T} (h : A.A ≅ B.A) (w : (T : C ⥤ C).map h.hom ≫ B.a = A.a ≫ h.hom) :
+  A ≅ B :=
 { hom := { f := h.hom },
   inv :=
   { f := h.inv,
@@ -143,7 +144,7 @@ Given an algebra morphism whose carrier part is an isomorphism, we get an algebr
 -/
 lemma algebra_iso_of_iso {A B : algebra T} (f : A ⟶ B) [is_iso f.f] : is_iso f :=
 ⟨⟨{ f := inv f.f,
-    h' := by { rw [is_iso.eq_comp_inv f.f, category.assoc, ← f.h], dsimp, simp } }, by tidy⟩⟩
+    h' := by { rw [is_iso.eq_comp_inv f.f, category.assoc, ← f.h], simp } }, by tidy⟩⟩
 
 instance forget_reflects_iso : reflects_isomorphisms (forget T) :=
 { reflects := λ A B, algebra_iso_of_iso T }
@@ -229,7 +230,7 @@ namespace comonad
 @[nolint has_inhabited_instance]
 structure coalgebra (G : comonad C) : Type (max u₁ v₁) :=
 (A : C)
-(a : A ⟶ G.obj A)
+(a : A ⟶ (G : C ⥤ C).obj A)
 (counit' : a ≫ G.ε.app A = 𝟙 A . obviously)
 (coassoc' : a ≫ G.δ.app A = a ≫ G.map a . obviously)
 
@@ -243,7 +244,7 @@ variables {G : comonad C}
 /-- 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)
+(h' : A.a ≫ (G : C ⥤ C).map f = f ≫ B.a . obviously)
 
 restate_axiom hom.h'
 attribute [simp, reassoc] hom.h
@@ -283,7 +284,8 @@ To construct an isomorphism of coalgebras, it suffices to give an isomorphism of
 commutes with the structure morphisms.
 -/
 @[simps]
-def iso_mk {A B : coalgebra G} (h : A.A ≅ B.A) (w : A.a ≫ G.map h.hom = h.hom ≫ B.a) : A ≅ B :=
+def iso_mk {A B : coalgebra G} (h : A.A ≅ B.A) (w : A.a ≫ (G : C ⥤ C).map h.hom = h.hom ≫ B.a) :
+  A ≅ B :=
 { hom := { f := h.hom },
   inv :=
   { f := h.inv,
@@ -304,7 +306,7 @@ Given a coalgebra morphism whose carrier part is an isomorphism, we get a coalge
 -/
 lemma coalgebra_iso_of_iso {A B : coalgebra G} (f : A ⟶ B) [is_iso f.f] : is_iso f :=
 ⟨⟨{ f := inv f.f,
-    h' := by { rw [is_iso.eq_inv_comp f.f, ←f.h_assoc], dsimp, simp } }, by tidy⟩⟩
+    h' := by { rw [is_iso.eq_inv_comp f.f, ←f.h_assoc], simp } }, by tidy⟩⟩
 
 instance forget_reflects_iso : reflects_isomorphisms (forget G) :=
 { reflects := λ A B, coalgebra_iso_of_iso G }

src/category_theory/monad/limits.lean

@@ -7,6 +7,20 @@ import category_theory.monad.adjunction
 import category_theory.adjunction.limits
 import category_theory.limits.preserves.shapes.terminal
 
+/-!
+# Limits and colimits in the category of algebras
+
+This file shows that the forgetful functor `forget T : algebra T ⥤ C` for a monad `T : C ⥤ C`
+creates limits and creates any colimits which `T` preserves.
+This is used to show that `algebra T` has any limits which `C` has, and any colimits which `C` has
+and `T` preserves.
+This is generalised to the case of a monadic functor `D ⥤ C`.
+
+## TODO
+
+Dualise for the category of coalgebras and comonadic left adjoints.
+-/
+
 namespace category_theory
 open category
 open category_theory.limits
@@ -22,42 +36,32 @@ variables {J : Type v₁} [small_category J]
 
 namespace forget_creates_limits
 
-variables (D : J ⥤ algebra T) (c : cone (D ⋙ forget T)) (t : is_limit c)
+variables (D : J ⥤ algebra T) (c : cone (D ⋙ T.forget)) (t : is_limit c)
 
 /-- (Impl) The natural transformation used to define the new cone -/
-@[simps] def γ : (D ⋙ forget T ⋙ ↑T) ⟶ (D ⋙ forget T) := { app := λ j, (D.obj j).a }
+@[simps] def γ : (D ⋙ T.forget ⋙ ↑T) ⟶ D ⋙ T.forget := { app := λ j, (D.obj j).a }
 
 /-- (Impl) This new cone is used to construct the algebra structure -/
-@[simps] def new_cone : cone (D ⋙ forget T) :=
+@[simps π_app] def new_cone : cone (D ⋙ forget T) :=
 { X := T.obj c.X,
-  π := (functor.const_comp _ _ ↑T).inv ≫ whisker_right c.π T ≫ (γ D) }
+  π := (functor.const_comp _ _ ↑T).inv ≫ whisker_right c.π T ≫ γ D }
 
 /-- The algebra structure which will be the apex of the new limit cone for `D`. -/
 @[simps] def cone_point : algebra T :=
 { A := c.X,
   a := t.lift (new_cone D c),
-  unit' :=
+  unit' := t.hom_ext $ λ j,
   begin
-    apply t.hom_ext,
-    intro j,
-    erw [category.assoc, t.fac (new_cone D c), id_comp],
-    dsimp,
-    erw [id_comp, ← category.assoc, ← T.η.naturality, functor.id_map, category.assoc,
-         (D.obj j).unit, comp_id],
+    rw [category.assoc, t.fac, new_cone_π_app, ←T.η.naturality_assoc, functor.id_map,
+      (D.obj j).unit],
+    dsimp, simp -- See library note [dsimp, simp]
   end,
-  assoc' :=
+  assoc' := t.hom_ext $ λ j,
   begin
-    apply t.hom_ext,
-    intro j,
-    rw [category.assoc, category.assoc, t.fac (new_cone D c)],
-    dsimp,
-    erw id_comp,
-    slice_lhs 1 2 {rw ← T.μ.naturality},
-    slice_lhs 2 3 {rw (D.obj j).assoc},
-    slice_rhs 1 2 {rw ← (T : C ⥤ C).map_comp},
-    rw t.fac (new_cone D c),
-    dsimp,
-    erw [id_comp, functor.map_comp, category.assoc]
+    rw [category.assoc, category.assoc, t.fac (new_cone D c), new_cone_π_app,
+      ←functor.map_comp_assoc, t.fac (new_cone D c), new_cone_π_app, ←T.μ.naturality_assoc,
+      (D.obj j).assoc, functor.map_comp, category.assoc],
+    refl,
   end }
 
 /-- (Impl) Construct the lifted cone in `algebra T` which will be limiting. -/
@@ -71,24 +75,19 @@ variables (D : J ⥤ algebra T) (c : cone (D ⋙ forget T)) (t : is_limit c)
 def lifted_cone_is_limit : is_limit (lifted_cone D c t) :=
 { lift := λ s,
   { f := t.lift ((forget T).map_cone s),
-    h' :=
+    h' := t.hom_ext $ λ j,
     begin
-      apply t.hom_ext, intro j,
-      slice_rhs 2 3 {rw t.fac ((forget T).map_cone s) j},
-      dsimp,
-      slice_lhs 2 3 {rw t.fac (new_cone D c) j},
       dsimp,
-      rw category.id_comp,
-      slice_lhs 1 2 {rw ← (T : C ⥤ C).map_comp},
-      rw t.fac ((forget T).map_cone s) j,
-      exact (s.π.app j).h
+      rw [category.assoc, category.assoc, t.fac, new_cone_π_app, ←functor.map_comp_assoc, t.fac,
+        functor.map_cone_π_app],
+      apply (s.π.app j).h,
     end },
   uniq' := λ s m J,
   begin
     ext1,
     apply t.hom_ext,
     intro j,
-    simpa [t.fac (functor.map_cone (forget T) s) j] using congr_arg algebra.hom.f (J j),
+    simpa [t.fac ((forget T).map_cone s) j] using congr_arg algebra.hom.f (J j),
   end }
 
 end forget_creates_limits
@@ -152,12 +151,12 @@ we will show is the colimiting object. We use the cocone constructed by `c` and
 -/
 @[reducible]
 def lambda : ((T : C ⥤ C).map_cocone c).X ⟶ c.X :=
-(preserves_colimit.preserves t).desc (new_cocone c)
+(is_colimit_of_preserves _ t).desc (new_cocone c)
 
 /-- (Impl) The key property defining the map `λ : TL ⟶ L`. -/
 lemma commuting (j : J) :
-T.map (c.ι.app j) ≫ lambda c t = (D.obj j).a ≫ c.ι.app j :=
-is_colimit.fac (preserves_colimit.preserves t) (new_cocone c) j
+(T : C ⥤ C).map (c.ι.app j) ≫ lambda c t = (D.obj j).a ≫ c.ι.app j :=
+(is_colimit_of_preserves _ t).fac (new_cocone c) j
 
 variables [preserves_colimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)]
 
@@ -175,45 +174,35 @@ algebra T :=
   begin
     apply t.hom_ext,
     intro j,
-    erw [comp_id, ← category.assoc, T.η.naturality, category.assoc, commuting, ← category.assoc],
-    erw algebra.unit, apply id_comp
+    rw [(show c.ι.app j ≫ T.η.app c.X ≫ _ = T.η.app (D.obj j).A ≫ _ ≫ _,
+                  from T.η.naturality_assoc _ _), commuting, algebra.unit_assoc (D.obj j)],
+    dsimp, simp -- See library note [dsimp, simp]
   end,
   assoc' :=
   begin
-    apply is_colimit.hom_ext (preserves_colimit.preserves (preserves_colimit.preserves t)),
-    intro j,
-    erw [← category.assoc, T.μ.naturality, ← functor.map_cocone_ι_app, category.assoc,
-         is_colimit.fac _ (new_cocone c) j],
-    rw ← category.assoc,
-    erw [← functor.map_comp, commuting],
-    dsimp,
-    erw [← category.assoc, algebra.assoc, category.assoc, functor.map_comp, category.assoc,
-      commuting],
-    apply_instance, apply_instance
+    refine (is_colimit_of_preserves _ (is_colimit_of_preserves _ t)).hom_ext (λ j, _),
+    rw [functor.map_cocone_ι_app, functor.map_cocone_ι_app,
+      (show (T : C ⥤ C).map ((T : C ⥤ C).map _) ≫ _ ≫ _ = _, from T.μ.naturality_assoc _ _),
+      ←functor.map_comp_assoc, commuting, functor.map_comp, category.assoc, commuting],
+    apply (D.obj j).assoc_assoc _,
   end }
 
 /-- (Impl) Construct the lifted cocone in `algebra T` which will be colimiting. -/
 @[simps] def lifted_cocone : cocone D :=
 { X := cocone_point c t,
   ι := { app := λ j, { f := c.ι.app j, h' := commuting _ _ _ },
-         naturality' := λ A B f, by { ext1, dsimp, erw [comp_id, c.w] } } }
+         naturality' := λ A B f, by { ext1, dsimp, rw [comp_id], apply c.w } } }
 
 /-- (Impl) Prove that the lifted cocone is colimiting. -/
 @[simps]
 def lifted_cocone_is_colimit : is_colimit (lifted_cocone c t) :=
 { desc := λ s,
   { f := t.desc ((forget T).map_cocone s),
-    h' :=
+    h' := (is_colimit_of_preserves (T : C ⥤ C) t).hom_ext $ λ j,
     begin
       dsimp,
-      apply is_colimit.hom_ext (preserves_colimit.preserves t),
-      intro j,
-      rw ← category.assoc, erw ← functor.map_comp,
-      erw t.fac',
-      rw ← category.assoc, erw forget_creates_colimits.commuting,
-      rw category.assoc, rw t.fac',
+      rw [←functor.map_comp_assoc, ←category.assoc, t.fac, commuting, category.assoc, t.fac],
       apply algebra.hom.h,
-      apply_instance
     end },
   uniq' := λ s m J,
   by { ext1, apply t.hom_ext, intro j, simpa using congr_arg algebra.hom.f (J j) } }