-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathInducedLimitFunctors.v
171 lines (151 loc) · 6.75 KB
/
InducedLimitFunctors.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
Require Export LimitFunctorTheorems SpecializedLaxCommaCategory.
Require Import Common DefinitionSimplification SpecializedCategory Functor NaturalTransformation Duals CanonicalStructureSimplification.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Section InducedFunctor.
(* The components of the functor can be useful even if we don't have
a category that we're coming from. So prove them separately, so
we can use them elsewhere, without assuming a full [HasLimits]. *)
Variable I : Type.
Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
Local Coercion Index2Cat : I >-> SpecializedCategory.
Local Notation "'CAT' ⇑ D" := (@LaxCosliceSpecializedCategory _ _ Index2Cat _ D).
Local Notation "'CAT' ⇓ D" := (@LaxSliceSpecializedCategory _ _ Index2Cat _ D).
Context `(D : @SpecializedCategory objD).
Let DOp := OppositeCategory D.
Section Limit.
Definition InducedLimitFunctor_MorphismOf (s d : CAT ⇑ D) (limS : Limit (projT2 s)) (limD : Limit (projT2 d))
(m : Morphism (CAT ⇑ D) s d) :
Morphism D (LimitObject limS) (LimitObject limD)
:= InducedLimitMap (projT2 m) _ _.
Lemma InducedLimitFunctor_FCompositionOf (s d d' : CAT ⇑ D) (limS : Limit (projT2 s)) (limD : Limit (projT2 d)) (limD' : Limit (projT2 d'))
(m1 : Morphism _ s d) (m2 : Morphism _ d d') :
InducedLimitFunctor_MorphismOf limS limD' (Compose m2 m1) =
Compose (InducedLimitFunctor_MorphismOf limD limD' m2) (InducedLimitFunctor_MorphismOf limS limD m1).
Proof.
unfold InducedLimitFunctor_MorphismOf.
unfold InducedLimitMap at 1; cbv zeta.
match goal with
| [ |- TerminalProperty_Morphism ?a ?b ?c = _ ] => apply (proj2 (TerminalProperty a b c))
end (* 3 s *).
nt_eq (* 4 s *).
rsimplify_morphisms (* 11 s *).
repeat rewrite Associativity (* 3 s *).
match goal with
| [ |- Compose ?a (Compose ?b ?c) = Compose ?a' (Compose ?b' ?c') ] =>
eapply (@eq_trans _ _ (Compose a' (Compose _ c)) _);
try_associativity ltac:(apply f_equal2; try reflexivity)
end (* 13 s *);
unfold InducedLimitMap;
match goal with
| [ |- appcontext[TerminalProperty_Morphism ?a ?b ?c] ] =>
let H := constr:(TerminalProperty a) in
let H' := fresh in
pose proof (fun x Y f => f_equal (fun T => T.(ComponentsOf) x) (proj1 (H Y f))) as H';
simpl in H';
unfold Object, Morphism in *;
simpl in *;
rewrite H';
clear H'
end (* 7 s *);
simpl;
rsimplify_morphisms;
reflexivity (* 6 s since [simpl] *).
Qed.
Lemma InducedLimitFunctor_FIdentityOf (x : CAT ⇑ D) (limX : Limit (projT2 x)) :
InducedLimitFunctor_MorphismOf limX limX (Identity x) =
Identity (LimitObject limX).
Proof.
unfold InducedLimitFunctor_MorphismOf.
unfold InducedLimitMap at 1; cbv zeta.
match goal with
| [ |- TerminalProperty_Morphism ?a ?b ?c = _ ] => apply (proj2 (TerminalProperty a b c))
end (* 3 s *).
nt_eq (* 4 s *).
rsimplify_morphisms;
reflexivity. (* 2 s *)
Qed.
Variable HasLimits : forall C : CAT ⇑ D, Limit (projT2 C).
Hint Resolve InducedLimitFunctor_FCompositionOf InducedLimitFunctor_FIdentityOf.
Definition InducedLimitFunctor : SpecializedFunctor (CAT ⇑ D) D.
match goal with
| [ |- SpecializedFunctor ?C ?D ] =>
refine (Build_SpecializedFunctor C D
(fun x => LimitObject (HasLimits x))
(fun s d => @InducedLimitFunctor_MorphismOf s d (HasLimits s) (HasLimits d))
_
_
)
end;
abstract trivial.
Defined.
End Limit.
Section Colimit.
Definition InducedColimitFunctor_MorphismOf (s d : CAT ⇓ D) (colimS : Colimit (projT2 s)) (colimD : Colimit (projT2 d))
(m : Morphism (CAT ⇓ D) s d) :
Morphism D (ColimitObject colimS) (ColimitObject colimD)
:= InducedColimitMap (projT2 m) _ _.
Lemma InducedColimitFunctor_FCompositionOf (s d d' : CAT ⇓ D) (colimS : Colimit (projT2 s)) (colimD : Colimit (projT2 d)) (colimD' : Colimit (projT2 d'))
(m1 : Morphism _ s d) (m2 : Morphism _ d d') :
InducedColimitFunctor_MorphismOf colimS colimD' (Compose m2 m1) =
Compose (InducedColimitFunctor_MorphismOf colimD colimD' m2) (InducedColimitFunctor_MorphismOf colimS colimD m1).
Proof.
unfold InducedColimitFunctor_MorphismOf.
unfold InducedColimitMap at 1; cbv zeta.
match goal with
| [ |- InitialProperty_Morphism ?a ?b ?c = _ ] => apply (proj2 (InitialProperty a b c))
end (* 3 s *).
nt_eq (* 4 s *).
rsimplify_morphisms (* 8 s *).
repeat rewrite Associativity (* 3 s *).
match goal with
| [ |- Compose ?a (Compose ?b ?c) = Compose ?a' (Compose ?b' ?c') ] =>
symmetry; eapply (@eq_trans _ _ (Compose a (Compose _ c')) _);
try_associativity ltac:(apply f_equal2; try reflexivity)
end (* 13 s *);
unfold InducedColimitMap;
match goal with
| [ |- appcontext[InitialProperty_Morphism ?a ?b ?c] ] =>
let H := constr:(InitialProperty a) in
let H' := fresh in
pose proof (fun x Y f => f_equal (fun T => T.(ComponentsOf) x) (proj1 (H Y f))) as H';
simpl in H';
unfold Object in *;
simpl in *;
try (rewrite H'; clear H')
end (* 7 s *);
simpl;
rsimplify_morphisms;
reflexivity (* 4 s since [simpl] *).
Qed.
Lemma InducedColimitFunctor_FIdentityOf (x : CAT ⇓ D) (colimX : Colimit (projT2 x)) :
InducedColimitFunctor_MorphismOf colimX colimX (Identity x) =
Identity (ColimitObject colimX).
Proof.
unfold InducedColimitFunctor_MorphismOf.
unfold InducedColimitMap at 1; cbv zeta.
match goal with
| [ |- InitialProperty_Morphism ?a ?b ?c = _ ] => apply (proj2 (InitialProperty a b c))
end (* 3 s *).
nt_eq (* 4 s *).
rsimplify_morphisms. (* 1.5 s *)
reflexivity.
Qed.
Variable HasColimits : forall C : CAT ⇓ D, Colimit (projT2 C).
Hint Resolve InducedColimitFunctor_FCompositionOf InducedColimitFunctor_FIdentityOf.
Definition InducedColimitFunctor : SpecializedFunctor (CAT ⇓ D) D.
match goal with
| [ |- SpecializedFunctor ?C ?D ] =>
refine (Build_SpecializedFunctor C D
(fun x => ColimitObject (HasColimits x))
(fun s d => @InducedColimitFunctor_MorphismOf s d (HasColimits s) (HasColimits d))
_
_
)
end;
abstract trivial.
Defined.
End Colimit.
End InducedFunctor.