/
SmallComplete.lean
77 lines (61 loc) · 2.25 KB
/
SmallComplete.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
/-
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta
-/
import Mathlib.CategoryTheory.Limits.Shapes.Products
import Mathlib.SetTheory.Cardinal.Basic
#align_import category_theory.limits.small_complete from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
/-!
# Any small complete category is a preorder
We show that any small category which has all (small) limits is a preorder: In particular, we show
that if a small category `C` in universe `u` has products of size `u`, then for any `X Y : C`
there is at most one morphism `X ⟶ Y`.
Note that in Lean, a preorder category is strictly one where the morphisms are in `Prop`, so
we instead show that the homsets are subsingleton.
## References
* https://ncatlab.org/nlab/show/complete+small+category#in_classical_logic
## Tags
small complete, preorder, Freyd
-/
namespace CategoryTheory
open Category Limits
open Cardinal
universe u
variable {C : Type u} [SmallCategory C] [HasProducts.{u} C]
/-- A small category with products is a thin category.
in Lean, a preorder category is one where the morphisms are in Prop, which is weaker than the usual
notion of a preorder/thin category which says that each homset is subsingleton; we show the latter
rather than providing a `Preorder C` instance.
-/
instance (priority := 100) : Quiver.IsThin C := fun X Y =>
⟨fun r s => by
classical
by_contra r_ne_s
have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
rw [Cardinal.two_le_iff]
exact ⟨_, _, r_ne_s⟩
let md := ΣZ W : C, Z ⟶ W
let α := #md
apply not_le_of_lt (Cardinal.cantor α)
let yp : C := ∏ fun _ : md => Y
refine' _root_.trans _ _
· exact #(X ⟶ yp)
· apply le_trans (Cardinal.power_le_power_right z)
rw [Cardinal.power_def]
apply le_of_eq
rw [Cardinal.eq]
refine' ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, _, _⟩⟩
· intro f
ext k
simp
· intro f
ext ⟨j⟩
simp
· apply Cardinal.mk_le_of_injective _
· intro f
exact ⟨_, _, f⟩
· rintro f g k
cases k
rfl⟩
end CategoryTheory