-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathLimits.v
186 lines (155 loc) · 7.02 KB
/
Limits.v
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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
Require Export SpecializedCategory Functor UniversalProperties.
Require Import Common FunctorCategory NaturalTransformation.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Local Open Scope category_scope.
Section DiagonalFunctor.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
(**
Quoting Dwyer and Spalinski:
There is a diagonal or ``constant diagram'' functor
Δ : C -> C^D,
which carries an object [X : C] to the constant functor [Δ X : D -> C] (by definition,
this ``constant functor'' sends each object of [D] to [X] and each morphism of [D]
to [Identity X]). The functor Δ assigns to each morphism [f : X -> X'] of [C] the constant
natural transformation [t(f) : Δ X -> Δ X'] determined by the formula [t(f) d = f] for
each object [d] of [D].
**)
Definition diagonal_functor_object_of (c : C) : C ^ D.
refine {| ObjectOf := fun _ => c;
MorphismOf := (fun _ _ _ => Identity c)
|}; abstract t.
Defined.
Definition diagonal_functor_morphism_of o1 o2 : C.(Morphism) o1 o2 -> (C ^ D).(Morphism) (diagonal_functor_object_of o1) (diagonal_functor_object_of o2).
simpl; unfold diagonal_functor_object_of; intro m.
hnf.
match goal with
| [ |- SpecializedNaturalTransformation ?F ?G ] =>
refine (Build_SpecializedNaturalTransformation F G
(fun d => m : C.(Morphism) ((diagonal_functor_object_of o1) d) ((diagonal_functor_object_of o2) d))
_
)
end;
simpl; abstract (intros; autorewrite with morphism; trivial).
Defined.
Definition DiagonalFunctor' : SpecializedFunctor C (C ^ D).
match goal with
| [ |- SpecializedFunctor ?C ?D ] =>
refine (Build_SpecializedFunctor C D
diagonal_functor_object_of
diagonal_functor_morphism_of
_
_
)
end;
abstract nt_eq.
Defined.
Definition DiagonalFunctor := Eval cbv beta iota zeta delta [DiagonalFunctor' diagonal_functor_object_of (*diagonal_functor_morphism_of*)] in DiagonalFunctor'.
End DiagonalFunctor.
Section DiagonalFunctorLemmas.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Context `(D' : @SpecializedCategory objD').
Lemma Compose_DiagonalFunctor x (F : SpecializedFunctor D' D) :
ComposeFunctors (DiagonalFunctor C D x) F = DiagonalFunctor _ _ x.
functor_eq.
Qed.
Definition Compose_DiagonalFunctor_NT x (F : SpecializedFunctor D' D) :
SpecializedNaturalTransformation (ComposeFunctors (DiagonalFunctor C D x) F) (DiagonalFunctor _ _ x)
:= Build_SpecializedNaturalTransformation (ComposeFunctors (DiagonalFunctor C D x) F)
(DiagonalFunctor _ _ x)
(fun z => Identity x)
(fun _ _ _ => eq_refl).
End DiagonalFunctorLemmas.
Hint Rewrite @Compose_DiagonalFunctor.
Section Limit.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Variable F : SpecializedFunctor D C.
(**
Quoting Dwyer and Spalinski:
Let [D] be a small category and [F : D -> C] a functor. A limit
for [F] is an object [L] of [C] together with a natural transformation [t : Δ L -> F]
such that for every object [X] of [C] and every natural transformation [s : Δ X -> F],
there exists a unique map [s' : X -> L] in [C] such that [t (Δ s') = s].
**)
Definition Limit := TerminalMorphism (DiagonalFunctor C D) F.
Definition IsLimit := IsTerminalMorphism (U := DiagonalFunctor C D) (X := F).
(* Definition Limit (L : C) :=
{ t : SmallSpecializedNaturalTransformation ((DiagonalFunctor C D) L) F &
forall X : C, forall s : SmallSpecializedNaturalTransformation ((DiagonalFunctor C D) X) F,
{ s' : C.(Morphism) X L |
unique
(fun s' => SNTComposeT t ((DiagonalFunctor C D).(MorphismOf) s') = s)
s'
}
}.*)
(**
Quoting Dwyer and Spalinski:
Let [D] be a small category and [F : D -> C] a functor. A colimit
for [F] is an object [c] of [C] together with a natural transformation [t : F -> Δ c]
such that for every object [X] of [C] and every natural transformation [s : F -> Δ X],
there exists a unique map [s' : c -> X] in [C] such that [(Δ s') t = s].
**)
Definition Colimit := @InitialMorphism (C ^ D) _ F (DiagonalFunctor C D).
Definition IsColimit := @IsInitialMorphism (C ^ D) _ F (DiagonalFunctor C D).
(* Definition Colimit (c : C) :=
{ t : SmallSpecializedNaturalTransformation F ((DiagonalFunctor C D) c) &
forall X : C, forall s : SmallSpecializedNaturalTransformation F ((DiagonalFunctor C D) X),
{ s' : C.(Morphism) c X | is_unique s' /\
SNTComposeT ((DiagonalFunctor C D).(MorphismOf) s') t = s
}
}.*)
Section coercions.
Definition Limit_IsLimit : forall o : Limit, IsLimit o
:= fun o => TerminalMorphism_IsTerminalMorphism o.
Definition IsLimit_Limit : forall o, IsLimit o -> Limit
:= fun o H => IsTerminalMorphism_TerminalMorphism H.
Global Coercion Limit_IsLimit : Limit >-> IsLimit.
Global Coercion IsLimit_Limit : IsLimit >-> Limit.
Definition Colimit_IsColimit : forall o : Colimit, IsColimit o
:= fun o => InitialMorphism_IsInitialMorphism o.
Definition IsColimit_Colimit : forall o, IsColimit o -> Colimit
:= fun o H => IsInitialMorphism_InitialMorphism H.
Global Coercion Colimit_IsColimit : Colimit >-> IsColimit.
Global Coercion IsColimit_Colimit : IsColimit >-> Colimit.
End coercions.
Section AbstractionBarrier.
Variable l : Limit.
Variable c : Colimit.
Definition LimitObject := TerminalMorphism_Object l.
Definition LimitMorphism := TerminalMorphism_Morphism l.
Definition LimitProperty_Morphism := TerminalProperty_Morphism l.
Definition LimitProperty := TerminalProperty l.
Definition ColimitObject := InitialMorphism_Object c.
Definition ColimitMorphism := InitialMorphism_Morphism c.
Definition ColimitProperty_Morphism := InitialProperty_Morphism c.
Definition ColimitProperty := InitialProperty c.
End AbstractionBarrier.
End Limit.
Section LimitMorphisms.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Variable F : SpecializedFunctor D C.
Definition MorphismBetweenLimits (L L' : Limit F) : C.(Morphism) (LimitObject L) (LimitObject L').
unfold Limit, LimitObject in *.
intro_universal_morphisms.
intro_universal_property_morphisms.
match goal with
| [ |- Morphism _ ?a ?b ] => pose a; pose b
end.
specialized_assumption idtac.
Defined.
Definition MorphismBetweenColimits (c c' : Colimit F) : C.(Morphism) (ColimitObject c) (ColimitObject c').
unfold Colimit, ColimitObject in *.
intro_universal_morphisms.
intro_universal_property_morphisms.
match goal with
| [ |- Morphism _ ?a ?b ] => pose a; pose b
end.
specialized_assumption idtac.
Defined.
End LimitMorphisms.