feat(category_theory/limits): has_limit F ↔ has_terminal (cone F) (#1…

…5797)

This will be used to show that `C` has limits of shape `J` if and only if `const J` has a right adjoint.

src/category_theory/limits/cone_category.lean

@@ -35,6 +35,10 @@ is_limit.iso_unique_cone_morphism.to_equiv.trans
   left_inv := by tidy,
   right_inv := by tidy }
 
+lemma has_limit_iff_has_terminal_cone (F : J ⥤ C) : has_limit F ↔ has_terminal (cone F) :=
+⟨λ h, by exactI (cone.is_limit_equiv_is_terminal _ (limit.is_limit F)).has_terminal,
+ λ h, ⟨⟨by exactI ⟨⊤_ _, (cone.is_limit_equiv_is_terminal _).symm terminal_is_terminal⟩⟩⟩⟩
+
 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
@@ -66,6 +70,10 @@ is_colimit.iso_unique_cocone_morphism.to_equiv.trans
   left_inv := by tidy,
   right_inv := by tidy }
 
+lemma has_colimit_iff_has_initial_cocone (F : J ⥤ C) : has_colimit F ↔ has_initial (cocone F) :=
+⟨λ h, by exactI (cocone.is_colimit_equiv_is_initial _ (colimit.is_colimit F)).has_initial,
+ λ h, ⟨⟨by exactI ⟨⊥_ _, (cocone.is_colimit_equiv_is_initial _).symm initial_is_initial⟩⟩⟩⟩
+
 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 =

src/category_theory/limits/shapes/terminal.lean

@@ -235,11 +235,18 @@ and showing there is a unique morphism to it from any other object. -/
 lemma has_terminal_of_unique (X : C) [h : Π Y : C, unique (Y ⟶ X)] : has_terminal C :=
 { has_limit := λ F, has_limit.mk ⟨_, (is_terminal_equiv_unique F X).inv_fun h⟩ }
 
+lemma is_terminal.has_terminal {X : C} (h : is_terminal X) : has_terminal C :=
+{ has_limit := λ F, has_limit.mk ⟨⟨X, by tidy⟩, is_limit_change_empty_cone _ h _ (iso.refl _)⟩ }
+
 /-- We can more explicitly show that a category has an initial object by specifying the object,
 and showing there is a unique morphism from it to any other object. -/
 lemma has_initial_of_unique (X : C) [h : Π Y : C, unique (X ⟶ Y)] : has_initial C :=
 { has_colimit := λ F, has_colimit.mk ⟨_, (is_initial_equiv_unique F X).inv_fun h⟩ }
 
+lemma is_initial.has_initial {X : C} (h : is_initial X) : has_initial C :=
+{ has_colimit := λ F, has_colimit.mk
+    ⟨⟨X, by tidy⟩, is_colimit_change_empty_cocone _ h _ (iso.refl _)⟩ }
+
 /-- The map from an object to the terminal object. -/
 abbreviation terminal.from [has_terminal C] (P : C) : P ⟶ ⊤_ C :=
 limit.lift (functor.empty C) (as_empty_cone P)