chore(category_theory/limits): some limit lemmas (#4238)

A couple of lemmas characterising definitions which are already there (the first part of #4163)

Author: b-mehta

src/category_theory/limits/limits.lean

@@ -95,6 +95,16 @@ namespace is_limit
 instance subsingleton {t : cone F} : subsingleton (is_limit t) :=
 ⟨by intros P Q; cases P; cases Q; congr; ext; solve_by_elim⟩
 
+/-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cone point
+of any cone over `F` to the cone point of a limit cone over `G`. -/
+def map {F G : J ⥤ C} (s : cone F) {t : cone G} (P : is_limit t)
+  (α : F ⟶ G) : s.X ⟶ t.X :=
+P.lift ((cones.postcompose α).obj s)
+
+@[simp, reassoc] lemma map_π {F G : J ⥤ C} (c : cone F) {d : cone G} (hd : is_limit d)
+  (α : F ⟶ G) (j : J) : hd.map c α ≫ d.π.app j = c.π.app j ≫ α.app j :=
+fac _ _ _
+
 /- Repackaging the definition in terms of cone morphisms. -/
 
 /-- The universal morphism from any other cone to a limit cone. -/
@@ -136,7 +146,6 @@ def hom_is_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) (f : s ⟶ t) :
   inv_hom_id' := Q.uniq_cone_morphism, }
 
 /-- Limits of `F` are unique up to isomorphism. -/
--- We may later want to prove the coherence of these isomorphisms.
 def cone_point_unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s.X ≅ t.X :=
 (cones.forget F).map_iso (unique_up_to_iso P Q)
 
@@ -148,12 +157,38 @@ def cone_point_unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t)
   (Q : is_limit t) (j : J) : (cone_point_unique_up_to_iso P Q).inv ≫ s.π.app j = t.π.app j :=
 (unique_up_to_iso P Q).inv.w _
 
+@[simp, reassoc] lemma lift_comp_cone_point_unique_up_to_iso_hom {r s t : cone F}
+  (P : is_limit s) (Q : is_limit t) :
+  P.lift r ≫ (cone_point_unique_up_to_iso P Q).hom = Q.lift r :=
+Q.uniq _ _ (by simp)
+
+@[simp, reassoc] lemma lift_comp_cone_point_unique_up_to_iso_inv {r s t : cone F}
+  (P : is_limit s) (Q : is_limit t) :
+  Q.lift r ≫ (cone_point_unique_up_to_iso P Q).inv = P.lift r :=
+P.uniq _ _ (by simp)
+
 /-- Transport evidence that a cone is a limit cone across an isomorphism of cones. -/
 def of_iso_limit {r t : cone F} (P : is_limit r) (i : r ≅ t) : is_limit t :=
 is_limit.mk_cone_morphism
   (λ s, P.lift_cone_morphism s ≫ i.hom)
   (λ s m, by rw ←i.comp_inv_eq; apply P.uniq_cone_morphism)
 
+@[simp] lemma of_iso_limit_lift {r t : cone F} (P : is_limit r) (i : r ≅ t) (s) :
+  (P.of_iso_limit i).lift s = P.lift s ≫ i.hom.hom :=
+rfl
+
+/-- Isomorphism of cones preserves whether or not they are limiting cones. -/
+def equiv_iso_limit {r t : cone F} (i : r ≅ t) : is_limit r ≃ is_limit t :=
+{ to_fun := λ h, h.of_iso_limit i,
+  inv_fun := λ h, h.of_iso_limit i.symm,
+  left_inv := by tidy,
+  right_inv := by tidy }
+
+@[simp] lemma equiv_iso_limit_apply {r t : cone F} (i : r ≅ t) (P : is_limit r) :
+  equiv_iso_limit i P = P.of_iso_limit i := rfl
+@[simp] lemma equiv_iso_limit_symm_apply {r t : cone F} (i : r ≅ t) (P : is_limit t) :
+  (equiv_iso_limit i).symm P = P.of_iso_limit i.symm := rfl
+
 /--
 If the canonical morphism from a cone point to a limiting cone point is an iso, then the
 first cone was limiting also.
@@ -224,10 +259,28 @@ are themselves isomorphic.
 @[simps]
 def cone_points_iso_of_nat_iso {F G : J ⥤ C} {s : cone F} {t : cone G}
   (P : is_limit s) (Q : is_limit t) (w : F ≅ G) : s.X ≅ t.X :=
