1 Generalizable All Variables.
2 Require Import Notations.
3 Require Import Categories_ch1_3.
4 Require Import Functors_ch1_4.
5 Require Import Isomorphisms_ch1_5.
6 Require Import InitialTerminal_ch2_2.
7 Require Import Subcategories_ch7_1.
8 Require Import NaturalTransformations_ch7_4.
9 Require Import NaturalIsomorphisms_ch7_5.
10 Require Import Coherence_ch7_8.
11 Require Import BinoidalCategories.
12 Require Import PreMonoidalCategories.
13 Require Import MonoidalCategories_ch7_8.
15 (******************************************************************************)
16 (* Facts about the center of a Binoidal or PreMonoidal Category *)
17 (******************************************************************************)
19 Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
20 : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
22 apply Build_CentralMorphism; intros.
23 abstract (setoid_rewrite <- (fmor_preserves_comp(bin_first c0));
24 setoid_rewrite associativity;
25 setoid_rewrite centralmor_first;
26 setoid_rewrite <- associativity;
27 setoid_rewrite centralmor_first;
28 setoid_rewrite associativity;
29 setoid_rewrite <- (fmor_preserves_comp(bin_first d));
31 abstract (setoid_rewrite <- (fmor_preserves_comp(bin_second d));
32 setoid_rewrite <- associativity;
33 setoid_rewrite centralmor_second;
34 setoid_rewrite associativity;
35 setoid_rewrite centralmor_second;
36 setoid_rewrite <- associativity;
37 setoid_rewrite <- (fmor_preserves_comp(bin_second c0));
41 (* the central morphisms of a category constitute a subcategory *)
42 Definition Center `(bc:BinoidalCat) : WideSubcategory bc (fun _ _ f => CentralMorphism f).
43 apply Build_WideSubcategory; intros.
44 apply Build_CentralMorphism; intros.
45 abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
46 setoid_rewrite (fmor_preserves_id(bin_first d));
47 setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
48 abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
49 setoid_rewrite (fmor_preserves_id(bin_second d));
50 setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
51 apply central_morphisms_compose; auto.
54 (* if one half of an iso is central, so is the other half *)
55 Lemma iso_central_both `{C:BinoidalCat}{a b:C}(i:a ≅ b) : CentralMorphism #i -> CentralMorphism #i⁻¹.
57 apply Build_CentralMorphism; intros; simpl.
61 setoid_rewrite associativity.
62 setoid_replace (id (a ⊗ d)) with ((#i >>> iso_backward i) ⋉ d).
63 setoid_rewrite <- fmor_preserves_comp.
64 setoid_rewrite <- associativity.
65 setoid_rewrite juggle3.
66 setoid_rewrite <- (centralmor_first(CentralMorphism:=cm)).
67 setoid_rewrite <- associativity.
68 setoid_rewrite (fmor_preserves_comp (-⋉c)).
69 apply comp_respects; try reflexivity.
70 etransitivity; [ idtac | apply left_identity ].
71 apply comp_respects; try reflexivity.
72 etransitivity; [ idtac | apply (fmor_preserves_id (-⋉c)) ].
73 apply (fmor_respects (-⋉c)).
76 etransitivity; [ idtac | apply (fmor_preserves_id (-⋉d)) ].
77 apply (fmor_respects (-⋉d)).
83 setoid_replace (id (c ⊗ b)) with (c ⋊ (iso_backward i >>> #i)).
84 setoid_rewrite <- fmor_preserves_comp.
85 setoid_rewrite juggle3.
86 setoid_rewrite <- (centralmor_second(CentralMorphism:=cm)).
87 setoid_rewrite associativity.
88 apply comp_respects; try reflexivity.
89 setoid_rewrite associativity.
90 setoid_rewrite (fmor_preserves_comp (d⋊-)).
91 etransitivity; [ idtac | apply right_identity ].
92 apply comp_respects; try reflexivity.
93 etransitivity; [ idtac | apply (fmor_preserves_id (d⋊-)) ].
94 apply (fmor_respects (d⋊-)).
97 etransitivity; [ idtac | apply (fmor_preserves_id (c⋊-)) ].
98 apply (fmor_respects (c⋊-)).
102 Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
104 apply Build_CentralMorphism; simpl; intros.
106 set (ni_commutes (pmon_assoc_rr c c0) f) as q.
107 apply iso_shift_right' in q.
108 unfold fmor in q at 1; simpl in q.
112 set (ni_commutes (pmon_assoc_rr c d) f) as q.
113 apply iso_shift_right' in q.
114 unfold fmor in q at 1; simpl in q.
118 set (ni_commutes (pmon_assoc_ll b c) g) as q.
120 apply iso_shift_left' in q.
124 setoid_rewrite pmon_coherent_r at 1.
125 setoid_rewrite pmon_coherent_l at 1.
126 setoid_rewrite juggle3.
127 setoid_rewrite juggle3.
128 set (@iso_comp2 _ _ _ _ _ ((pmon_assoc b c0) c)) as q.
131 setoid_rewrite right_identity.
134 setoid_rewrite (centralmor_first(CentralMorphism:=cm)).
136 repeat setoid_rewrite <- associativity.
138 apply comp_respects; [ idtac | reflexivity ].
139 set (ni_commutes (pmon_assoc_ll a c) g) as q.
141 apply iso_shift_left' in q.
144 repeat setoid_rewrite associativity.
145 setoid_rewrite pmon_coherent_l.
146 set (pmon_coherent_l(PreMonoidalCat:=C) c a d) as q.
147 apply isos_forward_equal_then_backward_equal in q.
150 setoid_rewrite <- pmon_coherent_r.
151 setoid_rewrite iso_comp1.
152 setoid_rewrite right_identity.
153 unfold fmor at 3; simpl.
154 apply comp_respects; [ idtac | reflexivity ].
156 set (pmon_coherent_r a c c0) as q.
157 apply isos_forward_equal_then_backward_equal in q.
158 setoid_rewrite iso_inv_inv in q.
161 setoid_rewrite pmon_coherent_r.
164 set (@isos_forward_equal_then_backward_equal) as q.
165 unfold iso_inv in q; simpl in q.
167 apply pmon_coherent_l.
171 set (ni_commutes (pmon_assoc_rr a c) g) as q.
173 apply iso_shift_left' in q.
174 unfold fmor in q at 2.
179 set (ni_commutes (pmon_assoc d c) f) as q.
180 apply iso_shift_right' in q.
181 unfold fmor in q at 1; simpl in q.
185 set (pmon_coherent_r d a c) as q.
186 apply isos_forward_equal_then_backward_equal in q.
187 rewrite iso_inv_inv in q.
188 unfold iso_inv in q; simpl in q.
192 setoid_rewrite juggle3.
193 set (iso_comp1 ((pmon_assoc d c) a)) as q.
196 setoid_rewrite right_identity.
198 set (ni_commutes (pmon_assoc_rr b c) g) as q.
200 apply iso_shift_left' in q.
201 unfold fmor in q at 2.
206 set (ni_commutes (pmon_assoc c0 c) f) as q.
207 unfold fmor in q; simpl in q.
208 apply iso_shift_right' in q.
212 set (pmon_coherent_r c0 b c) as q.
216 setoid_rewrite juggle3.
217 setoid_rewrite juggle3.
218 set (iso_comp1 ((pmon_assoc c0 c) b)) as q.
221 setoid_rewrite right_identity.
223 setoid_rewrite pmon_coherent_r.
224 repeat setoid_rewrite associativity.
225 apply comp_respects; [ reflexivity | idtac ].
226 repeat setoid_rewrite <- associativity.
228 setoid_rewrite (fmor_preserves_comp (-⋉c)).
229 apply (fmor_respects (-⋉c)).
230 apply centralmor_second.
231 set (pmon_coherent_r d b c) as q.
232 apply isos_forward_equal_then_backward_equal in q.
233 rewrite iso_inv_inv in q.
238 Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f).
240 apply Build_CentralMorphism; simpl; intros.
242 set (ni_commutes (pmon_assoc_ll c a) g) as q.
244 apply iso_shift_left' in q.
245 unfold fmor in q at 2.
250 set (ni_commutes (pmon_assoc c d) f) as q.
252 apply iso_shift_left' in q.
253 unfold fmor in q at 1; simpl in q.
257 rewrite <- pmon_coherent_l.
258 setoid_rewrite <- associativity.
259 setoid_rewrite juggle3.
260 set (iso_comp2 ((pmon_assoc_ll c a) d)) as q.
262 setoid_rewrite right_identity.
265 set (ni_commutes (pmon_assoc_ll c b) g) as q.
267 apply iso_shift_left' in q.
268 unfold fmor in q at 1; simpl in q.
272 set (ni_commutes (pmon_assoc c c0) f) as q.
273 unfold fmor in q; simpl in q.
275 apply iso_shift_left' in q.
279 rewrite pmon_coherent_l.
280 setoid_rewrite <- associativity.
281 setoid_rewrite juggle3.
282 set (iso_comp2 ((pmon_assoc c c0) b)) as q.
284 setoid_rewrite right_identity.
286 setoid_rewrite pmon_coherent_l.
288 repeat setoid_rewrite associativity.
289 apply comp_respects; [ reflexivity | idtac ].
290 repeat setoid_rewrite <- associativity.
292 setoid_rewrite (fmor_preserves_comp (c⋊-)).
293 apply (fmor_respects (c⋊-)).
294 apply centralmor_first.
295 set (pmon_coherent_l b c d) as q.
296 apply isos_forward_equal_then_backward_equal in q.
300 set (ni_commutes (pmon_assoc_ll d c) f) as q.
301 apply iso_shift_right' in q.
302 unfold fmor in q at 1; simpl in q.
306 set (ni_commutes (pmon_assoc_rr c a) g) as q.
308 unfold fmor in q at 2; simpl in q.
309 apply iso_shift_left' in q.
313 setoid_rewrite juggle3.
314 set (pmon_coherent_r d c a) as q.
315 apply isos_forward_equal_then_backward_equal in q.
316 setoid_rewrite iso_inv_inv in q.
319 setoid_rewrite <- pmon_coherent_l.
320 set (iso_comp1 (((pmon_assoc_ll d c) a))) as q.
323 setoid_rewrite right_identity.
324 setoid_rewrite juggle3.
325 setoid_rewrite (centralmor_second(CentralMorphism:=cm)).
327 apply iso_shift_left.
328 setoid_rewrite pmon_coherent_r.
329 set (pmon_coherent_l c d b) as q.
330 apply isos_forward_equal_then_backward_equal in q.
333 apply iso_shift_right.
334 setoid_rewrite iso_inv_inv.
335 repeat setoid_rewrite <- associativity.
337 set (ni_commutes (pmon_assoc_ll c0 c) f) as x.
338 setoid_rewrite <- pmon_coherent_l.
340 unfold fmor in x at 2; simpl in x.
344 set (ni_commutes (pmon_assoc_rr c b) g) as x.
346 unfold fmor in x at 2; simpl in x.
347 setoid_rewrite pmon_coherent_l.
348 setoid_rewrite <- pmon_coherent_r.
349 repeat setoid_rewrite associativity.
352 setoid_rewrite <- associativity.
353 setoid_rewrite juggle3.
354 setoid_rewrite pmon_coherent_r.
355 set (iso_comp1 ((pmon_assoc c0 b) c)) as x.
358 setoid_rewrite right_identity.
362 Section Center_is_Monoidal.
364 Context `(pm:PreMonoidalCat(I:=pmI)).
366 Definition Center_is_Binoidal : BinoidalCat (Center pm) bin_obj'.
367 apply PreMonoidalWideSubcategory_is_Binoidal.
368 intros; apply first_preserves_centrality; auto.
369 intros; apply second_preserves_centrality; auto.
372 Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal pmI.
373 apply PreMonoidalWideSubcategory_PreMonoidal; intros.
374 apply pmon_assoc_central.
375 apply iso_central_both; apply pmon_assoc_central.
376 apply pmon_cancell_central.
377 apply iso_central_both; apply pmon_cancell_central.
378 apply pmon_cancelr_central.
379 apply iso_central_both; apply pmon_cancelr_central.
382 Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal.
383 apply Build_MonoidalCat.
384 apply Build_CommutativeCat.
386 apply Build_CentralMorphism; unfold hom;
387 intros; destruct f; destruct g; simpl in *.
388 apply (centralmor_second(CentralMorphism:=c1)).
389 apply (centralmor_second(CentralMorphism:=c0)).
392 End Center_is_Monoidal.