Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 78d6780

Browse files
committed
chore(category_theory/pempty): use discrete pempty instead of a special pempty category (#3191)
Use `discrete pempty` instead of a specialised `pempty` category. Motivation: Since we have a good API for `discrete` categories, there doesn't seem to be much point in defining a specialised `pempty` category with an equivalence, instead we might as well just use `discrete pempty`.
1 parent 2d270ff commit 78d6780

File tree

3 files changed

+37
-31
lines changed

3 files changed

+37
-31
lines changed

src/category_theory/limits/shapes/terminal.lean

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,26 +18,28 @@ namespace category_theory.limits
1818

1919
variables (C : Type u) [category.{v} C]
2020

21-
/-- A category has a terminal object if it has a limit over the empty diagram. -/
22-
-- Use `has_terminal_of_unique` to construct instances.
21+
/--
22+
A category has a terminal object if it has a limit over the empty diagram.
23+
Use `has_terminal_of_unique` to construct instances.
24+
-/
2325
class has_terminal :=
24-
(has_limits_of_shape : has_limits_of_shape.{v} pempty C)
25-
/-- A category has an initial object if it has a colimit over the empty diagram. -/
26-
-- Use `has_initial_of_unique` to construct instances.
26+
(has_limits_of_shape : has_limits_of_shape.{v} (discrete pempty) C)
27+
/--
28+
A category has an initial object if it has a colimit over the empty diagram.
29+
Use `has_initial_of_unique` to construct instances.
30+
-/
2731
class has_initial :=
28-
(has_colimits_of_shape : has_colimits_of_shape.{v} pempty C)
32+
(has_colimits_of_shape : has_colimits_of_shape.{v} (discrete pempty) C)
2933

3034
attribute [instance] has_terminal.has_limits_of_shape has_initial.has_colimits_of_shape
3135

3236
@[priority 100] -- see Note [lower instance priority]
3337
instance [has_finite_products.{v} C] : has_terminal.{v} C :=
34-
{ has_limits_of_shape :=
35-
{ has_limit := λ F,
36-
has_limit_of_equivalence_comp ((functor.empty.{v} (discrete pempty.{v+1})).as_equivalence.symm) } }
38+
{ has_limits_of_shape := by apply_instance }
39+
3740
@[priority 100] -- see Note [lower instance priority]
3841
instance [has_finite_coproducts.{v} C] : has_initial.{v} C :=
39-
{ has_colimits_of_shape :=
40-
{ has_colimit := λ F, has_colimit_of_equivalence_comp ((functor.empty (discrete pempty)).as_equivalence.symm) } }
42+
{ has_colimits_of_shape := by apply_instance }
4143

4244
abbreviation terminal [has_terminal.{v} C] : C := limit (functor.empty C)
4345
abbreviation initial [has_initial.{v} C] : C := colimit (functor.empty C)

src/category_theory/limits/shapes/zero.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ import category_theory.limits.shapes.binary_products
77
import category_theory.limits.shapes.images
88
import category_theory.epi_mono
99
import category_theory.punit
10+
import category_theory.discrete_category
1011

1112
/-!
1213
# Zero morphisms and zero objects
@@ -45,7 +46,7 @@ attribute [simp] has_zero_morphisms.comp_zero
4546
restate_axiom has_zero_morphisms.zero_comp'
4647
attribute [simp, reassoc] has_zero_morphisms.zero_comp
4748

48-
instance has_zero_morphisms_pempty : has_zero_morphisms.{v} pempty.{v+1} :=
49+
instance has_zero_morphisms_pempty : has_zero_morphisms.{v} (discrete pempty.{v+1}) :=
4950
{ has_zero := by tidy }
5051

5152
instance has_zero_morphisms_punit : has_zero_morphisms.{v} punit.{v+1} :=

src/category_theory/pempty.lean

Lines changed: 22 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
/-
22
Copyright (c) 2018 Scott Morrison. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
4-
Authors: Scott Morrison
4+
Authors: Scott Morrison, Bhavik Mehta.
55
-/
66
import category_theory.discrete_category
77

@@ -14,29 +14,32 @@ Defines a category structure on `pempty`, and the unique functor `pempty ⥤ C`
1414
universes v u w -- declare the `v`'s first; see `category_theory.category` for an explanation
1515

1616
namespace category_theory
17-
18-
/-- The empty category -/
19-
instance pempty_category : small_category.{w} pempty.{w+1} :=
20-
{ hom := λ X Y, pempty,
21-
id := by obviously,
22-
comp := by obviously }
23-
2417
namespace functor
18+
2519
variables (C : Type u) [category.{v} C]
2620

27-
/-- The unique functor from the empty category to any target category. -/
28-
def empty : pempty.{v+1} ⥤ C := by tidy
21+
/-- The canonical functor out of the empty category. -/
22+
def empty : discrete pempty.{v+1} ⥤ C := discrete.functor pempty.elim
2923

30-
/-- The natural isomorphism between any two functors out of the empty category. -/
31-
@[simps]
32-
def empty_ext (F G : pempty.{v+1} ⥤ C) : F ≅ G :=
33-
{ hom := { app := λ j, by cases j },
34-
inv := { app := λ j, by cases j } }
24+
variable {C}
25+
/-- Any two functors out of the empty category are isomorphic. -/
26+
def empty_ext (F G : discrete pempty.{v+1} ⥤ C) : F ≅ G :=
27+
discrete.nat_iso (λ x, pempty.elim x)
3528

36-
end functor
29+
/--
30+
Any functor out of the empty category is isomorphic to the canonical functor from the empty
31+
category.
32+
-/
33+
def unique_from_empty (F : discrete pempty.{v+1} ⥤ C) : F ≅ empty C :=
34+
empty_ext _ _
35+
36+
/--
37+
Any two functors out of the empty category are *equal*. You probably want to use
38+
`empty_ext` instead of this.
39+
-/
40+
lemma empty_ext' (F G : discrete pempty.{v+1} ⥤ C) : F = G :=
41+
functor.ext (λ x, x.elim) (λ x _ _, x.elim)
3742

38-
/-- The category `pempty` is equivalent to the category `discrete pempty`. -/
39-
instance pempty_equiv_discrete_pempty : is_equivalence (functor.empty.{v} (discrete pempty.{v+1})) :=
40-
by obviously
43+
end functor
4144

4245
end category_theory

0 commit comments

Comments
 (0)