feat(category_theory/limits/concrete): simp lemmas (#3973)

Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element.

This isn't exhaustive; just the things I've wanted recently.



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

src/algebra/category/Group/limits.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import algebra.category.Mon.limits
 import algebra.category.Group.preadditive
 import category_theory.over
+import category_theory.limits.concrete_category
 import category_theory.limits.shapes.concrete_category
 
 /-!
@@ -209,14 +210,6 @@ end CommGroup
 
 namespace AddCommGroup
 
--- PROJECT:
--- it would be nice if this were available just by virtue of `forget AddCommGroup`
--- preserving limits.
-@[simp]
-lemma lift_π_apply (F : J ⥤ AddCommGroup) (s : cone F) (j : J) (x : s.X) :
-  limit.π F j (limit.lift F s x) = s.π.app j x :=
-congr_fun (congr_arg (λ f : s.X ⟶ F.obj j, (f : s.X → F.obj j)) (limit.lift_π s j)) x
-
 /--
 The categorical kernel of a morphism in `AddCommGroup`
 agrees with the usual group-theoretical kernel.

src/category_theory/concrete_category/basic.lean

@@ -18,8 +18,8 @@ forgetful functor.
 Each concrete category `C` comes with a canonical faithful functor
 `forget C : C ⥤ Type*`.  We say that a concrete category `C` admits a
 *forgetful functor* to a concrete category `D`, if it has a functor
-`forget₂ C D : C ⥤ D` such that `(forget₂ C D) ⋙ (forget D) = forget
-C`, see `class has_forget₂`.  Due to `faithful.div_comp`, it suffices
+`forget₂ C D : C ⥤ D` such that `(forget₂ C D) ⋙ (forget D) = forget C`,
+see `class has_forget₂`.  Due to `faithful.div_comp`, it suffices
 to verify that `forget₂.obj` and `forget₂.map` agree with the equality
 above; then `forget₂` will satisfy the functor laws automatically, see
 `has_forget₂.mk'`.
@@ -34,15 +34,23 @@ See [Ahrens and Lumsdaine, *Displayed Categories*][ahrens2017] for
 related work.
 -/
 
-universes u v v'
+universes w v v' u
 
 namespace category_theory
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
-/-- A concrete category is a category `C` with a fixed faithful functor `forget : C ⥤ Type`. -/
-class concrete_category (C : Type v) [category C] :=
-(forget [] : C ⥤ Type u)
+/--
+A concrete category is a category `C` with a fixed faithful functor `forget : C ⥤ Type`.
+
+Note that `concrete_category` potentially depends on three independent universe levels,
+* the universe level `w` appearing in `forget : C ⥤ Type w`
+* the universe level `v` of the morphisms (i.e. we have a `category.{v} C`)
+* the universe level `u` of the objects (i.e `C : Type u`)
+They are specified that order, to avoid unnecessary universe annotations.
+-/
+class concrete_category (C : Type u) [category.{v} C] :=
+(forget [] : C ⥤ Type w)
 [forget_faithful : faithful forget]
 end prio
 

src/category_theory/limits/concrete_category.lean

@@ -3,51 +3,102 @@ Copyright (c) 2017 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.limits.cones
+import category_theory.limits.limits
 import category_theory.concrete_category.basic
 
 /-!
-# Facts about limits of functors into concrete categories
+# Facts about (co)limits of functors into concrete categories
 -/
 
-universes u
+universes w v u
 
 open category_theory
 
 namespace category_theory.limits
 
-variables {C : Type (u+1)} [large_category C] [concrete_category C]
+variables {J : Type v} [small_category J]
+variables {C : Type u} [category.{v} C] [concrete_category.{v} C]
 
 local attribute [instance] concrete_category.has_coe_to_sort
 local attribute [instance] concrete_category.has_coe_to_fun
 
 -- We now prove a lemma about naturality of cones over functors into bundled categories.
 namespace cone
 
-variables {J : Type u} [small_category J]
-
 /-- Naturality of a cone over functors to a concrete category. -/
-@[simp] lemma naturality_concrete {G : J ⥤ C} (s : cone G) {j j' : J} (f : j ⟶ j') (x : s.X) :
-   (G.map f) ((s.π.app j) x) = (s.π.app j') x :=
+@[simp] lemma w_apply {F : J ⥤ C} (s : cone F) {j j' : J} (f : j ⟶ j') (x : s.X) :
+   F.map f (s.π.app j x) = s.π.app j' x :=
 begin
-  convert congr_fun (congr_arg (λ k : s.X ⟶ G.obj j', (k : s.X → G.obj j')) (s.π.naturality f).symm) x;
-  { dsimp, simp [-cone.w] },
+  convert congr_fun (congr_arg (λ k : s.X ⟶ F.obj j', (k : s.X → F.obj j')) (s.w f)) x,
+  simp only [coe_comp],
 end
 
