feat(category_theory): subsingleton (has_zero_morphisms) (#2180)

* feat(category_theory): subsingleton (has_zero_morphisms)

* fix

* Update src/category_theory/limits/shapes/zero.lean

Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>

* Update src/category_theory/limits/shapes/zero.lean

Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>

* non-terminal simp

* add warning message

* Update src/category_theory/discrete_category.lean

Co-Authored-By: Markus Himmel <markus@himmel-villmar.de>

* Apply suggestions from code review

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/category_theory/discrete_category.lean

@@ -100,7 +100,7 @@ include 𝒞
 @[simp] lemma functor_map_id
   (F : discrete J ⥤ C) {j : discrete J} (f : j ⟶ j) : F.map f = 𝟙 (F.obj j) :=
 begin
-  have h : f = 𝟙 j, cases f, cases f, ext,
+  have h : f = 𝟙 j, { cases f, cases f, ext, },
   rw h,
   simp,
 end

src/category_theory/limits/shapes/zero.lean

@@ -45,6 +45,42 @@ attribute [simp] has_zero_morphisms.comp_zero
 restate_axiom has_zero_morphisms.zero_comp'
 attribute [simp, reassoc] has_zero_morphisms.zero_comp
 
+namespace has_zero_morphisms
+variables {C}
+
+/-- This lemma will be immediately superseded by `ext`, below. -/
+private lemma ext_aux (I J : has_zero_morphisms.{v} C)
+  (w : ∀ X Y : C, (@has_zero_morphisms.has_zero.{v} _ _ I X Y).zero = (@has_zero_morphisms.has_zero.{v} _ _ J X Y).zero) : I = J :=
+begin
+  resetI,
+  cases I, cases J,
+  congr,
+  { ext X Y,
+    exact w X Y },
+  { apply proof_irrel_heq },
+  { apply proof_irrel_heq }
+end
+
+/--
+If you're tempted to use this lemma "in the wild", you should probably
+carefully consider whether you've made a mistake in allowing two
+instances of `has_zero_morphisms` to exist at all.
+
+See, particularly, the note on `zero_morphisms_of_zero_object` below.
+-/
+lemma ext (I J : has_zero_morphisms.{v} C) : I = J :=
+begin
+  apply ext_aux,
+  intros X Y,
+  rw ←@has_zero_morphisms.comp_zero _ _ I X X (@has_zero_morphisms.has_zero _ _ J X X).zero,
+  rw @has_zero_morphisms.zero_comp _ _ J,
+end
+
+instance : subsingleton (has_zero_morphisms.{v} C) :=
+⟨ext⟩
+
+end has_zero_morphisms
+
 section
 variables {C} [has_zero_morphisms.{v} C]
 
@@ -56,6 +92,26 @@ by { rw [←has_zero_morphisms.comp_zero.{v} C f Z, cancel_epi] at h, exact h }
 
 end
 
+section
+universes v' u'
+variables (D : Type u') [𝒟 : category.{v'} D]
+include 𝒟
+
+variables [has_zero_morphisms.{v} C] [has_zero_morphisms.{v'} D]
+
+@[simp] lemma equivalence_preserves_zero_morphisms (F : C ≌ D) (X Y : C) :
+  F.functor.map (0 : X ⟶ Y) = (0 : F.functor.obj X ⟶ F.functor.obj Y) :=
+begin
+  have t : F.functor.map (0 : X ⟶ Y) = F.functor.map (0 : X ⟶ Y) ≫ (0 : F.functor.obj Y ⟶ F.functor.obj Y),
+  { apply faithful.injectivity (F.inverse),
+    simp only [functor.map_comp, equivalence.unit, equivalence.unit_inv, equivalence.inv_fun_map, category.assoc],
+    dsimp,
+    simp, },
+  exact t.trans (by simp)
+end
+
+end
+
 /-- A category "has a zero object" if it has an object which is both initial and terminal. -/
 class has_zero_object :=
 (zero : C)
@@ -96,13 +152,15 @@ section
 variable [has_zero_morphisms.{v} C]
 
 /--  An arrow ending in the zero object is zero -/
+@[ext]
 lemma zero_of_to_zero {X : C} (f : X ⟶ 0) : f = 0 :=
 begin
   rw (has_zero_object.unique_from.{v} X).uniq f,
   rw (has_zero_object.unique_from.{v} X).uniq (0 : X ⟶ 0)
 end
 
 /-- An arrow starting at the zero object is zero -/
+@[ext]
 lemma zero_of_from_zero {X : C} (f : 0 ⟶ X) : f = 0 :=
 begin
   rw (has_zero_object.unique_to.{v} X).uniq f,

src/tactic/ext.lean

@@ -269,23 +269,25 @@ add_tactic_doc
   decl_names               := [`extensional_attribute],
   tags                     := [] }
 
+-- We mark some existing extensionality lemmas.
 attribute [ext] array.ext propext prod.ext
 attribute [ext [(→),thunk]] _root_.funext
 
-namespace ulift
-@[ext] lemma ext {α : Type u₁} (X Y : ulift.{u₂} α) (w : X.down = Y.down) : X = Y :=
-begin
-  cases X, cases Y, dsimp at w, rw w,
-end
-end ulift
+-- We create some extensionality lemmas for existing structures.
+attribute [ext] ulift
 
 namespace plift
+-- This is stronger than the one generated automatically.
 @[ext] lemma ext {P : Prop} (a b : plift P) : a = b :=
 begin
   cases a, cases b, refl
 end
 end plift
 
+-- Conservatively, we'll only add extensionality lemmas for `has_*` structures
+-- as they become useful.
+attribute [ext] has_zero
+
 namespace tactic
 
 meta def try_intros : ext_patt → tactic ext_patt