-{ hom := Q.lift ((limits.cones.postcompose w.hom).obj s),
-  inv := P.lift ((limits.cones.postcompose w.inv).obj t),
-  hom_inv_id' := by { apply hom_ext P, tidy, },
-  inv_hom_id' := by { apply hom_ext Q, tidy, }, }
+{ hom := Q.map s w.hom,
+  inv := P.map t w.inv,
+  hom_inv_id' := P.hom_ext (by tidy),
+  inv_hom_id' := Q.hom_ext (by tidy), }
+
+@[reassoc]
+lemma cone_points_iso_of_nat_iso_hom_comp {F G : J ⥤ C} {s : cone F} {t : cone G}
+  (P : is_limit s) (Q : is_limit t) (w : F ≅ G) (j : J) :
+  (cone_points_iso_of_nat_iso P Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j :=
+by simp
+
+@[reassoc]
+lemma cone_points_iso_of_nat_iso_inv_comp {F G : J ⥤ C} {s : cone F} {t : cone G}
+  (P : is_limit s) (Q : is_limit t) (w : F ≅ G) (j : J) :
+  (cone_points_iso_of_nat_iso P Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j :=
+by simp
+
+@[reassoc]
+lemma lift_comp_cone_points_iso_of_nat_iso_hom {F G : J ⥤ C} {r s : cone F} {t : cone G}
+  (P : is_limit s) (Q : is_limit t) (w : F ≅ G) :
+  P.lift r ≫ (cone_points_iso_of_nat_iso P Q w).hom = Q.map r w.hom :=
+Q.hom_ext (by simp)
 
 section equivalence
 open category_theory.equivalence
@@ -318,25 +371,21 @@ If `F` and `G` are naturally isomorphic, then `F.map_cone c` being a limit impli
 -/
 def map_cone_equiv {D : Type u'} [category.{v} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G) {c : cone K}
   (t : is_limit (F.map_cone c)) : is_limit (G.map_cone c) :=
-{ lift := λ s, t.lift ((cones.postcompose (iso_whisker_left K h).inv).obj s) ≫ h.hom.app c.X,
+{ lift := λ s, t.map s (iso_whisker_left K h).inv ≫ h.hom.app c.X,
   fac' := λ s j,
   begin
-    slice_lhs 2 3 {erw ← h.hom.naturality (c.π.app j)},
-    slice_lhs 1 2 {erw t.fac ((cones.postcompose (iso_whisker_left K h).inv).obj s) j},
+    erw [assoc, ← h.hom.naturality (c.π.app j), t.map_π_assoc s (iso_whisker_left K h).inv j],
     dsimp,
-    slice_lhs 2 3 {rw iso.inv_hom_id_app},
-    rw category.comp_id,
+    simp,
   end,
   uniq' := λ s m J,
   begin
     rw ← cancel_mono (h.inv.app c.X),
     apply t.hom_ext,
     intro j,
-    dsimp,
-    slice_lhs 2 3 {erw ← h.inv.naturality (c.π.app j)},
-    slice_lhs 1 2 {erw J j},
-    conv_rhs {congr, rw [category.assoc, iso.hom_inv_id_app, comp_id]},
-    apply (t.fac ((cones.postcompose (iso_whisker_left K h).inv).obj s) j).symm
+    rw [assoc, assoc, assoc, h.hom_inv_id_app_assoc],
+    erw [← h.inv.naturality (c.π.app j), reassoc_of (J j)],
+    apply (t.map_π s (iso_whisker_left K h).inv j).symm,
   end }
 
 /--
@@ -452,6 +501,17 @@ namespace is_colimit
 instance subsingleton {t : cocone F} : subsingleton (is_colimit t) :=
 ⟨by intros P Q; cases P; cases Q; congr; ext; solve_by_elim⟩
 
+/-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cocone point
+of a colimit cocone over `F` to the cocone point of any cocone over `G`. -/
+def map {F G : J ⥤ C} {s : cocone F} (P : is_colimit s) (t : cocone G)
+  (α : F ⟶ G) : s.X ⟶ t.X :=
+P.desc ((cocones.precompose α).obj t)
+
+@[simp, reassoc]
+lemma ι_map {F G : J ⥤ C} {c : cocone F} (hc : is_colimit c) (d : cocone G) (α : F ⟶ G)
+  (j : J) : c.ι.app j ≫ is_colimit.map hc d α = α.app j ≫ d.ι.app j :=
+fac _ _ _
+
 /- Repackaging the definition in terms of cocone morphisms. -/
 
 /-- The universal morphism from a colimit cocone to any other cocone. -/
@@ -493,7 +553,6 @@ def hom_is_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) (f : s ⟶
   inv_hom_id' := Q.uniq_cocone_morphism, }
 
 /-- Colimits of `F` are unique up to isomorphism. -/
--- We may later want to prove the coherence of these isomorphisms.
 def cocone_point_unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) : s.X ≅ t.X :=
 (cocones.forget F).map_iso (unique_up_to_iso P Q)
 
@@ -505,12 +564,36 @@ def cocone_point_unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_co
   (Q : is_colimit t) (j : J) : t.ι.app j ≫ (cocone_point_unique_up_to_iso P Q).inv = s.ι.app j :=
 (unique_up_to_iso P Q).inv.w _
 
+@[simp, reassoc] lemma cocone_point_unique_up_to_iso_hom_desc {r s t : cocone F} (P : is_colimit s)
+  (Q : is_colimit t) : (cocone_point_unique_up_to_iso P Q).hom ≫ Q.desc r = P.desc r :=
+P.uniq _ _ (by simp)
+
+@[simp, reassoc] lemma cocone_point_unique_up_to_iso_inv_desc {r s t : cocone F} (P : is_colimit s)
+  (Q : is_colimit t) : (cocone_point_unique_up_to_iso P Q).inv ≫ P.desc r = Q.desc r :=
+Q.uniq _ _ (by simp)
+
 /-- Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones. -/
 def of_iso_colimit {r t : cocone F} (P : is_colimit r) (i : r ≅ t) : is_colimit t :=
 is_colimit.mk_cocone_morphism
   (λ s, i.inv ≫ P.desc_cocone_morphism s)
   (λ s m, by rw i.eq_inv_comp; apply P.uniq_cocone_morphism)
 
+@[simp] lemma of_iso_colimit_desc {r t : cocone F} (P : is_colimit r) (i : r ≅ t) (s) :
+  (P.of_iso_colimit i).desc s = i.inv.hom ≫ P.desc s :=
+rfl
+
+/-- Isomorphism of cocones preserves whether or not they are colimiting cocones. -/
+def equiv_iso_colimit {r t : cocone F} (i : r ≅ t) : is_colimit r ≃ is_colimit t :=
+{ to_fun := λ h, h.of_iso_colimit i,
+  inv_fun := λ h, h.of_iso_colimit i.symm,
+  left_inv := by tidy,
+  right_inv := by tidy }
+
+@[simp] lemma equiv_iso_colimit_apply {r t : cocone F} (i : r ≅ t) (P : is_colimit r) :
+  equiv_iso_colimit i P = P.of_iso_colimit i := rfl
+@[simp] lemma equiv_iso_colimit_symm_apply {r t : cocone F} (i : r ≅ t) (P : is_colimit t) :
+  (equiv_iso_colimit i).symm P = P.of_iso_colimit i.symm := rfl
+
 /--
 If the canonical morphism to a cocone point from a colimiting cocone point is an iso, then the
 first cocone was colimiting also.
@@ -596,10 +679,28 @@ are themselves isomorphic.
 @[simps]
 def cocone_points_iso_of_nat_iso {F G : J ⥤ C} {s : cocone F} {t : cocone G}
   (P : is_colimit s) (Q : is_colimit t) (w : F ≅ G) : s.X ≅ t.X :=
-{ hom := P.desc ((limits.cocones.precompose w.hom).obj t),
-  inv := Q.desc ((limits.cocones.precompose w.inv).obj s),
-  hom_inv_id' := by { apply hom_ext P, tidy, },
-  inv_hom_id' := by { apply hom_ext Q, tidy, }, }
+{ hom := P.map t w.hom,
+  inv := Q.map s w.inv,
+  hom_inv_id' := P.hom_ext (by tidy),
+  inv_hom_id' := Q.hom_ext (by tidy) }
+
+@[reassoc]
+lemma comp_cocone_points_iso_of_nat_iso_hom {F G : J ⥤ C} {s : cocone F} {t : cocone G}
+  (P : is_colimit s) (Q : is_colimit t) (w : F ≅ G) (j : J) :
+  s.ι.app j ≫ (cocone_points_iso_of_nat_iso P Q w).hom = w.hom.app j ≫ t.ι.app j :=
+by simp
+
+@[reassoc]
+lemma comp_cocone_points_iso_of_nat_iso_inv {F G : J ⥤ C} {s : cocone F} {t : cocone G}
+  (P : is_colimit s) (Q : is_colimit t) (w : F ≅ G) (j : J) :
+  t.ι.app j ≫ (cocone_points_iso_of_nat_iso P Q w).inv = w.inv.app j ≫ s.ι.app j :=
+by simp
+
+@[reassoc]
+lemma cocone_points_iso_of_nat_iso_hom_desc {F G : J ⥤ C} {s : cocone F} {r t : cocone G}
+  (P : is_colimit s) (Q : is_colimit t) (w : F ≅ G) :
+  (cocone_points_iso_of_nat_iso P Q w).hom ≫ Q.desc r = P.map _ w.hom :=
+P.hom_ext (by simp)
 
 section equivalence
 open category_theory.equivalence
@@ -853,9 +954,23 @@ def limit.lift (F : J ⥤ C) [has_limit F] (c : cone F) : c.X ⟶ limit F :=
   limit.lift F c ≫ limit.π F j = c.π.app j :=
 is_limit.fac _ c j
 
+/--
+Functoriality of limits.
+
+Usually this morphism should be accessed through `lim.map`,
+but may be needed separately when you have specified limits for the source and target functors,
+but not necessarily for all functors of shape `J`.
+-/
+def lim_map {F G : J ⥤ C} [has_limit F] [has_limit G] (α : F ⟶ G) : limit F ⟶ limit G :=
+is_limit.map _ (limit.is_limit G) α
+
+@[simp, reassoc] lemma lim_map_π {F G : J ⥤ C} [has_limit F] [has_limit G] (α : F ⟶ G) (j : J) :
+  lim_map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
+limit.lift_π _ j
+
 /-- The cone morphism from any cone to the arbitrary choice of limit cone. -/
 def limit.cone_morphism {F : J ⥤ C} [has_limit F] (c : cone F) :
-  c ⟶ (limit.cone F) :=
+  c ⟶ limit.cone F :=
 (limit.is_limit F).lift_cone_morphism c
 
 @[simp] lemma limit.cone_morphism_hom {F : J ⥤ C} [has_limit F] (c : cone F) :
@@ -964,7 +1079,13 @@ is_limit.cone_points_iso_of_nat_iso (limit.is_limit F) (limit.is_limit G) w
 lemma has_limit.iso_of_nat_iso_hom_π {F G : J ⥤ C} [has_limit F] [has_limit G]
   (w : F ≅ G) (j : J) :
   (has_limit.iso_of_nat_iso w).hom ≫ limit.π G j = limit.π F j ≫ w.hom.app j :=
-by simp [has_limit.iso_of_nat_iso, is_limit.cone_points_iso_of_nat_iso_hom]
+is_limit.cone_points_iso_of_nat_iso_hom_comp _ _ _ _
+
+@[simp, reassoc]
+lemma has_limit.lift_iso_of_nat_iso_hom {F G : J ⥤ C} [has_limit F] [has_limit G] (t : cone F)
+  (w : F ≅ G) :
+  limit.lift F t ≫ (has_limit.iso_of_nat_iso w).hom = limit.lift G ((cones.postcompose w.hom).obj _) :=
+is_limit.lift_comp_cone_points_iso_of_nat_iso_hom _ _ _
 
 /--
 The limits of `F : J ⥤ C` and `G : K ⥤ C` are isomorphic,
@@ -1088,29 +1209,6 @@ end
 
 section lim_functor
 
-/-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cone point
-of any cone over `F` to the cone point of a limit cone over `G`. -/
-def is_limit.map {F G : J ⥤ C} (s : cone F) {t : cone G} (P : is_limit t)
-  (α : F ⟶ G) : s.X ⟶ t.X :=
-P.lift ((cones.postcompose α).obj s)
-
-@[simp, reassoc] lemma is_limit_map_π {F G : J ⥤ C} (c : cone F) {d : cone G} (hd : is_limit d)
-  (α : F ⟶ G) (j : J) : is_limit.map c hd α ≫ d.π.app j = c.π.app j ≫ α.app j :=
-by apply is_limit.fac
-
-/--
-Functoriality of limits.
-
-Usually this morphism should be accessed through `lim.map`,
-but may be needed separately when you have specified limits for the source and target functors,
-but not necessarily for all functors of shape `J`.
--/
-def lim_map {F G : J ⥤ C} [has_limit F] [has_limit G] (α : F ⟶ G) : limit F ⟶ limit G :=
-is_limit.map _ (limit.is_limit G) α
-
-@[simp, reassoc] lemma lim_map_π {F G : J ⥤ C} [has_limit F] [has_limit G] (α : F ⟶ G) (j : J) :
-  lim_map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
-by apply is_limit.fac
 
 variables [has_limits_of_shape J C]
 
@@ -1269,6 +1367,21 @@ We thus use `reassoc` to define additional `@[simp]` lemmas, with an arbitrary e
   colimit.ι F j ≫ colimit.desc F c = c.ι.app j :=
 is_colimit.fac _ c j
 
+/--
+Functoriality of colimits.
+
+Usually this morphism should be accessed through `colim.map`,
+but may be needed separately when you have specified colimits for the source and target functors,
+but not necessarily for all functors of shape `J`.
+-/
+def colim_map {F G : J ⥤ C} [has_colimit F] [has_colimit G] (α : F ⟶ G) : colimit F ⟶ colimit G :=
+is_colimit.map (colimit.is_colimit F) _ α
+
+@[simp, reassoc]
+lemma ι_colim_map {F G : J ⥤ C} [has_colimit F] [has_colimit G] (α : F ⟶ G) (j : J) :
+  colimit.ι F j ≫ colim_map α = α.app j ≫ colimit.ι G j :=
+colimit.ι_desc _ j
+
 /-- The cocone morphism from the arbitrary choice of colimit cocone to any cocone. -/
 def colimit.cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) :
   (colimit.cocone F) ⟶ c :=
@@ -1383,7 +1496,13 @@ is_colimit.cocone_points_iso_of_nat_iso (colimit.is_colimit F) (colimit.is_colim
 lemma has_colimit.iso_of_nat_iso_ι_hom {F G : J ⥤ C} [has_colimit F] [has_colimit G]
   (w : F ≅ G) (j : J) :
   colimit.ι F j ≫ (has_colimit.iso_of_nat_iso w).hom = w.hom.app j ≫ colimit.ι G j :=
-by simp [has_colimit.iso_of_nat_iso, is_colimit.cocone_points_iso_of_nat_iso_inv]
+is_colimit.comp_cocone_points_iso_of_nat_iso_hom _ _ _ _
+
+@[simp, reassoc]
+lemma has_colimit.iso_of_nat_iso_hom_desc {F G : J ⥤ C} [has_colimit F] [has_colimit G] (t : cocone G)
+  (w : F ≅ G) :
+  (has_colimit.iso_of_nat_iso w).hom ≫ colimit.desc G t = colimit.desc F ((cocones.precompose w.hom).obj _) :=
+is_colimit.cocone_points_iso_of_nat_iso_hom_desc _ _ _
 
 /--
 The colimits of `F : J ⥤ C` and `G : K ⥤ C` are isomorphic,
@@ -1517,31 +1636,6 @@ end
 
 section colim_functor
 
-/-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cocone point
-of a colimit cocone over `F` to the cocone point of any cocone over `G`. -/
-def is_colimit.map {F G : J ⥤ C} {s : cocone F} (P : is_colimit s) (t : cocone G)
-  (α : F ⟶ G) : s.X ⟶ t.X :=
-P.desc ((cocones.precompose α).obj t)
-
-@[simp, reassoc]
-lemma ι_is_colimit_map {F G : J ⥤ C} {c : cocone F} (hc : is_colimit c) (d : cocone G) (α : F ⟶ G)
-  (j : J) : c.ι.app j ≫ is_colimit.map hc d α = α.app j ≫ d.ι.app j :=
-by apply is_colimit.fac
-
-/--
-Functoriality of colimits.
-
-Usually this morphism should be accessed through `colim.map`,
-but may be needed separately when you have specified colimits for the source and target functors,
-but not necessarily for all functors of shape `J`.
--/
-def colim_map {F G : J ⥤ C} [has_colimit F] [has_colimit G] (α : F ⟶ G) : colimit F ⟶ colimit G :=
-is_colimit.map (colimit.is_colimit F) _ α
-
-@[simp, reassoc]
-lemma ι_colim_map {F G : J ⥤ C} [has_colimit F] [has_colimit G] (α : F ⟶ G) (j : J) :
-  colimit.ι F j ≫ colim_map α = α.app j ≫ colimit.ι G j :=
-by apply is_colimit.fac
 
 variables [has_colimits_of_shape J C]
 

src/category_theory/limits/preserves/shapes.lean

@@ -57,9 +57,9 @@ lemma preserves_products_iso_hom_π
   (preserves_products_iso G f).hom ≫ pi.π _ j = G.map (pi.π f j) :=
 begin
   dsimp [preserves_products_iso, preserves_limits_iso, has_limit.iso_of_nat_iso, cones.postcompose,
-    is_limit.unique_up_to_iso, is_limit.lift_cone_morphism],
+         is_limit.unique_up_to_iso, is_limit.lift_cone_morphism, is_limit.map],
   simp only [limit.lift_π, discrete.nat_iso_hom_app, limit.cone_π, limit.lift_π_assoc,
-    nat_trans.comp_app, category.assoc, functor.map_cone_π],
+             nat_trans.comp_app, category.assoc, functor.map_cone_π, is_limit.map_π],
   dsimp, simp, -- See note [dsimp, simp],
 end