feat(category_theory/limits): monomorphisms from initial (#8099)

Defines a class for categories where every morphism from initial is a monomorphism. If the category has a terminal object, this is equivalent to saying the unique morphism from initial to terminal is a monomorphism, so this is essentially a "zero_le_one" for categories. I'm happy to change the name of this class!

This axiom does not appear to have a common name, though it is (equivalent to) the second of Freyd's AT axioms: specifically it is a property shared by abelian categories and pretoposes. The main advantage to this class is that it is the precise condition required for the subobject lattice to have a bottom element, resolving the discussion here: #6278 (comment)

I've also made some minor changes to later parts of this file, essentially de-duplicating arguments, and moving the `comparison` section up so that all the results about terminal objects in index categories of limits are together rather than split in two.

src/category_theory/limits/shapes/terminal.lean

@@ -100,6 +100,18 @@ by haveI := t.split_mono_from f; apply_instance
 lemma is_initial.epi_to {X Y : C} (t : is_initial X) (f : Y ⟶ X) : epi f :=
 by haveI := t.split_epi_to f; apply_instance
 
+/-- If `T` and `T'` are terminal, they are isomorphic. -/
+@[simps]
+def is_terminal.unique_up_to_iso {T T' : C} (hT : is_terminal T) (hT' : is_terminal T') : T ≅ T' :=
+{ hom := hT'.from _,
+  inv := hT.from _ }
+
+/-- If `I` and `I'` are initial, they are isomorphic. -/
+@[simps]
+def is_initial.unique_up_to_iso {I I' : C} (hI : is_initial I) (hI' : is_initial I') : I ≅ I' :=
+{ hom := hI.to _,
+  inv := hI'.to _ }
+
 variable (C)
 
 /--
@@ -204,10 +216,90 @@ def initial_unop_of_terminal {X : Cᵒᵖ} (t : is_terminal X) : is_initial X.un
 { desc := λ s, (t.from (opposite.op s.X)).unop,
   uniq' := λ s m w, quiver.hom.op_inj (t.hom_ext _ _) }
 
+/-- A category is a `initial_mono_class` if the canonical morphism of an initial object is a
+monomorphism.  In practice, this is most useful when given an arbitrary morphism out of the chosen
+initial object, see `initial.mono_from`.
+Given a terminal object, this is equivalent to the assumption that the unique morphism from initial
+to terminal is a monomorphism, which is the second of Freyd's axioms for an AT category.
+
+TODO: This is a condition satisfied by categories with zero objects and morphisms, as well as
+categories with a strict initial object; though these conditions are essentially mutually exclusive.
+-/
+class initial_mono_class (C : Type u) [category.{v} C] : Prop :=
+(is_initial_mono_from : ∀ {I} (X : C) (hI : is_initial I), mono (hI.to X))
+
+lemma is_initial.mono_from [initial_mono_class C] {I} {X : C} (hI : is_initial I) (f : I ⟶ X) :
+  mono f :=
+begin
+  rw hI.hom_ext f (hI.to X),
+  apply initial_mono_class.is_initial_mono_from,
+end
+
+@[priority 100]
+instance initial.mono_from [has_initial C] [initial_mono_class C] (X : C) (f : ⊥_ C ⟶ X) :
+  mono f :=
+initial_is_initial.mono_from f
+
+/-- To show a category is a `initial_mono_class` it suffices to give an initial object such that
+every morphism out of it is a monomorphism. -/
+lemma initial_mono_class.of_is_initial {I : C} (hI : is_initial I) (h : ∀ X, mono (hI.to X)) :
+  initial_mono_class C :=
+{ is_initial_mono_from := λ I' X hI',
+  begin
+    rw hI'.hom_ext (hI'.to X) ((hI'.unique_up_to_iso hI).hom ≫ hI.to X),
+    apply mono_comp,
+  end }
+
+/-- To show a category is a `initial_mono_class` it suffices to show every morphism out of the
+initial object is a monomorphism. -/
+lemma initial_mono_class.of_initial [has_initial C] (h : ∀ X : C, mono (initial.to X)) :
+  initial_mono_class C :=
+initial_mono_class.of_is_initial initial_is_initial h
+
+/-- To show a category is a `initial_mono_class` it suffices to show the unique morphism from an
+initial object to a terminal object is a monomorphism. -/
+lemma initial_mono_class.of_is_terminal {I T : C} (hI : is_initial I) (hT : is_terminal T)
+  (f : mono (hI.to T)) :
+  initial_mono_class C :=
+initial_mono_class.of_is_initial hI (λ X, mono_of_mono_fac (hI.hom_ext (_ ≫ hT.from X) (hI.to T)))
+
+/-- To show a category is a `initial_mono_class` it suffices to show the unique morphism from the
+initial object to a terminal object is a monomorphism. -/
+lemma initial_mono_class.of_terminal [has_initial C] [has_terminal C]
+  (h : mono (initial.to (⊤_ C))) :
+  initial_mono_class C :=
+initial_mono_class.of_is_terminal initial_is_initial terminal_is_terminal h
+
+section comparison
+variables {D : Type u₂} [category.{v} D] (G : C ⥤ D)
+
+/--
+The comparison morphism from the image of a terminal object to the terminal object in the target
+category.
+This is an isomorphism iff `G` preserves terminal objects, see
+`category_theory.limits.preserves_terminal.of_iso_comparison`.
+-/
+def terminal_comparison [has_terminal C] [has_terminal D] :
+  G.obj (⊤_ C) ⟶ ⊤_ D :=
+terminal.from _
+
+/--
+The comparison morphism from the initial object in the target category to the image of the initial
+object.
+-/
+-- TODO: Show this is an isomorphism if and only if `G` preserves initial objects.
+def initial_comparison [has_initial C] [has_initial D] :
+  ⊥_ D ⟶ G.obj (⊥_ C) :=
+initial.to _
+
+end comparison
+
+variables {J : Type v} [small_category J]
+
 /-- From a functor `F : J ⥤ C`, given an initial object of `J`, construct a cone for `J`.
 In `limit_of_diagram_initial` we show it is a limit cone. -/
 @[simps]
-def cone_of_diagram_initial {J : Type v} [small_category J]
+def cone_of_diagram_initial
   {X : J} (tX : is_initial X) (F : J ⥤ C) : cone F :=
 { X := F.obj X,
   π :=
@@ -220,7 +312,7 @@ def cone_of_diagram_initial {J : Type v} [small_category J]
 
 /-- From a functor `F : J ⥤ C`, given an initial object of `J`, show the cone
 `cone_of_diagram_initial` is a limit. -/
-def limit_of_diagram_initial {J : Type v} [small_category J]
+def limit_of_diagram_initial
   {X : J} (tX : is_initial X) (F : J ⥤ C) :
 is_limit (cone_of_diagram_initial tX F) :=
 { lift := λ s, s.π.app X,
@@ -234,7 +326,7 @@ is_limit (cone_of_diagram_initial tX F) :=
 /-- For a functor `F : J ⥤ C`, if `J` has an initial object then the image of it is isomorphic
 to the limit of `F`. -/
 @[reducible]
-def limit_of_initial {J : Type v} [small_category J] (F : J ⥤ C)
+def limit_of_initial (F : J ⥤ C)
   [has_initial J] [has_limit F] :
 limit F ≅ F.obj (⊥_ J) :=
 is_limit.cone_point_unique_up_to_iso
@@ -244,7 +336,7 @@ is_limit.cone_point_unique_up_to_iso
 /-- From a functor `F : J ⥤ C`, given a terminal object of `J`, construct a cocone for `J`.
 In `colimit_of_diagram_terminal` we show it is a colimit cocone. -/
 @[simps]
-def cocone_of_diagram_terminal {J : Type v} [small_category J]
+def cocone_of_diagram_terminal
   {X : J} (tX : is_terminal X) (F : J ⥤ C) : cocone F :=
 { X := F.obj X,
   ι :=
@@ -257,7 +349,7 @@ def cocone_of_diagram_terminal {J : Type v} [small_category J]
 
 /-- From a functor `F : J ⥤ C`, given a terminal object of `J`, show the cocone
 `cocone_of_diagram_terminal` is a colimit. -/
-def colimit_of_diagram_terminal {J : Type v} [small_category J]
+def colimit_of_diagram_terminal
   {X : J} (tX : is_terminal X) (F : J ⥤ C) :
 is_colimit (cocone_of_diagram_terminal tX F) :=
 { desc := λ s, s.ι.app X,
@@ -268,40 +360,13 @@ is_colimit (cocone_of_diagram_terminal tX F) :=
 /-- For a functor `F : J ⥤ C`, if `J` has a terminal object then the image of it is isomorphic
 to the colimit of `F`. -/
 @[reducible]
-def colimit_of_terminal {J : Type v} [small_category J] (F : J ⥤ C)
+def colimit_of_terminal (F : J ⥤ C)
   [has_terminal J] [has_colimit F] :
 colimit F ≅ F.obj (⊤_ J) :=
 is_colimit.cocone_point_unique_up_to_iso
   (colimit.is_colimit _)
   (colimit_of_diagram_terminal terminal_is_terminal F)
 
-end
-
-section comparison
-variables {C} {D : Type u₂} [category.{v} D] (G : C ⥤ D)
-
-/--
-The comparison morphism from the image of a terminal object to the terminal object in the target
-category.
--/
--- TODO: Show this is an isomorphism if and only if `G` preserves terminal objects.
-def terminal_comparison [has_terminal C] [has_terminal D] :
-  G.obj (⊤_ C) ⟶ ⊤_ D :=
-terminal.from _
-
-/--
-The comparison morphism from the initial object in the target category to the image of the initial
-object.
--/
--- TODO: Show this is an isomorphism if and only if `G` preserves initial objects.
-def initial_comparison [has_initial C] [has_initial D] :
-  ⊥_ D ⟶ G.obj (⊥_ C) :=
-initial.to _
-
-end comparison
-
-variables {C} {J : Type v} [small_category J]
-
 /--
 If `j` is initial in the index category, then the map `limit.π F j` is an isomorphism.
 -/
@@ -324,4 +389,6 @@ instance is_iso_ι_terminal [has_terminal J] (F : J ⥤ C) [has_colimit F] :
   is_iso (colimit.ι F (⊤_ J)) :=
 is_iso_ι_of_is_terminal (terminal_is_terminal) F
 
+end
+
 end category_theory.limits