+@[simp]
+lemma w_forget_apply (F : J ⥤ C) (s : cone (F ⋙ forget C)) {j j' : J} (f : j ⟶ j') (x : s.X) :
+  F.map f (s.π.app j x) = s.π.app j' x :=
+congr_fun (s.w f : _) x
+
 end cone
 
 namespace cocone
 
-variables {J : Type u} [small_category J]
-
 /-- Naturality of a cocone over functors into a concrete category. -/
-@[simp] lemma naturality_concrete {G : J ⥤ C} (s : cocone G) {j j' : J} (f : j ⟶ j') (x : G.obj j) :
-  (s.ι.app j') ((G.map f) x) = (s.ι.app j) x :=
+@[simp] lemma w_apply {F : J ⥤ C} (s : cocone F) {j j' : J} (f : j ⟶ j') (x : F.obj j) :
+  s.ι.app j' (F.map f x) = s.ι.app j x :=
 begin
-  convert congr_fun (congr_arg (λ k : G.obj j ⟶ s.X, (k : G.obj j → s.X)) (s.ι.naturality f)) x;
-  { dsimp, simp [-nat_trans.naturality, -cocone.w] },
+  convert congr_fun (congr_arg (λ k : F.obj j ⟶ s.X, (k : F.obj j → s.X)) (s.w f)) x,
+  simp only [coe_comp],
 end
 
+@[simp]
+lemma w_forget_apply (F : J ⥤ C) (s : cocone (F ⋙ forget C)) {j j' : J} (f : j ⟶ j') (x : F.obj j) :
+  s.ι.app j' (F.map f x) = (s.ι.app j x : s.X) :=
+congr_fun (s.w f : _) x
+
 end cocone
 
+section has_limit
+
+@[simp]
+lemma limit.lift_π_apply (F : J ⥤ C) [has_limit F] (s : cone F) (j : J) (x : s.X) :
+  limit.π F j (limit.lift F s x) = s.π.app j x :=
+begin
+  have w := congr_arg (λ f : s.X ⟶ F.obj j, (f : s.X → F.obj j) x) (limit.lift_π s j),
+  dsimp at w,
+  rwa coe_comp at w,
+end
+
+@[simp]
+lemma limit.w_apply (F : J ⥤ C) [has_limit F] {j j' : J} (f : j ⟶ j') (x : limit F) :
+  F.map f (limit.π F j x) = limit.π F j' x :=
+begin
+  have w := congr_arg (λ f : limit F ⟶ F.obj j', (f : limit F → F.obj j') x) (limit.w F f),
+  dsimp at w,
+  rwa coe_comp at w,
+end
+
+end has_limit
+
+section has_colimit
+
+@[simp]
+lemma colimit.ι_desc_apply (F : J ⥤ C) [has_colimit F] (s : cocone F) (j : J) (x : F.obj j) :
+  colimit.desc F s (colimit.ι F j x) = s.ι.app j x :=
+begin
+  have w := congr_arg (λ f : F.obj j ⟶ s.X, (f : F.obj j → s.X) x) (colimit.ι_desc s j),
+  dsimp at w,
+  rwa coe_comp at w,
+end
+
+@[simp]
+lemma colimit.w_apply (F : J ⥤ C) [has_colimit F] {j j' : J} (f : j ⟶ j') (x : F.obj j) :
+  colimit.ι F j' (F.map f x) = colimit.ι F j x :=
+begin
+  have w := congr_arg (λ f : F.obj j ⟶ colimit F, (f : F.obj j → colimit F) x) (colimit.w F f),
+  dsimp at w,
+  rwa coe_comp at w,
+end
+
+end has_colimit
+
 end category_theory.limits