feat(category_theory/subobject): generalise bot of subobject lattice (#8232)

Author: b-mehta

src/algebra/homology/homology.lean

@@ -28,7 +28,7 @@ variables {ι : Type*}
 variables {V : Type u} [category.{v} V] [has_zero_morphisms V]
 variables {c : complex_shape ι} (C : homological_complex V c)
 
-open_locale classical
+open_locale classical zero_object
 noncomputable theory
 
 namespace homological_complex

src/category_theory/abelian/basic.lean

@@ -126,6 +126,10 @@ limits.has_finite_biproducts.of_has_finite_products
 instance has_binary_biproducts : has_binary_biproducts C :=
 limits.has_binary_biproducts_of_finite_biproducts _
 
+@[priority 100]
+instance has_zero_object : has_zero_object C :=
+has_zero_object_of_has_initial_object
+
 section to_non_preadditive_abelian
 
 /-- Every abelian category is, in particular, `non_preadditive_abelian`. -/

src/category_theory/limits/shapes/zero.lean

@@ -210,12 +210,25 @@ def zero_morphisms_of_zero_object : has_zero_morphisms C :=
   comp_zero' := λ X Y Z f, by { dunfold has_zero.zero, rw ←category.assoc, congr, }}
 
 /-- A zero object is in particular initial. -/
-lemma has_initial : has_initial C :=
+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. -/
-lemma has_terminal : has_terminal C :=
+@[priority 10]
+instance has_terminal : has_terminal C :=
 has_terminal_of_unique 0
 
+@[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) :=
@@ -380,8 +393,7 @@ def is_iso_zero_self_equiv_iso_zero (X : C) : is_iso (0 : X ⟶ X) ≃ (X ≅ 0)
 end is_iso
 
 /-- If there are zero morphisms, any initial object is a zero object. -/
-@[priority 50]
-instance has_zero_object_of_has_initial_object
+def has_zero_object_of_has_initial_object
   [has_zero_morphisms C] [has_initial C] : has_zero_object C :=
 { zero := ⊥_ C,
   unique_to := λ X, ⟨⟨0⟩, by tidy⟩,
@@ -393,8 +405,7 @@ instance has_zero_object_of_has_initial_object
   ⟩ }
 
 /-- If there are zero morphisms, any terminal object is a zero object. -/
-@[priority 50]
-instance has_zero_object_of_has_terminal_object
+def has_zero_object_of_has_terminal_object
   [has_zero_morphisms C] [has_terminal C] : has_zero_object C :=
 { zero := ⊤_ C,
   unique_from := λ X, ⟨⟨0⟩, by tidy⟩,

src/category_theory/subobject/factor_thru.lean

@@ -30,7 +30,7 @@ namespace mono_over
 `P.factors f` expresses that there exists a factorisation of `f` through `P`.
 Given `h : P.factors f`, you can recover the morphism as `P.factor_thru f h`.
 -/
-def factors {X Y : C} (P : mono_over Y) (f : X ⟶ Y) : Prop := ∃ g : X ⟶ P.val.left, g ≫ P.arrow = f
+def factors {X Y : C} (P : mono_over Y) (f : X ⟶ Y) : Prop := ∃ g : X ⟶ (P : C), g ≫ P.arrow = f
 
 lemma factors_congr {X : C} {f g : mono_over X} {Y : C} (h : Y ⟶ X) (e : f ≅ g) :
   f.factors h ↔ g.factors h :=
@@ -39,7 +39,7 @@ lemma factors_congr {X : C} {f g : mono_over X} {Y : C} (h : Y ⟶ X) (e : f ≅
 
 /-- `P.factor_thru f h` provides a factorisation of `f : X ⟶ Y` through some `P : mono_over Y`,
 given the evidence `h : P.factors f` that such a factorisation exists. -/
-def factor_thru {X Y : C} (P : mono_over Y) (f : X ⟶ Y) (h : factors P f) : X ⟶ P.val.left :=
+def factor_thru {X Y : C} (P : mono_over Y) (f : X ⟶ Y) (h : factors P f) : X ⟶ (P : C) :=
 classical.some h
 
 end mono_over

src/category_theory/subobject/lattice.lean

@@ -68,26 +68,39 @@ end
 end has_top
 
 section has_bot
-variables [has_zero_morphisms C] [has_zero_object C]
-open_locale zero_object
+
+variables [has_initial C] [initial_mono_class C]
 
 instance {X : C} : has_bot (mono_over X) :=
-{ bot := mk' (0 : 0 ⟶ X) }
+{ bot := mk' (initial.to X) }
 
-@[simp] lemma bot_left (X : C) : ((⊥ : mono_over X) : C) = 0 := rfl
-@[simp] lemma bot_arrow {X : C} : (⊥ : mono_over X).arrow = 0 :=
-by ext
+@[simp] lemma bot_left (X : C) : ((⊥ : mono_over X) : C) = ⊥_ C := rfl
+@[simp] lemma bot_arrow {X : C} : (⊥ : mono_over X).arrow = initial.to X := rfl
 
 /-- The (unique) morphism from `⊥ : mono_over X` to any other `f : mono_over X`. -/
 def bot_le {X : C} (f : mono_over X) : ⊥ ⟶ f :=
-hom_mk 0 (by simp)
+hom_mk (initial.to _) (by simp)
 
 /-- `map f` sends `⊥ : mono_over X` to `⊥ : mono_over Y`. -/
 def map_bot (f : X ⟶ Y) [mono f] : (map f).obj ⊥ ≅ ⊥ :=
-iso_of_both_ways (hom_mk 0 (by simp)) (hom_mk (𝟙 _) (by simp [id_comp f]))
+iso_of_both_ways (hom_mk (initial.to _) (by simp)) (hom_mk (𝟙 _) (by simp))
 
 end has_bot
 
+section zero_order_bot
+
+variables [has_zero_object C]
+open_locale zero_object
+
+/-- The object underlying `⊥ : subobject B` is (up to isomorphism) the zero object. -/
+def bot_coe_iso_zero {B : C} : ((⊥ : mono_over B) : C) ≅ 0 :=
+initial_is_initial.unique_up_to_iso has_zero_object.zero_is_initial
+
+@[simp] lemma bot_arrow_eq_zero [has_zero_morphisms C] {B : C} : (⊥ : mono_over B).arrow = 0 :=
+zero_of_source_iso_zero _ bot_coe_iso_zero
+
+end zero_order_bot
+
 section inf
 variables [has_pullbacks C]
 
@@ -245,8 +258,7 @@ end
 end order_top
 
 section order_bot
-variables [has_zero_morphisms C] [has_zero_object C]
-open_locale zero_object
+variables [has_initial C] [initial_mono_class C]
 
 instance order_bot {X : C} : order_bot (subobject X) :=
 { bot := quotient.mk' ⊥,
@@ -257,21 +269,37 @@ instance order_bot {X : C} : order_bot (subobject X) :=
   end,
   ..subobject.partial_order X }
 
-lemma bot_eq_zero {B : C} : (⊥ : subobject B) = subobject.mk (0 : 0 ⟶ B) := rfl
+lemma bot_eq_initial_to {B : C} : (⊥ : subobject B) = subobject.mk (initial.to B) := rfl
+
+/-- The object underlying `⊥ : subobject B` is (up to isomorphism) the initial object. -/
+def bot_coe_iso_initial {B : C} : ((⊥ : subobject B) : C) ≅ ⊥_ C := underlying_iso _
+
+lemma map_bot (f : X ⟶ Y) [mono f] : (map f).obj ⊥ = ⊥ :=
+quotient.sound' ⟨mono_over.map_bot f⟩
+
+end order_bot
+
+section zero_order_bot
+
+variables [has_zero_object C]
+open_locale zero_object
 
 /-- The object underlying `⊥ : subobject B` is (up to isomorphism) the zero object. -/
-def bot_coe_iso_zero {B : C} : ((⊥ : subobject B) : C) ≅ 0 := underlying_iso _
+def bot_coe_iso_zero {B : C} : ((⊥ : subobject B) : C) ≅ 0 :=
+bot_coe_iso_initial ≪≫ initial_is_initial.unique_up_to_iso has_zero_object.zero_is_initial
+
+variables [has_zero_morphisms C]
+
+lemma bot_eq_zero {B : C} : (⊥ : subobject B) = subobject.mk (0 : 0 ⟶ B) :=
+mk_eq_mk_of_comm _ _ (initial_is_initial.unique_up_to_iso has_zero_object.zero_is_initial) (by simp)
 
 @[simp] lemma bot_arrow {B : C} : (⊥ : subobject B).arrow = 0 :=
 zero_of_source_iso_zero _ bot_coe_iso_zero
 
-lemma map_bot (f : X ⟶ Y) [mono f] : (map f).obj ⊥ = ⊥ :=
-quotient.sound' ⟨mono_over.map_bot f⟩
-
 lemma bot_factors_iff_zero {A B : C} (f : A ⟶ B) : (⊥ : subobject B).factors f ↔ f = 0 :=
-⟨by { rintro ⟨h, w⟩, simp at w, exact w.symm, }, by { rintro rfl, exact ⟨0, by simp⟩, }⟩
+⟨by { rintro ⟨h, rfl⟩, simp }, by { rintro rfl, exact ⟨0, by simp⟩, }⟩
 
-end order_bot
+end zero_order_bot
 
 section functor
 variable (C)
@@ -442,16 +470,7 @@ lemma sup_factors_of_factors_right {A B : C} {X Y : subobject B} {f : A ⟶ B} (
   (X ⊔ Y).factors f :=
 factors_of_le f le_sup_right P
 
-/-!
-Unfortunately, there are two different ways we may obtain a `semilattice_sup_bot (subobject B)`,
-either as here, by assuming `[has_zero_morphisms C] [has_zero_object C]`,
-or if `C` is cartesian closed.
-
-These will be definitionally different, and at the very least we will need two different versions
-of `finset_sup_factors`. So far I don't see how to handle this through generalization.
--/
-section
-variables [has_zero_morphisms C] [has_zero_object C]
+variables [has_initial C] [initial_mono_class C]
 
 instance {B : C} : semilattice_sup_bot (subobject B) :=
 { ..subobject.order_bot,
@@ -472,8 +491,6 @@ begin
     { exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩), }, },
 end
 
-end
-
 end semilattice_sup
 
 section lattice
@@ -483,7 +500,7 @@ instance {B : C} : lattice (subobject B) :=
 { ..subobject.semilattice_inf_top,
   ..subobject.semilattice_sup }
 
-variables [has_zero_morphisms C] [has_zero_object C]
+variables [has_initial C] [initial_mono_class C]
 
 instance {B : C} : bounded_lattice (subobject B) :=
 { ..subobject.semilattice_inf_top,
@@ -648,7 +665,7 @@ end Sup
 
 section complete_lattice
 variables [well_powered C] [has_wide_pullbacks C] [has_images C] [has_coproducts C]
-  [has_zero_morphisms C] [has_zero_object C]
+  [initial_mono_class C]
 
 instance {B : C} : complete_lattice (subobject B) :=
 { ..subobject.semilattice_inf_top,

src/category_theory/subobject/limits.lean

@@ -259,23 +259,28 @@ lemma factor_thru_image_subobject_comp_self_assoc {W W' : C} (k : W ⟶ W') (k'
   (image_subobject f).factor_thru (k ≫ k' ≫ f) h = k ≫ k' ≫ factor_thru_image_subobject f :=
 by { ext, simp, }
 
+/-- The image of `h ≫ f` is always a smaller subobject than the image of `f`. -/
+lemma image_subobject_comp_le
+  {X' : C} (h : X' ⟶ X) (f : X ⟶ Y) [has_image f] [has_image (h ≫ f)] :
+  image_subobject (h ≫ f) ≤ image_subobject f :=
+subobject.mk_le_mk_of_comm (image.pre_comp h f) (by simp)
+
+section
+open_locale zero_object
+variables [has_zero_morphisms C] [has_zero_object C]
+
 @[simp]
-lemma image_subobject_zero_arrow [has_zero_morphisms C] [has_zero_object C] :
+lemma image_subobject_zero_arrow :
   (image_subobject (0 : X ⟶ Y)).arrow = 0 :=
 by { rw ←image_subobject_arrow, simp, }
 
 @[simp]
-lemma image_subobject_zero [has_zero_morphisms C] [has_zero_object C]{A B : C} :
+lemma image_subobject_zero {A B : C} :
   image_subobject (0 : A ⟶ B) = ⊥ :=
 subobject.eq_of_comm
   (image_subobject_iso _ ≪≫ image_zero ≪≫ subobject.bot_coe_iso_zero.symm) (by simp)
 
-/-- The image of `h ≫ f` is always a smaller subobject than the image of `f`. -/
-lemma image_subobject_comp_le
-  {X' : C} (h : X' ⟶ X) (f : X ⟶ Y) [has_image f] [has_image (h ≫ f)] :
-  image_subobject (h ≫ f) ≤ image_subobject f :=
-subobject.mk_le_mk_of_comm (image.pre_comp h f) (by simp)
-
+end
 
 section
 variables [has_equalizers C]