|
| 1 | +/- |
| 2 | +Copyright (c) 2019 Scott Morrison. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Scott Morrison, Johan Commelin |
| 5 | +-/ |
| 6 | +import category_theory.limits.shapes.products |
| 7 | +import category_theory.limits.shapes.images |
| 8 | +import category_theory.isomorphism_classes |
| 9 | + |
| 10 | +/-! |
| 11 | +# Zero objects |
| 12 | +
|
| 13 | +A category "has a zero object" if it has an object which is both initial and terminal. Having a |
| 14 | +zero object provides zero morphisms, as the unique morphisms factoring through the zero object; |
| 15 | +see `category_theory.limits.shapes.zero_morphisms`. |
| 16 | +
|
| 17 | +## References |
| 18 | +
|
| 19 | +* [F. Borceux, *Handbook of Categorical Algebra 2*][borceux-vol2] |
| 20 | +-/ |
| 21 | + |
| 22 | +noncomputable theory |
| 23 | + |
| 24 | +universes v u v' u' |
| 25 | + |
| 26 | +open category_theory |
| 27 | +open category_theory.category |
| 28 | + |
| 29 | +namespace category_theory.limits |
| 30 | + |
| 31 | +variables {C : Type u} [category.{v} C] |
| 32 | +variables {D : Type u'} [category.{v'} D] |
| 33 | + |
| 34 | +/-- An object `X` in a category is a *zero object* if for every object `Y` |
| 35 | +there is a unique morphism `to : X → Y` and a unique morphism `from : Y → X`. |
| 36 | +
|
| 37 | +This is a characteristic predicate for `has_zero_object`. -/ |
| 38 | +structure is_zero (X : C) : Prop := |
| 39 | +(unique_to : ∀ Y, nonempty (unique (X ⟶ Y))) |
| 40 | +(unique_from : ∀ Y, nonempty (unique (Y ⟶ X))) |
| 41 | + |
| 42 | +namespace is_zero |
| 43 | + |
| 44 | +variables {X Y : C} |
| 45 | + |
| 46 | +/-- If `h : is_zero X`, then `h.to Y` is a choice of unique morphism `X → Y`. -/ |
| 47 | +protected def «to» (h : is_zero X) (Y : C) : X ⟶ Y := |
| 48 | +@default (X ⟶ Y) $ @unique.inhabited _ $ (h.unique_to Y).some |
| 49 | + |
| 50 | +lemma eq_to (h : is_zero X) (f : X ⟶ Y) : f = h.to Y := |
| 51 | +@unique.eq_default _ (id _) _ |
| 52 | + |
| 53 | +lemma to_eq (h : is_zero X) (f : X ⟶ Y) : h.to Y = f := |
| 54 | +(h.eq_to f).symm |
| 55 | + |
| 56 | +/-- If `h : is_zero X`, then `h.from Y` is a choice of unique morphism `Y → X`. -/ |
| 57 | +protected def «from» (h : is_zero X) (Y : C) : Y ⟶ X := |
| 58 | +@default (Y ⟶ X) $ @unique.inhabited _ $ (h.unique_from Y).some |
| 59 | + |
| 60 | +lemma eq_from (h : is_zero X) (f : Y ⟶ X) : f = h.from Y := |
| 61 | +@unique.eq_default _ (id _) _ |
| 62 | + |
| 63 | +lemma from_eq (h : is_zero X) (f : Y ⟶ X) : h.from Y = f := |
| 64 | +(h.eq_from f).symm |
| 65 | + |
| 66 | +lemma eq_of_src (hX : is_zero X) (f g : X ⟶ Y) : f = g := |
| 67 | +(hX.eq_to f).trans (hX.eq_to g).symm |
| 68 | + |
| 69 | +lemma eq_of_tgt (hX : is_zero X) (f g : Y ⟶ X) : f = g := |
| 70 | +(hX.eq_from f).trans (hX.eq_from g).symm |
| 71 | + |
| 72 | +/-- Any two zero objects are isomorphic. -/ |
| 73 | +def iso (hX : is_zero X) (hY : is_zero Y) : X ≅ Y := |
| 74 | +{ hom := hX.to Y, |
| 75 | + inv := hX.from Y, |
| 76 | + hom_inv_id' := hX.eq_of_src _ _, |
| 77 | + inv_hom_id' := hY.eq_of_src _ _, } |
| 78 | + |
| 79 | +/-- A zero object is in particular initial. -/ |
| 80 | +protected def is_initial (hX : is_zero X) : is_initial X := |
| 81 | +@is_initial.of_unique _ _ X $ λ Y, (hX.unique_to Y).some |
| 82 | + |
| 83 | +/-- A zero object is in particular terminal. -/ |
| 84 | +protected def is_terminal (hX : is_zero X) : is_terminal X := |
| 85 | +@is_terminal.of_unique _ _ X $ λ Y, (hX.unique_from Y).some |
| 86 | + |
| 87 | +/-- The (unique) isomorphism between any initial object and the zero object. -/ |
| 88 | +def iso_is_initial (hX : is_zero X) (hY : is_initial Y) : X ≅ Y := |
| 89 | +hX.is_initial.unique_up_to_iso hY |
| 90 | + |
| 91 | +/-- The (unique) isomorphism between any terminal object and the zero object. -/ |
| 92 | +def iso_is_terminal (hX : is_zero X) (hY : is_terminal Y) : X ≅ Y := |
| 93 | +hX.is_terminal.unique_up_to_iso hY |
| 94 | + |
| 95 | +lemma of_iso (hY : is_zero Y) (e : X ≅ Y) : is_zero X := |
| 96 | +begin |
| 97 | + refine ⟨λ Z, ⟨⟨⟨e.hom ≫ hY.to Z⟩, λ f, _⟩⟩, λ Z, ⟨⟨⟨hY.from Z ≫ e.inv⟩, λ f, _⟩⟩⟩, |
| 98 | + { rw ← cancel_epi e.inv, apply hY.eq_of_src, }, |
| 99 | + { rw ← cancel_mono e.hom, apply hY.eq_of_tgt, }, |
| 100 | +end |
| 101 | + |
| 102 | +end is_zero |
| 103 | + |
| 104 | +lemma iso.is_zero_iff {X Y : C} (e : X ≅ Y) : |
| 105 | + is_zero X ↔ is_zero Y := |
| 106 | +⟨λ h, h.of_iso e.symm, λ h, h.of_iso e⟩ |
| 107 | + |
| 108 | +variables (C) |
| 109 | + |
| 110 | +/-- A category "has a zero object" if it has an object which is both initial and terminal. -/ |
| 111 | +class has_zero_object := |
| 112 | +(zero : C) |
| 113 | +(unique_to : Π X : C, unique (zero ⟶ X)) |
| 114 | +(unique_from : Π X : C, unique (X ⟶ zero)) |
| 115 | + |
| 116 | +instance has_zero_object_punit : has_zero_object (discrete punit) := |
| 117 | +{ zero := punit.star, |
| 118 | + unique_to := by tidy, |
| 119 | + unique_from := by tidy, } |
| 120 | + |
| 121 | + |
| 122 | +namespace has_zero_object |
| 123 | + |
| 124 | +variables [has_zero_object C] |
| 125 | + |
| 126 | +/-- |
| 127 | +Construct a `has_zero C` for a category with a zero object. |
| 128 | +This can not be a global instance as it will trigger for every `has_zero C` typeclass search. |
| 129 | +-/ |
| 130 | +protected def has_zero : has_zero C := |
| 131 | +{ zero := has_zero_object.zero } |
| 132 | + |
| 133 | +localized "attribute [instance] category_theory.limits.has_zero_object.has_zero" in zero_object |
| 134 | +localized "attribute [instance] category_theory.limits.has_zero_object.unique_to" in zero_object |
| 135 | +localized "attribute [instance] category_theory.limits.has_zero_object.unique_from" in zero_object |
| 136 | + |
| 137 | +lemma is_zero_zero : is_zero (0 : C) := |
| 138 | +{ unique_to := λ Y, ⟨has_zero_object.unique_to Y⟩, |
| 139 | + unique_from := λ Y, ⟨has_zero_object.unique_from Y⟩ } |
| 140 | + |
| 141 | +/-- Every zero object is isomorphic to *the* zero object. -/ |
| 142 | +def is_zero.iso_zero {X : C} (hX : is_zero X) : X ≅ 0 := |
| 143 | +hX.iso (is_zero_zero C) |
| 144 | + |
| 145 | +variables {C} |
| 146 | + |
| 147 | +@[ext] |
| 148 | +lemma to_zero_ext {X : C} (f g : X ⟶ 0) : f = g := |
| 149 | +(is_zero_zero C).eq_of_tgt _ _ |
| 150 | + |
| 151 | +@[ext] |
| 152 | +lemma from_zero_ext {X : C} (f g : 0 ⟶ X) : f = g := |
| 153 | +(is_zero_zero C).eq_of_src _ _ |
| 154 | + |
| 155 | +instance (X : C) : subsingleton (X ≅ 0) := by tidy |
| 156 | + |
| 157 | +instance {X : C} (f : 0 ⟶ X) : mono f := |
| 158 | +{ right_cancellation := λ Z g h w, by ext, } |
| 159 | + |
| 160 | +instance {X : C} (f : X ⟶ 0) : epi f := |
| 161 | +{ left_cancellation := λ Z g h w, by ext, } |
| 162 | + |
| 163 | +/-- A zero object is in particular initial. -/ |
| 164 | +def zero_is_initial : is_initial (0 : C) := |
| 165 | +is_initial.of_unique 0 |
| 166 | + |
| 167 | +/-- A zero object is in particular terminal. -/ |
| 168 | +def zero_is_terminal : is_terminal (0 : C) := |
| 169 | +is_terminal.of_unique 0 |
| 170 | + |
| 171 | +/-- A zero object is in particular initial. -/ |
| 172 | +@[priority 10] |
| 173 | +instance has_initial : has_initial C := |
| 174 | +has_initial_of_unique 0 |
| 175 | + |
| 176 | +/-- A zero object is in particular terminal. -/ |
| 177 | +@[priority 10] |
| 178 | +instance has_terminal : has_terminal C := |
| 179 | +has_terminal_of_unique 0 |
| 180 | + |
| 181 | +/-- The (unique) isomorphism between any initial object and the zero object. -/ |
| 182 | +def zero_iso_is_initial {X : C} (t : is_initial X) : 0 ≅ X := |
| 183 | +zero_is_initial.unique_up_to_iso t |
| 184 | + |
| 185 | +/-- The (unique) isomorphism between any terminal object and the zero object. -/ |
| 186 | +def zero_iso_is_terminal {X : C} (t : is_terminal X) : 0 ≅ X := |
| 187 | +zero_is_terminal.unique_up_to_iso t |
| 188 | + |
| 189 | +/-- The (unique) isomorphism between the chosen initial object and the chosen zero object. -/ |
| 190 | +def zero_iso_initial [has_initial C] : 0 ≅ ⊥_ C := |
| 191 | +zero_is_initial.unique_up_to_iso initial_is_initial |
| 192 | + |
| 193 | +/-- The (unique) isomorphism between the chosen terminal object and the chosen zero object. -/ |
| 194 | +def zero_iso_terminal [has_terminal C] : 0 ≅ ⊤_ C := |
| 195 | +zero_is_terminal.unique_up_to_iso terminal_is_terminal |
| 196 | + |
| 197 | +@[priority 100] |
| 198 | +instance has_strict_initial : initial_mono_class C := |
| 199 | +initial_mono_class.of_is_initial zero_is_initial (λ X, category_theory.mono _) |
| 200 | + |
| 201 | +open_locale zero_object |
| 202 | + |
| 203 | +end has_zero_object |
| 204 | + |
| 205 | +end category_theory.limits |
0 commit comments