From 634eab1080e5313afd206b1cc6e00aa28135fc15 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Tue, 19 Apr 2022 15:52:31 +0000
Subject: [PATCH] feat(category_theory/limits): add characteristic predicate
 for zero objects (#13511)

---
 src/algebra/category/Group/zero.lean          |   2 +-
 .../normed/group/SemiNormedGroup.lean         |   2 +-
 src/category_theory/closed/zero.lean          |   2 +-
 .../limits/preserves/shapes/zero.lean         |   2 +-
 .../limits/shapes/default.lean                |   2 +-
 .../shapes/{zero.lean => zero_morphisms.lean} |  90 ++------
 .../limits/shapes/zero_objects.lean           | 205 ++++++++++++++++++
 src/category_theory/simple.lean               |   2 +-
 8 files changed, 225 insertions(+), 82 deletions(-)
 rename src/category_theory/limits/shapes/{zero.lean => zero_morphisms.lean} (85%)
 create mode 100644 src/category_theory/limits/shapes/zero_objects.lean

diff --git a/src/algebra/category/Group/zero.lean b/src/algebra/category/Group/zero.lean
index ff16c712bbe24..47e5e3ec3d166 100644
--- a/src/algebra/category/Group/zero.lean
+++ b/src/algebra/category/Group/zero.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.category.Group.basic
-import category_theory.limits.shapes.zero
+import category_theory.limits.shapes.zero_morphisms
 
 /-!
 # The category of (commutative) (additive) groups has a zero object.
diff --git a/src/analysis/normed/group/SemiNormedGroup.lean b/src/analysis/normed/group/SemiNormedGroup.lean
index 3681388833d59..46a5a9d9646c5 100644
--- a/src/analysis/normed/group/SemiNormedGroup.lean
+++ b/src/analysis/normed/group/SemiNormedGroup.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Riccardo Brasca
 -/
 import analysis.normed.group.hom
-import category_theory.limits.shapes.zero
+import category_theory.limits.shapes.zero_morphisms
 import category_theory.concrete_category.bundled_hom
 
 /-!
diff --git a/src/category_theory/closed/zero.lean b/src/category_theory/closed/zero.lean
index 04f35974b8dc3..751ad5e9daf12 100644
--- a/src/category_theory/closed/zero.lean
+++ b/src/category_theory/closed/zero.lean
@@ -5,7 +5,7 @@ Authors: Bhavik Mehta
 -/
 
 import category_theory.closed.cartesian
-import category_theory.limits.shapes.zero
+import category_theory.limits.shapes.zero_morphisms
 import category_theory.punit
 import category_theory.conj
 
diff --git a/src/category_theory/limits/preserves/shapes/zero.lean b/src/category_theory/limits/preserves/shapes/zero.lean
index fe9098d1e9987..407b1444f4f9f 100644
--- a/src/category_theory/limits/preserves/shapes/zero.lean
+++ b/src/category_theory/limits/preserves/shapes/zero.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import category_theory.limits.preserves.shapes.terminal
-import category_theory.limits.shapes.zero
+import category_theory.limits.shapes.zero_morphisms
 
 /-!
 # Preservation of zero objects and zero morphisms
diff --git a/src/category_theory/limits/shapes/default.lean b/src/category_theory/limits/shapes/default.lean
index 157e139ed7f73..ce39844b6f1e1 100644
--- a/src/category_theory/limits/shapes/default.lean
+++ b/src/category_theory/limits/shapes/default.lean
@@ -5,7 +5,7 @@ import category_theory.limits.shapes.finite_products
 import category_theory.limits.shapes.finite_limits
 import category_theory.limits.shapes.biproducts
 import category_theory.limits.shapes.images
-import category_theory.limits.shapes.zero
+import category_theory.limits.shapes.zero_morphisms
 import category_theory.limits.shapes.kernels
 import category_theory.limits.shapes.equalizers
 import category_theory.limits.shapes.wide_pullbacks
diff --git a/src/category_theory/limits/shapes/zero.lean b/src/category_theory/limits/shapes/zero_morphisms.lean
similarity index 85%
rename from src/category_theory/limits/shapes/zero.lean
rename to src/category_theory/limits/shapes/zero_morphisms.lean
index 14beac6f2db01..d2c95656aef36 100644
--- a/src/category_theory/limits/shapes/zero.lean
+++ b/src/category_theory/limits/shapes/zero_morphisms.lean
@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import category_theory.limits.shapes.products
 import category_theory.limits.shapes.images
 import category_theory.isomorphism_classes
+import category_theory.limits.shapes.zero_objects
 
 /-!
 # Zero morphisms and zero objects
@@ -131,51 +132,24 @@ instance : has_zero_morphisms (C ⥤ D) :=
 
 end
 
-variables (C)
-
-/-- A category "has a zero object" if it has an object which is both initial and terminal. -/
-class has_zero_object :=
-(zero : C)
-(unique_to : Π X : C, unique (zero ⟶ X))
-(unique_from : Π X : C, unique (X ⟶ zero))
-
-instance has_zero_object_punit : has_zero_object (discrete punit) :=
-{ zero := punit.star,
-  unique_to := by tidy,
-  unique_from := by tidy, }
+/-- A category with a zero object has zero morphisms.
 
-variables {C}
+    It is rarely a good idea to use this. Many categories that have a zero object have zero
+    morphisms for some other reason, for example from additivity. Library code that uses
+    `zero_morphisms_of_zero_object` will then be incompatible with these categories because
+    the `has_zero_morphisms` instances will not be definitionally equal. For this reason library
+    code should generally ask for an instance of `has_zero_morphisms` separately, even if it already
+    asks for an instance of `has_zero_objects`. -/
+def is_zero.has_zero_morphisms {O : C} (hO : is_zero O) : has_zero_morphisms C :=
+{ has_zero := λ X Y,
+  { zero := hO.from X ≫ hO.to Y },
+  zero_comp' := λ X Y Z f, by { rw category.assoc, congr, apply hO.eq_of_src, },
+  comp_zero' := λ X Y Z f, by { rw ←category.assoc, congr, apply hO.eq_of_tgt, }}
 
 namespace has_zero_object
 
 variables [has_zero_object C]
-
-/--
-Construct a `has_zero C` for a category with a zero object.
-This can not be a global instance as it will trigger for every `has_zero C` typeclass search.
--/
-protected def has_zero : has_zero C :=
-{ zero := has_zero_object.zero }
-
-localized "attribute [instance] category_theory.limits.has_zero_object.has_zero" in zero_object
-localized "attribute [instance] category_theory.limits.has_zero_object.unique_to" in zero_object
-localized "attribute [instance] category_theory.limits.has_zero_object.unique_from" in zero_object
-
-@[ext]
-lemma to_zero_ext {X : C} (f g : X ⟶ 0) : f = g :=
-by rw [(has_zero_object.unique_from X).uniq f, (has_zero_object.unique_from X).uniq g]
-
-@[ext]
-lemma from_zero_ext {X : C} (f g : 0 ⟶ X) : f = g :=
-by rw [(has_zero_object.unique_to X).uniq f, (has_zero_object.unique_to X).uniq g]
-
-instance (X : C) : subsingleton (X ≅ 0) := by tidy
-
-instance {X : C} (f : 0 ⟶ X) : mono f :=
-{ right_cancellation := λ Z g h w, by ext, }
-
-instance {X : C} (f : X ⟶ 0) : epi f :=
-{ left_cancellation := λ Z g h w, by ext, }
+open_locale zero_object
 
 /-- A category with a zero object has zero morphisms.
 
@@ -191,38 +165,6 @@ def zero_morphisms_of_zero_object : has_zero_morphisms C :=
   zero_comp' := λ X Y Z f, by { dunfold has_zero.zero, rw category.assoc, congr, },
   comp_zero' := λ X Y Z f, by { dunfold has_zero.zero, rw ←category.assoc, congr, }}
 
-/-- A zero object is in particular initial. -/
-def zero_is_initial : is_initial (0 : C) :=
-is_initial.of_unique 0
-/-- A zero object is in particular terminal. -/
-def zero_is_terminal : is_terminal (0 : C) :=
-is_terminal.of_unique 0
-
-/-- A zero object is in particular initial. -/
-@[priority 10]
-instance has_initial : has_initial C :=
-has_initial_of_unique 0
-/-- A zero object is in particular terminal. -/
-@[priority 10]
-instance has_terminal : has_terminal C :=
-has_terminal_of_unique 0
-
-/-- The (unique) isomorphism between any initial object and the zero object. -/
-def zero_iso_is_initial {X : C} (t : is_initial X) : 0 ≅ X :=
-zero_is_initial.unique_up_to_iso t
-
-/-- The (unique) isomorphism between any terminal object and the zero object. -/
-def zero_iso_is_terminal {X : C} (t : is_terminal X) : 0 ≅ X :=
-zero_is_terminal.unique_up_to_iso t
-
-/-- The (unique) isomorphism between the chosen initial object and the chosen zero object. -/
-def zero_iso_initial [has_initial C] : 0 ≅ ⊥_ C :=
-zero_is_initial.unique_up_to_iso initial_is_initial
-
-/-- The (unique) isomorphism between the chosen terminal object and the chosen zero object. -/
-def zero_iso_terminal [has_terminal C] : 0 ≅ ⊤_ C :=
-zero_is_terminal.unique_up_to_iso terminal_is_terminal
-
 section has_zero_morphisms
 variables [has_zero_morphisms C]
 
@@ -256,10 +198,6 @@ by ext
 
 end has_zero_morphisms
 
-@[priority 100]
-instance has_strict_initial : initial_mono_class C :=
-initial_mono_class.of_is_initial zero_is_initial (λ X, category_theory.mono _)
-
 open_locale zero_object
 
 instance {B : Type*} [category B] [has_zero_morphisms C] : has_zero_object (B ⥤ C) :=
diff --git a/src/category_theory/limits/shapes/zero_objects.lean b/src/category_theory/limits/shapes/zero_objects.lean
new file mode 100644
index 0000000000000..0e6096842ebc9
--- /dev/null
+++ b/src/category_theory/limits/shapes/zero_objects.lean
@@ -0,0 +1,205 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Johan Commelin
+-/
+import category_theory.limits.shapes.products
+import category_theory.limits.shapes.images
+import category_theory.isomorphism_classes
+
+/-!
+# Zero objects
+
+A category "has a zero object" if it has an object which is both initial and terminal. Having a
+zero object provides zero morphisms, as the unique morphisms factoring through the zero object;
+see `category_theory.limits.shapes.zero_morphisms`.
+
+## References
+
+* [F. Borceux, *Handbook of Categorical Algebra 2*][borceux-vol2]
+-/
+
+noncomputable theory
+
+universes v u v' u'
+
+open category_theory
+open category_theory.category
+
+namespace category_theory.limits
+
+variables {C : Type u} [category.{v} C]
+variables {D : Type u'} [category.{v'} D]
+
+/-- An object `X` in a category is a *zero object* if for every object `Y`
+there is a unique morphism `to : X → Y` and a unique morphism `from : Y → X`.
+
+This is a characteristic predicate for `has_zero_object`. -/
+structure is_zero (X : C) : Prop :=
+(unique_to   : ∀ Y, nonempty (unique (X ⟶ Y)))
+(unique_from : ∀ Y, nonempty (unique (Y ⟶ X)))
+
+namespace is_zero
+
+variables {X Y : C}
+
+/-- If `h : is_zero X`, then `h.to Y` is a choice of unique morphism `X → Y`. -/
+protected def «to» (h : is_zero X) (Y : C) : X ⟶ Y :=
+@default (X ⟶ Y) $ @unique.inhabited _ $ (h.unique_to Y).some
+
+lemma eq_to (h : is_zero X) (f : X ⟶ Y) : f = h.to Y :=
+@unique.eq_default _ (id _) _
+
+lemma to_eq (h : is_zero X) (f : X ⟶ Y) : h.to Y = f :=
+(h.eq_to f).symm
+
+/-- If `h : is_zero X`, then `h.from Y` is a choice of unique morphism `Y → X`. -/
+protected def «from» (h : is_zero X) (Y : C) : Y ⟶ X :=
+@default (Y ⟶ X) $ @unique.inhabited _ $ (h.unique_from Y).some
+
+lemma eq_from (h : is_zero X) (f : Y ⟶ X) : f = h.from Y :=
+@unique.eq_default _ (id _) _
+
+lemma from_eq (h : is_zero X) (f : Y ⟶ X) : h.from Y = f :=
+(h.eq_from f).symm
+
+lemma eq_of_src (hX : is_zero X) (f g : X ⟶ Y) : f = g :=
+(hX.eq_to f).trans (hX.eq_to g).symm
+
+lemma eq_of_tgt (hX : is_zero X) (f g : Y ⟶ X) : f = g :=
+(hX.eq_from f).trans (hX.eq_from g).symm
+
+/-- Any two zero objects are isomorphic. -/
+def iso (hX : is_zero X) (hY : is_zero Y) : X ≅ Y :=
+{ hom := hX.to Y,
+  inv := hX.from Y,
+  hom_inv_id' := hX.eq_of_src _ _,
+  inv_hom_id' := hY.eq_of_src _ _, }
+
+/-- A zero object is in particular initial. -/
+protected def is_initial (hX : is_zero X) : is_initial X :=
+@is_initial.of_unique _ _ X $ λ Y, (hX.unique_to Y).some
+
+/-- A zero object is in particular terminal. -/
+protected def is_terminal (hX : is_zero X) : is_terminal X :=
+@is_terminal.of_unique _ _ X $ λ Y, (hX.unique_from Y).some
+
+/-- The (unique) isomorphism between any initial object and the zero object. -/
+def iso_is_initial (hX : is_zero X) (hY : is_initial Y) : X ≅ Y :=
+hX.is_initial.unique_up_to_iso hY
+
+/-- The (unique) isomorphism between any terminal object and the zero object. -/
+def iso_is_terminal (hX : is_zero X) (hY : is_terminal Y) : X ≅ Y :=
+hX.is_terminal.unique_up_to_iso hY
+
+lemma of_iso (hY : is_zero Y) (e : X ≅ Y) : is_zero X :=
+begin
+  refine ⟨λ Z, ⟨⟨⟨e.hom ≫ hY.to Z⟩, λ f, _⟩⟩, λ Z, ⟨⟨⟨hY.from Z ≫ e.inv⟩, λ f, _⟩⟩⟩,
+  { rw ← cancel_epi e.inv, apply hY.eq_of_src, },
+  { rw ← cancel_mono e.hom, apply hY.eq_of_tgt, },
+end
+
+end is_zero
+
+lemma iso.is_zero_iff {X Y : C} (e : X ≅ Y) :
+  is_zero X ↔ is_zero Y :=
+⟨λ h, h.of_iso e.symm, λ h, h.of_iso e⟩
+
+variables (C)
+
+/-- A category "has a zero object" if it has an object which is both initial and terminal. -/
+class has_zero_object :=
+(zero : C)
+(unique_to : Π X : C, unique (zero ⟶ X))
+(unique_from : Π X : C, unique (X ⟶ zero))
+
+instance has_zero_object_punit : has_zero_object (discrete punit) :=
+{ zero := punit.star,
+  unique_to := by tidy,
+  unique_from := by tidy, }
+
+
+namespace has_zero_object
+
+variables [has_zero_object C]
+
+/--
+Construct a `has_zero C` for a category with a zero object.
+This can not be a global instance as it will trigger for every `has_zero C` typeclass search.
+-/
+protected def has_zero : has_zero C :=
+{ zero := has_zero_object.zero }
+
+localized "attribute [instance] category_theory.limits.has_zero_object.has_zero" in zero_object
+localized "attribute [instance] category_theory.limits.has_zero_object.unique_to" in zero_object
+localized "attribute [instance] category_theory.limits.has_zero_object.unique_from" in zero_object
+
+lemma is_zero_zero : is_zero (0 : C) :=
+{ unique_to :=   λ Y, ⟨has_zero_object.unique_to Y⟩,
+  unique_from := λ Y, ⟨has_zero_object.unique_from Y⟩ }
+
+/-- Every zero object is isomorphic to *the* zero object. -/
+def is_zero.iso_zero {X : C} (hX : is_zero X) : X ≅ 0 :=
+hX.iso (is_zero_zero C)
+
+variables {C}
+
+@[ext]
+lemma to_zero_ext {X : C} (f g : X ⟶ 0) : f = g :=
+(is_zero_zero C).eq_of_tgt _ _
+
+@[ext]
+lemma from_zero_ext {X : C} (f g : 0 ⟶ X) : f = g :=
+(is_zero_zero C).eq_of_src _ _
+
+instance (X : C) : subsingleton (X ≅ 0) := by tidy
+
+instance {X : C} (f : 0 ⟶ X) : mono f :=
+{ right_cancellation := λ Z g h w, by ext, }
+
+instance {X : C} (f : X ⟶ 0) : epi f :=
+{ left_cancellation := λ Z g h w, by ext, }
+
+/-- A zero object is in particular initial. -/
+def zero_is_initial : is_initial (0 : C) :=
+is_initial.of_unique 0
+
+/-- A zero object is in particular terminal. -/
+def zero_is_terminal : is_terminal (0 : C) :=
+is_terminal.of_unique 0
+
+/-- A zero object is in particular initial. -/
+@[priority 10]
+instance has_initial : has_initial C :=
+has_initial_of_unique 0
+
+/-- A zero object is in particular terminal. -/
+@[priority 10]
+instance has_terminal : has_terminal C :=
+has_terminal_of_unique 0
+
+/-- The (unique) isomorphism between any initial object and the zero object. -/
+def zero_iso_is_initial {X : C} (t : is_initial X) : 0 ≅ X :=
+zero_is_initial.unique_up_to_iso t
+
+/-- The (unique) isomorphism between any terminal object and the zero object. -/
+def zero_iso_is_terminal {X : C} (t : is_terminal X) : 0 ≅ X :=
+zero_is_terminal.unique_up_to_iso t
+
+/-- The (unique) isomorphism between the chosen initial object and the chosen zero object. -/
+def zero_iso_initial [has_initial C] : 0 ≅ ⊥_ C :=
+zero_is_initial.unique_up_to_iso initial_is_initial
+
+/-- The (unique) isomorphism between the chosen terminal object and the chosen zero object. -/
+def zero_iso_terminal [has_terminal C] : 0 ≅ ⊤_ C :=
+zero_is_terminal.unique_up_to_iso terminal_is_terminal
+
+@[priority 100]
+instance has_strict_initial : initial_mono_class C :=
+initial_mono_class.of_is_initial zero_is_initial (λ X, category_theory.mono _)
+
+open_locale zero_object
+
+end has_zero_object
+
+end category_theory.limits
diff --git a/src/category_theory/simple.lean b/src/category_theory/simple.lean
index a3370b017afda..3f5a8fe86a69d 100644
--- a/src/category_theory/simple.lean
+++ b/src/category_theory/simple.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison
 -/
-import category_theory.limits.shapes.zero
+import category_theory.limits.shapes.zero_morphisms
 import category_theory.limits.shapes.kernels
 import category_theory.abelian.basic