feat(category_theory/limits/shapes/terminal): is_terminal object (#3957)

Add language to talk about when an object is terminal, and generalise some results to use this

Author: b-mehta

src/category_theory/closed/cartesian.lean

@@ -240,33 +240,33 @@ def internal_hom [cartesian_closed C] : C ⥤ Cᵒᵖ ⥤ C :=
   map_id' := λ X, by { ext, apply functor.map_id },
   map_comp' := λ X Y Z f g, by { ext, apply functor.map_comp } }
 
-/-- If an initial object `0` exists in a CCC, then `A ⨯ 0 ≅ 0`. -/
+/-- If an initial object `I` exists in a CCC, then `A ⨯ I ≅ I`. -/
 @[simps]
-def zero_mul [has_initial C] : A ⨯ ⊥_ C ≅ ⊥_ C :=
+def zero_mul {I : C} (t : is_initial I) : A ⨯ I ≅ I :=
 { hom := limits.prod.snd,
-  inv := default (⊥_ C ⟶ A ⨯ ⊥_ C),
+  inv := t.to _,
   hom_inv_id' :=
   begin
-    have: (limits.prod.snd : A ⨯ ⊥_ C ⟶ ⊥_ C) = uncurry (default _),
+    have: (limits.prod.snd : A ⨯ I ⟶ I) = uncurry (t.to _),
       rw ← curry_eq_iff,
-      apply subsingleton.elim,
+      apply t.hom_ext,
     rw [this, ← uncurry_natural_right, ← eq_curry_iff],
-    apply subsingleton.elim
+    apply t.hom_ext,
   end,
-  }
+  inv_hom_id' := t.hom_ext _ _ }
 
 /-- If an initial object `0` exists in a CCC, then `0 ⨯ A ≅ 0`. -/
-def mul_zero [has_initial C] : ⊥_ C ⨯ A ≅ ⊥_ C :=
-limits.prod.braiding _ _ ≪≫ zero_mul
+def mul_zero {I : C} (t : is_initial I) : I ⨯ A ≅ I :=
+limits.prod.braiding _ _ ≪≫ zero_mul t
 
 /-- If an initial object `0` exists in a CCC then `0^B ≅ 1` for any `B`. -/
-def pow_zero [has_initial C] [cartesian_closed C] : ⊥_C ⟹ B ≅ ⊤_ C :=
+def pow_zero {I : C} (t : is_initial I) [cartesian_closed C] : I ⟹ B ≅ ⊤_ C :=
 { hom := default _,
-  inv := curry (mul_zero.hom ≫ default (⊥_ C ⟶ B)),
+  inv := curry ((mul_zero t).hom ≫ t.to _),
   hom_inv_id' :=
   begin
-    rw [← curry_natural_left, curry_eq_iff, ← cancel_epi mul_zero.inv],
-    { apply subsingleton.elim },
+    rw [← curry_natural_left, curry_eq_iff, ← cancel_epi (mul_zero t).inv],
+    { apply t.hom_ext },
     { apply_instance },
     { apply_instance }
   end }
@@ -293,20 +293,28 @@ def prod_coprod_distrib [has_binary_coproducts C] [cartesian_closed C] (X Y Z :
   end }
 
 /--
-If an initial object `0` exists in a CCC then it is a strict initial object,
-i.e. any morphism to `0` is an iso.
+If an initial object `I` exists in a CCC then it is a strict initial object,
+i.e. any morphism to `I` is an iso.
+This actually shows a slightly stronger version: any morphism to an initial object from an
+exponentiable object is an isomorphism.
 -/
-instance strict_initial [has_initial C] {f : A ⟶ ⊥_ C} : is_iso f :=
+def strict_initial {I : C} (t : is_initial I) (f : A ⟶ I) : is_iso f :=
 begin
-  haveI : mono (limits.prod.lift (𝟙 A) f ≫ zero_mul.hom) := mono_comp _ _,
+  haveI : mono (limits.prod.lift (𝟙 A) f ≫ (zero_mul t).hom) := mono_comp _ _,
   rw [zero_mul_hom, prod.lift_snd] at _inst,
-  haveI: split_epi f := ⟨default _, subsingleton.elim _ _⟩,
+  haveI: split_epi f := ⟨t.to _, t.hom_ext _ _⟩,
   apply is_iso_of_mono_of_split_epi
 end
 
+instance [has_initial C] (f : A ⟶ ⊥_ C) : is_iso f :=
+strict_initial initial_is_initial _
+
 /-- If an initial object `0` exists in a CCC then every morphism from it is monic. -/
-instance initial_mono (B : C) [has_initial C] [cartesian_closed C] : mono (initial.to B) :=
-⟨λ B g h _, eq_of_inv_eq_inv (subsingleton.elim (inv g) (inv h))⟩
+lemma initial_mono {I : C} (B : C) (t : is_initial I) [cartesian_closed C] : mono (t.to B) :=
+⟨λ B g h _, by { haveI := strict_initial t g, haveI := strict_initial t h, exact eq_of_inv_eq_inv (t.hom_ext _ _) }⟩
+
+instance initial.mono_to [has_initial C] (B : C) [cartesian_closed C] : mono (initial.to B) :=
+initial_mono B initial_is_initial
 
 variables {D : Type u₂} [category.{v} D]
 section functor

src/category_theory/limits/shapes/terminal.lean

@@ -16,7 +16,43 @@ open category_theory
 
 namespace category_theory.limits
 
-variables (C : Type u) [category.{v} C]
+variables {C : Type u} [category.{v} C]
+
+/-- Construct a cone for the empty diagram given an object. -/
+def as_empty_cone (X : C) : cone (functor.empty C) := { X := X, π := by tidy }
+/-- Construct a cocone for the empty diagram given an object. -/
+def as_empty_cocone (X : C) : cocone (functor.empty C) := { X := X, ι := by tidy }
+
+/-- `X` is terminal if the cone it induces on the empty diagram is limiting. -/
+abbreviation is_terminal (X : C) := is_limit (as_empty_cone X)
+/-- `X` is initial if the cocone it induces on the empty diagram is colimiting. -/
+abbreviation is_initial (X : C) := is_colimit (as_empty_cocone X)
+
+/-- Give the morphism to a terminal object from any other. -/
+def is_terminal.from {X : C} (t : is_terminal X) (Y : C) : Y ⟶ X :=
+t.lift (as_empty_cone Y)
+
+/-- Any two morphisms to a terminal object are equal. -/
+lemma is_terminal.hom_ext {X Y : C} (t : is_terminal X) (f g : Y ⟶ X) : f = g :=
+t.hom_ext (by tidy)
+
+/-- Give the morphism from an initial object to any other. -/
+def is_initial.to {X : C} (t : is_initial X) (Y : C) : X ⟶ Y :=
+t.desc (as_empty_cocone Y)
+
+/-- Any two morphisms from an initial object are equal. -/
+lemma is_initial.hom_ext {X Y : C} (t : is_initial X) (f g : X ⟶ Y) : f = g :=
+t.hom_ext (by tidy)
+
+/-- Any morphism from a terminal object is mono. -/
+lemma is_terminal.mono_from {X Y : C} (t : is_terminal X) (f : X ⟶ Y) : mono f :=
+⟨λ Z g h eq, t.hom_ext _ _⟩
+
+/-- Any morphism to an initial object is epi. -/
+lemma is_initial.epi_to {X Y : C} (t : is_initial X) (f : Y ⟶ X) : epi f :=
+⟨λ Z g h eq, t.hom_ext _ _⟩
+
+variable (C)
 
 /--
 A category has a terminal object if it has a limit over the empty diagram.
@@ -64,10 +100,10 @@ def has_initial_of_unique (X : C) [h : Π Y : C, unique (X ⟶ Y)] : has_initial
 
 /-- The map from an object to the terminal object. -/
 abbreviation terminal.from [has_terminal C] (P : C) : P ⟶ ⊤_ C :=
-limit.lift (functor.empty C) { X := P, π := by tidy }.
+limit.lift (functor.empty C) (as_empty_cone P)
 /-- The map to an object from the initial object. -/
 abbreviation initial.to [has_initial C] (P : C) : ⊥_ C ⟶ P :=
-colimit.desc (functor.empty C) { X := P, ι := by tidy }.
+colimit.desc (functor.empty C) (as_empty_cocone P)
 
 instance unique_to_terminal [has_terminal C] (P : C) : unique (P ⟶ ⊤_ C) :=
 { default := terminal.from P,
@@ -76,6 +112,23 @@ instance unique_to_terminal [has_terminal C] (P : C) : unique (P ⟶ ⊤_ C) :=
 instance unique_from_initial [has_initial C] (P : C) : unique (⊥_ C ⟶ P) :=
 { default := initial.to P,
   uniq := λ m, by { apply colimit.hom_ext, rintro ⟨⟩ } }
+
+/-- The chosen terminal object is terminal. -/
+def terminal_is_terminal [has_terminal C] : is_terminal (⊤_ C) :=
+{ lift := λ s, terminal.from _ }
+
+/-- The chosen initial object is terminal. -/
+def initial_is_initial [has_initial C] : is_initial (⊥_ C) :=
+{ desc := λ s, initial.to _ }
+
+/-- Any morphism from a terminal object is mono. -/
+instance terminal.mono_from {Y : C} [has_terminal C] (f : ⊤_ C ⟶ Y) : mono f :=
+is_terminal.mono_from terminal_is_terminal _
+
+/-- Any morphism to an initial object is epi. -/
+instance initial.epi_to {Y : C} [has_initial C] (f : Y ⟶ ⊥_ C) : epi f :=
+is_initial.epi_to initial_is_initial _
+
 end
 
 end category_theory.limits