-
Notifications
You must be signed in to change notification settings - Fork 297
/
yoneda.lean
157 lines (131 loc) · 5.48 KB
/
yoneda.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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Bhavik Mehta
-/
import category_theory.limits.functor_category
import tactic.assert_exists
/-!
# Limit properties relating to the (co)yoneda embedding.
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
We calculate the colimit of `Y ↦ (X ⟶ Y)`, which is just `punit`.
(This is used in characterising cofinal functors.)
We also show the (co)yoneda embeddings preserve limits and jointly reflect them.
-/
open opposite
open category_theory
open category_theory.limits
universes w v u
namespace category_theory
namespace coyoneda
variables {C : Type v} [small_category C]
/--
The colimit cocone over `coyoneda.obj X`, with cocone point `punit`.
-/
@[simps]
def colimit_cocone (X : Cᵒᵖ) : cocone (coyoneda.obj X) :=
{ X := punit,
ι := { app := by tidy, } }
/--
The proposed colimit cocone over `coyoneda.obj X` is a colimit cocone.
-/
@[simps]
def colimit_cocone_is_colimit (X : Cᵒᵖ) : is_colimit (colimit_cocone X) :=
{ desc := λ s x, s.ι.app (unop X) (𝟙 _),
fac' := λ s Y, by { ext f, convert congr_fun (s.w f).symm (𝟙 (unop X)), simp, },
uniq' := λ s m w, by { ext ⟨⟩, rw ← w, simp, } }
instance (X : Cᵒᵖ) : has_colimit (coyoneda.obj X) :=
has_colimit.mk { cocone := _, is_colimit := colimit_cocone_is_colimit X }
/--
The colimit of `coyoneda.obj X` is isomorphic to `punit`.
-/
noncomputable
def colimit_coyoneda_iso (X : Cᵒᵖ) : colimit (coyoneda.obj X) ≅ punit :=
colimit.iso_colimit_cocone { cocone := _, is_colimit := colimit_cocone_is_colimit X }
end coyoneda
variables {C : Type u} [category.{v} C]
open limits
/-- The yoneda embedding `yoneda.obj X : Cᵒᵖ ⥤ Type v` for `X : C` preserves limits. -/
instance yoneda_preserves_limits (X : C) : preserves_limits (yoneda.obj X) :=
{ preserves_limits_of_shape := λ J 𝒥, by exactI
{ preserves_limit := λ K,
{ preserves := λ c t,
{ lift := λ s x, quiver.hom.unop (t.lift ⟨op X, λ j, (s.π.app j x).op, λ j₁ j₂ α, _⟩),
fac' := λ s j, funext $ λ x, quiver.hom.op_inj (t.fac _ _),
uniq' := λ s m w, funext $ λ x,
begin
refine quiver.hom.op_inj (t.uniq ⟨op X, _, _⟩ _ (λ j, _)),
{ dsimp, simp [← s.w α] }, -- See library note [dsimp, simp]
{ exact quiver.hom.unop_inj (congr_fun (w j) x) },
end } } } }
/-- The coyoneda embedding `coyoneda.obj X : C ⥤ Type v` for `X : Cᵒᵖ` preserves limits. -/
instance coyoneda_preserves_limits (X : Cᵒᵖ) : preserves_limits (coyoneda.obj X) :=
{ preserves_limits_of_shape := λ J 𝒥, by exactI
{ preserves_limit := λ K,
{ preserves := λ c t,
{ lift := λ s x, t.lift ⟨unop X, λ j, s.π.app j x, λ j₁ j₂ α, by { dsimp, simp [← s.w α]}⟩,
-- See library note [dsimp, simp]
fac' := λ s j, funext $ λ x, t.fac _ _,
uniq' := λ s m w, funext $ λ x,
begin
refine (t.uniq ⟨unop X, _⟩ _ (λ j, _)),
exact congr_fun (w j) x,
end } } } }
/-- The yoneda embeddings jointly reflect limits. -/
def yoneda_jointly_reflects_limits (J : Type w) [small_category J] (K : J ⥤ Cᵒᵖ) (c : cone K)
(t : Π (X : C), is_limit ((yoneda.obj X).map_cone c)) : is_limit c :=
let s' : Π (s : cone K), cone (K ⋙ yoneda.obj s.X.unop) :=
λ s, ⟨punit, λ j _, (s.π.app j).unop, λ j₁ j₂ α, funext $ λ _, quiver.hom.op_inj (s.w α).symm⟩
in
{ lift := λ s, ((t s.X.unop).lift (s' s) punit.star).op,
fac' := λ s j, quiver.hom.unop_inj (congr_fun ((t s.X.unop).fac (s' s) j) punit.star),
uniq' := λ s m w,
begin
apply quiver.hom.unop_inj,
suffices : (λ (x : punit), m.unop) = (t s.X.unop).lift (s' s),
{ apply congr_fun this punit.star },
apply (t _).uniq (s' s) _ (λ j, _),
ext,
exact quiver.hom.op_inj (w j),
end }
/-- The coyoneda embeddings jointly reflect limits. -/
def coyoneda_jointly_reflects_limits (J : Type w) [small_category J] (K : J ⥤ C) (c : cone K)
(t : Π (X : Cᵒᵖ), is_limit ((coyoneda.obj X).map_cone c)) : is_limit c :=
let s' : Π (s : cone K), cone (K ⋙ coyoneda.obj (op s.X)) :=
λ s, ⟨punit, λ j _, s.π.app j, λ j₁ j₂ α, funext $ λ _, (s.w α).symm⟩
in
{ lift := λ s, (t (op s.X)).lift (s' s) punit.star,
fac' := λ s j, congr_fun ((t _).fac (s' s) j) punit.star,
uniq' := λ s m w,
begin
suffices : (λ (x : punit), m) = (t _).lift (s' s),
{ apply congr_fun this punit.star },
apply (t _).uniq (s' s) _ (λ j, _),
ext,
exact (w j),
end }
variables {D : Type u} [small_category D]
instance yoneda_functor_preserves_limits : preserves_limits (@yoneda D _) :=
begin
apply preserves_limits_of_evaluation,
intro K,
change preserves_limits (coyoneda.obj K),
apply_instance
end
instance coyoneda_functor_preserves_limits : preserves_limits (@coyoneda D _) :=
begin
apply preserves_limits_of_evaluation,
intro K,
change preserves_limits (yoneda.obj K),
apply_instance
end
instance yoneda_functor_reflects_limits : reflects_limits (@yoneda D _) :=
limits.fully_faithful_reflects_limits _
instance coyoneda_functor_reflects_limits : reflects_limits (@coyoneda D _) :=
limits.fully_faithful_reflects_limits _
end category_theory
-- We don't need to have developed any algebra or set theory to reach (at least) this point
-- in the category theory hierarchy.
assert_not_exists set.range
assert_not_exists add_comm_monoid