feat(category_theory/limits): Cone limiting iff terminal. (#10266)

src/category_theory/limits/cone_category.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2021 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+
+import category_theory.limits.preserves.shapes.terminal
+
+/-!
+
+# Limits and the category of (co)cones
+
+This files contains results that stem from the limit API. For the definition and the category
+instance of `cone`, please refer to `category_theory/limits/cones.lean`.
+
+A cone is limiting iff it is terminal in the category of cones. As a corollary, an equivalence of
+categories of cones preserves limiting properties. We also provide the dual.
+
+-/
+
+namespace category_theory.limits
+
+open category_theory
+
+universes v u
+
+variables {J : Type v} [category.{v} J] {J' : Type v} [category.{v} J']
+variables {C : Type u} [category.{v} C] {C' : Type u} [category.{v} C']
+
+/-- A cone is a limit cone iff it is terminal. -/
+def cone.is_limit_equiv_is_terminal {F : J ⥤ C} (c : cone F) : is_limit c ≃ is_terminal c :=
+is_limit.iso_unique_cone_morphism.to_equiv.trans
+{ to_fun := λ h, by exactI is_terminal.of_unique _,
+  inv_fun := λ h s, ⟨⟨is_terminal.from h s⟩, λ a, is_terminal.hom_ext h a _⟩,
+  left_inv := by tidy,
+  right_inv := by tidy }
+
+lemma is_limit.lift_cone_morphism_eq_is_terminal_from {F : J ⥤ C} {c : cone F} (hc : is_limit c)
+  (s : cone F) : hc.lift_cone_morphism s =
+    is_terminal.from (cone.is_limit_equiv_is_terminal _ hc) _ := rfl
+
+lemma is_terminal.from_eq_lift_cone_morphism {F : J ⥤ C} {c : cone F} (hc : is_terminal c)
+  (s : cone F) : is_terminal.from hc s =
+    ((cone.is_limit_equiv_is_terminal _).symm hc).lift_cone_morphism s :=
+by convert (is_limit.lift_cone_morphism_eq_is_terminal_from _ s).symm
+
+/-- If `G : cone F ⥤ cone F'` preserves terminal objects, it preserves limit cones. -/
+def is_limit.of_preserves_cone_terminal {F : J ⥤ C} {F' : J' ⥤ C'} (G : cone F ⥤ cone F')
+  [preserves_limit (functor.empty _) G] {c : cone F} (hc : is_limit c) :
+  is_limit (G.obj c) :=
+(cone.is_limit_equiv_is_terminal _).symm $
+  (cone.is_limit_equiv_is_terminal _ hc).is_terminal_obj _ _
+
+/-- If `G : cone F ⥤ cone F'` reflects terminal objects, it reflects limit cones. -/
+def is_limit.of_reflects_cone_terminal {F : J ⥤ C} {F' : J' ⥤ C'} (G : cone F ⥤ cone F')
+  [reflects_limit (functor.empty _) G] {c : cone F} (hc : is_limit (G.obj c)) :
+  is_limit c :=
+(cone.is_limit_equiv_is_terminal _).symm $
+  (cone.is_limit_equiv_is_terminal _ hc).is_terminal_of_obj _ _
+
+/-- A cocone is a colimit cocone iff it is initial. -/
+def cocone.is_colimit_equiv_is_initial {F : J ⥤ C} (c : cocone F) : is_colimit c ≃ is_initial c :=
+is_colimit.iso_unique_cocone_morphism.to_equiv.trans
+{ to_fun := λ h, by exactI is_initial.of_unique _,
+  inv_fun := λ h s, ⟨⟨is_initial.to h s⟩, λ a, is_initial.hom_ext h a _⟩,
+  left_inv := by tidy,
+  right_inv := by tidy }
+
+lemma is_colimit.desc_cocone_morphism_eq_is_initial_to {F : J ⥤ C} {c : cocone F}
+  (hc : is_colimit c) (s : cocone F) :
+  hc.desc_cocone_morphism s =
+    is_initial.to (cocone.is_colimit_equiv_is_initial _ hc) _ := rfl
+
+lemma is_initial.to_eq_desc_cocone_morphism {F : J ⥤ C} {c : cocone F}
+  (hc : is_initial c) (s : cocone F) :
+  is_initial.to hc s = ((cocone.is_colimit_equiv_is_initial _).symm hc).desc_cocone_morphism s :=
+by convert (is_colimit.desc_cocone_morphism_eq_is_initial_to _ s).symm
+
+/-- If `G : cocone F ⥤ cocone F'` preserves initial objects, it preserves colimit cocones. -/
+def is_colimit.of_preserves_cocone_initial {F : J ⥤ C} {F' : J' ⥤ C'} (G : cocone F ⥤ cocone F')
+  [preserves_colimit (functor.empty _) G] {c : cocone F} (hc : is_colimit c) :
+  is_colimit (G.obj c) :=
+(cocone.is_colimit_equiv_is_initial _).symm $
+  (cocone.is_colimit_equiv_is_initial _ hc).is_initial_obj _ _
+
+/-- If `G : cocone F ⥤ cocone F'` reflects initial objects, it reflects colimit cocones. -/
+def is_colimit.of_reflects_cocone_initial {F : J ⥤ C} {F' : J' ⥤ C'} (G : cocone F ⥤ cocone F')
+  [reflects_colimit (functor.empty _) G] {c : cocone F} (hc : is_colimit (G.obj c)) :
+  is_colimit c :=
+(cocone.is_colimit_equiv_is_initial _).symm $
+  (cocone.is_colimit_equiv_is_initial _ hc).is_initial_of_obj _ _
+
+end category_theory.limits

src/category_theory/limits/preserves/shapes/terminal.lean

@@ -30,6 +30,8 @@ namespace category_theory.limits
 
 variables (X : C)
 
+section terminal
+
 /--
 The map of an empty cone is a limit iff the mapped object is terminal.
 -/
@@ -39,12 +41,12 @@ def is_limit_map_cone_empty_cone_equiv :
   (is_limit.equiv_iso_limit (cones.ext (iso.refl _) (by tidy)))
 
 /-- The property of preserving terminal objects expressed in terms of `is_terminal`. -/
-def is_terminal_obj_of_is_terminal [preserves_limit (functor.empty C) G]
+def is_terminal.is_terminal_obj [preserves_limit (functor.empty C) G]
   (l : is_terminal X) : is_terminal (G.obj X) :=
 is_limit_map_cone_empty_cone_equiv G X (preserves_limit.preserves l)
 
 /-- The property of reflecting terminal objects expressed in terms of `is_terminal`. -/
-def is_terminal_of_is_terminal_obj [reflects_limit (functor.empty C) G]
+def is_terminal.is_terminal_of_obj [reflects_limit (functor.empty C) G]
   (l : is_terminal (G.obj X)) : is_terminal X :=
 reflects_limit.reflects ((is_limit_map_cone_empty_cone_equiv G X).symm l)
 
@@ -55,7 +57,7 @@ object is terminal.
 -/
 def is_limit_of_has_terminal_of_preserves_limit [preserves_limit (functor.empty C) G] :
   is_terminal (G.obj (⊤_ C)) :=
-is_terminal_obj_of_is_terminal G (⊤_ C) terminal_is_terminal
+terminal_is_terminal.is_terminal_obj G (⊤_ C)
 
 /--
 If `C` has a terminal object and `G` preserves terminal objects, then `D` has a terminal object
@@ -100,7 +102,9 @@ preserves_terminal_of_is_iso G f.hom
 
 variables [preserves_limit (functor.empty C) G]
 
-/-- If `G` preserves terminal objects, then the terminal comparison map for `G` an isomorphism. -/
+/--
+If `G` preserves terminal objects, then the terminal comparison map for `G` is an isomorphism.
+-/
 def preserves_terminal.iso : G.obj (⊤_ C) ≅ ⊤_ D :=
 (is_limit_of_has_terminal_of_preserves_limit G).cone_point_unique_up_to_iso (limit.is_limit _)
 
@@ -114,4 +118,95 @@ begin
   apply_instance,
 end
 
+end terminal
+
+section initial
+
+/--
+The map of an empty cocone is a colimit iff the mapped object is initial.
+-/
+def is_colimit_map_cocone_empty_cocone_equiv :
+  is_colimit (G.map_cocone (as_empty_cocone X)) ≃ is_initial (G.obj X) :=
+(is_colimit.precompose_hom_equiv (functor.empty_ext _ _) _).symm.trans
+  (is_colimit.equiv_iso_colimit (cocones.ext (iso.refl _) (by tidy)))
+
+/-- The property of preserving initial objects expressed in terms of `is_initial`. -/
+def is_initial.is_initial_obj [preserves_colimit (functor.empty C) G]
+  (l : is_initial X) : is_initial (G.obj X) :=
+is_colimit_map_cocone_empty_cocone_equiv G X (preserves_colimit.preserves l)
+
+/-- The property of reflecting initial objects expressed in terms of `is_initial`. -/
+def is_initial.is_initial_of_obj [reflects_colimit (functor.empty C) G]
+  (l : is_initial (G.obj X)) : is_initial X :=
+reflects_colimit.reflects ((is_colimit_map_cocone_empty_cocone_equiv G X).symm l)
+
+variables [has_initial C]
+/--
+If `G` preserves the initial object and `C` has a initial object, then the image of the initial
+object is initial.
+-/
+def is_colimit_of_has_initial_of_preserves_colimit [preserves_colimit (functor.empty C) G] :
+  is_initial (G.obj (⊥_ C)) :=
+initial_is_initial.is_initial_obj G (⊥_ C)
+
+/--
+If `C` has a initial object and `G` preserves initial objects, then `D` has a initial object
+also.
+Note this property is somewhat unique to colimits of the empty diagram: for general `J`, if `C`
+has colimits of shape `J` and `G` preserves them, then `D` does not necessarily have colimits of
+shape `J`.
+-/
+lemma has_initial_of_has_initial_of_preserves_colimit [preserves_colimit (functor.empty C) G] :
+  has_initial D :=
+⟨λ F,
+begin
+  haveI := has_colimit.mk ⟨_, is_colimit_of_has_initial_of_preserves_colimit G⟩,
+  apply has_colimit_of_iso F.unique_from_empty,
+end⟩
+
+variable [has_initial D]
+/--
+If the initial comparison map for `G` is an isomorphism, then `G` preserves initial objects.
+-/
+def preserves_initial.of_iso_comparison
+  [i : is_iso (initial_comparison G)] : preserves_colimit (functor.empty C) G :=
+begin
+  apply preserves_colimit_of_preserves_colimit_cocone initial_is_initial,
+  apply (is_colimit_map_cocone_empty_cocone_equiv _ _).symm _,
+  apply is_colimit.of_point_iso (colimit.is_colimit (functor.empty D)),
+  apply i,
+end
+
+/-- If there is any isomorphism `⊥ ⟶ G.obj ⊥`, then `G` preserves initial objects. -/
+def preserves_initial_of_is_iso
+  (f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : is_iso f] : preserves_colimit (functor.empty C) G :=
+begin
+  rw subsingleton.elim f (initial_comparison G) at i,
+  exactI preserves_initial.of_iso_comparison G,
+end
+
+/-- If there is any isomorphism `⊥ ≅ G.obj ⊥ `, then `G` preserves initial objects. -/
+def preserves_initial_of_iso
+  (f : ⊥_ D ≅ G.obj (⊥_ C)) : preserves_colimit (functor.empty C) G :=
+preserves_initial_of_is_iso G f.hom
+
+variables [preserves_colimit (functor.empty C) G]
+
+/-- If `G` preserves initial objects, then the initial comparison map for `G` is an isomorphism. -/
+def preserves_initial.iso : G.obj (⊥_ C) ≅ ⊥_ D :=
+(is_colimit_of_has_initial_of_preserves_colimit G).cocone_point_unique_up_to_iso
+  (colimit.is_colimit _)
+
+@[simp]
+lemma preserves_initial.iso_hom : (preserves_initial.iso G).inv = initial_comparison G :=
+rfl
+
+instance : is_iso (initial_comparison G) :=
+begin
+  rw ← preserves_initial.iso_hom,
+  apply_instance,
+end
+
+end initial
+
 end category_theory.limits