1 Generalizable All Variables.
2 Require Import Preamble.
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_SubCategory; 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 Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
56 apply Build_CentralMorphism; simpl; intros.
58 set (ni_commutes (pmon_assoc_rr c c0) f) as q.
59 apply iso_shift_right' in q.
60 unfold fmor in q at 1; simpl in q.
64 set (ni_commutes (pmon_assoc_rr c d) f) as q.
65 apply iso_shift_right' in q.
66 unfold fmor in q at 1; simpl in q.
70 set (ni_commutes (pmon_assoc_ll b c) g) as q.
72 apply iso_shift_left' in q.
76 setoid_rewrite pmon_coherent_r at 1.
77 setoid_rewrite pmon_coherent_l at 1.
78 setoid_rewrite juggle3.
79 setoid_rewrite juggle3.
80 set (@iso_comp2 _ _ _ _ _ ((pmon_assoc b c0) c)) as q.
83 setoid_rewrite right_identity.
86 setoid_rewrite (centralmor_first(CentralMorphism:=cm)).
88 repeat setoid_rewrite <- associativity.
90 apply comp_respects; [ idtac | reflexivity ].
91 set (ni_commutes (pmon_assoc_ll a c) g) as q.
93 apply iso_shift_left' in q.
96 repeat setoid_rewrite associativity.
97 setoid_rewrite pmon_coherent_l.
98 set (pmon_coherent_l(PreMonoidalCat:=C) c a d) as q.
99 apply isos_forward_equal_then_backward_equal in q.
102 setoid_rewrite <- pmon_coherent_r.
103 setoid_rewrite iso_comp1.
104 setoid_rewrite right_identity.
105 unfold fmor at 3; simpl.
106 apply comp_respects; [ idtac | reflexivity ].
108 set (pmon_coherent_r a c c0) as q.
109 apply isos_forward_equal_then_backward_equal in q.
110 setoid_rewrite iso_inv_inv in q.
113 setoid_rewrite pmon_coherent_r.
116 set (@isos_forward_equal_then_backward_equal) as q.
117 unfold iso_inv in q; simpl in q.
119 apply pmon_coherent_l.
123 set (ni_commutes (pmon_assoc_rr a c) g) as q.
125 apply iso_shift_left' in q.
126 unfold fmor in q at 2.
131 set (ni_commutes (pmon_assoc d c) f) as q.
132 apply iso_shift_right' in q.
133 unfold fmor in q at 1; simpl in q.
137 set (pmon_coherent_r d a c) as q.
138 apply isos_forward_equal_then_backward_equal in q.
139 rewrite iso_inv_inv in q.
140 unfold iso_inv in q; simpl in q.
144 setoid_rewrite juggle3.
145 set (iso_comp1 ((pmon_assoc d c) a)) as q.
148 setoid_rewrite right_identity.
150 set (ni_commutes (pmon_assoc_rr b c) g) as q.
152 apply iso_shift_left' in q.
153 unfold fmor in q at 2.
158 set (ni_commutes (pmon_assoc c0 c) f) as q.
159 unfold fmor in q; simpl in q.
160 apply iso_shift_right' in q.
164 set (pmon_coherent_r c0 b c) as q.
168 setoid_rewrite juggle3.
169 setoid_rewrite juggle3.
170 set (iso_comp1 ((pmon_assoc c0 c) b)) as q.
173 setoid_rewrite right_identity.
175 setoid_rewrite pmon_coherent_r.
176 repeat setoid_rewrite associativity.
177 apply comp_respects; [ reflexivity | idtac ].
178 repeat setoid_rewrite <- associativity.
180 setoid_rewrite (fmor_preserves_comp (-⋉c)).
181 apply (fmor_respects (-⋉c)).
182 apply centralmor_second.
183 set (pmon_coherent_r d b c) as q.
184 apply isos_forward_equal_then_backward_equal in q.
185 rewrite iso_inv_inv in q.
190 Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f).
192 apply Build_CentralMorphism; simpl; intros.
194 set (ni_commutes (pmon_assoc_ll c a) g) as q.
196 apply iso_shift_left' in q.
197 unfold fmor in q at 2.
202 set (ni_commutes (pmon_assoc c d) f) as q.
204 apply iso_shift_left' in q.
205 unfold fmor in q at 1; simpl in q.
209 rewrite <- pmon_coherent_l.
210 setoid_rewrite <- associativity.
211 setoid_rewrite juggle3.
212 set (iso_comp2 ((pmon_assoc_ll c a) d)) as q.
214 setoid_rewrite right_identity.
217 set (ni_commutes (pmon_assoc_ll c b) g) as q.
219 apply iso_shift_left' in q.
220 unfold fmor in q at 1; simpl in q.
224 set (ni_commutes (pmon_assoc c c0) f) as q.
225 unfold fmor in q; simpl in q.
227 apply iso_shift_left' in q.
231 rewrite pmon_coherent_l.
232 setoid_rewrite <- associativity.
233 setoid_rewrite juggle3.
234 set (iso_comp2 ((pmon_assoc c c0) b)) as q.
236 setoid_rewrite right_identity.
238 setoid_rewrite pmon_coherent_l.
240 repeat setoid_rewrite associativity.
241 apply comp_respects; [ reflexivity | idtac ].
242 repeat setoid_rewrite <- associativity.
244 setoid_rewrite (fmor_preserves_comp (c⋊-)).
245 apply (fmor_respects (c⋊-)).
246 apply centralmor_first.
247 set (pmon_coherent_l b c d) as q.
248 apply isos_forward_equal_then_backward_equal in q.
252 set (ni_commutes (pmon_assoc_ll d c) f) as q.
253 apply iso_shift_right' in q.
254 unfold fmor in q at 1; simpl in q.
258 set (ni_commutes (pmon_assoc_rr c a) g) as q.
260 unfold fmor in q at 2; simpl in q.
261 apply iso_shift_left' in q.
265 setoid_rewrite juggle3.
266 set (pmon_coherent_r d c a) as q.
267 apply isos_forward_equal_then_backward_equal in q.
268 setoid_rewrite iso_inv_inv in q.
271 setoid_rewrite <- pmon_coherent_l.
272 set (iso_comp1 (((pmon_assoc_ll d c) a))) as q.
275 setoid_rewrite right_identity.
276 setoid_rewrite juggle3.
277 setoid_rewrite (centralmor_second(CentralMorphism:=cm)).
279 apply iso_shift_left.
280 setoid_rewrite pmon_coherent_r.
281 set (pmon_coherent_l c d b) as q.
282 apply isos_forward_equal_then_backward_equal in q.
285 apply iso_shift_right.
286 setoid_rewrite iso_inv_inv.
287 repeat setoid_rewrite <- associativity.
289 set (ni_commutes (pmon_assoc_ll c0 c) f) as x.
290 setoid_rewrite <- pmon_coherent_l.
292 unfold fmor in x at 2; simpl in x.
296 set (ni_commutes (pmon_assoc_rr c b) g) as x.
298 unfold fmor in x at 2; simpl in x.
299 setoid_rewrite pmon_coherent_l.
300 setoid_rewrite <- pmon_coherent_r.
301 repeat setoid_rewrite associativity.
304 setoid_rewrite <- associativity.
305 setoid_rewrite juggle3.
306 setoid_rewrite pmon_coherent_r.
307 set (iso_comp1 ((pmon_assoc c0 b) c)) as x.
310 setoid_rewrite right_identity.
314 Section Center_is_Monoidal.
316 Context `(pm:PreMonoidalCat(I:=pmI)).
318 Definition Center_is_Binoidal : BinoidalCat (Center pm) bin_obj'.
319 apply PreMonoidalWideSubcategory_is_Binoidal.
320 intros; apply first_preserves_centrality; auto.
321 intros; apply second_preserves_centrality; auto.
324 Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal pmI.
325 apply PreMonoidalWideSubcategory_PreMonoidal.
328 Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal.
329 apply Build_MonoidalCat.
330 apply Build_CommutativeCat.
332 apply Build_CentralMorphism; unfold hom;
333 intros; destruct f; destruct g; simpl in *.
334 apply (centralmor_second(CentralMorphism:=c1)).
335 apply (centralmor_second(CentralMorphism:=c0)).
338 End Center_is_Monoidal.