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) : SubCategory bc (fun _ => True) (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.
55 Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
57 apply Build_CentralMorphism; simpl; intros.
59 set (ni_commutes (pmon_assoc_rr c c0) f) as q.
60 apply iso_shift_right' in q.
61 unfold fmor in q at 1; simpl in q.
65 set (ni_commutes (pmon_assoc_rr c d) f) as q.
66 apply iso_shift_right' in q.
67 unfold fmor in q at 1; simpl in q.
71 set (ni_commutes (pmon_assoc_ll b c) g) as q.
73 apply iso_shift_left' in q.
77 setoid_rewrite pmon_coherent_r at 1.
78 setoid_rewrite pmon_coherent_l at 1.
79 setoid_rewrite juggle3.
80 setoid_rewrite juggle3.
81 set (@iso_comp2 _ _ _ _ _ ((pmon_assoc b c0) c)) as q.
84 setoid_rewrite right_identity.
87 setoid_rewrite (centralmor_first(CentralMorphism:=cm)).
89 repeat setoid_rewrite <- associativity.
91 apply comp_respects; [ idtac | reflexivity ].
92 set (ni_commutes (pmon_assoc_ll a c) g) as q.
94 apply iso_shift_left' in q.
97 repeat setoid_rewrite associativity.
98 setoid_rewrite pmon_coherent_l.
99 set (pmon_coherent_l(PreMonoidalCat:=C) c a d) as q.
100 apply isos_forward_equal_then_backward_equal in q.
103 setoid_rewrite <- pmon_coherent_r.
104 setoid_rewrite iso_comp1.
105 setoid_rewrite right_identity.
106 unfold fmor at 3; simpl.
107 apply comp_respects; [ idtac | reflexivity ].
109 set (pmon_coherent_r a c c0) as q.
110 apply isos_forward_equal_then_backward_equal in q.
111 setoid_rewrite iso_inv_inv in q.
114 setoid_rewrite pmon_coherent_r.
117 set (@isos_forward_equal_then_backward_equal) as q.
118 unfold iso_inv in q; simpl in q.
120 apply pmon_coherent_l.
124 set (ni_commutes (pmon_assoc_rr a c) g) as q.
126 apply iso_shift_left' in q.
127 unfold fmor in q at 2.
132 set (ni_commutes (pmon_assoc d c) f) as q.
133 apply iso_shift_right' in q.
134 unfold fmor in q at 1; simpl in q.
138 set (pmon_coherent_r d a c) as q.
139 apply isos_forward_equal_then_backward_equal in q.
140 rewrite iso_inv_inv in q.
141 unfold iso_inv in q; simpl in q.
145 setoid_rewrite juggle3.
146 set (iso_comp1 ((pmon_assoc d c) a)) as q.
149 setoid_rewrite right_identity.
151 set (ni_commutes (pmon_assoc_rr b c) g) as q.
153 apply iso_shift_left' in q.
154 unfold fmor in q at 2.
159 set (ni_commutes (pmon_assoc c0 c) f) as q.
160 unfold fmor in q; simpl in q.
161 apply iso_shift_right' in q.
165 set (pmon_coherent_r c0 b c) as q.
169 setoid_rewrite juggle3.
170 setoid_rewrite juggle3.
171 set (iso_comp1 ((pmon_assoc c0 c) b)) as q.
174 setoid_rewrite right_identity.
176 setoid_rewrite pmon_coherent_r.
177 repeat setoid_rewrite associativity.
178 apply comp_respects; [ reflexivity | idtac ].
179 repeat setoid_rewrite <- associativity.
181 setoid_rewrite (fmor_preserves_comp (-⋉c)).
182 apply (fmor_respects (-⋉c)).
183 apply centralmor_second.
184 set (pmon_coherent_r d b c) as q.
185 apply isos_forward_equal_then_backward_equal in q.
186 rewrite iso_inv_inv in q.
191 Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f).
193 apply Build_CentralMorphism; simpl; intros.
195 set (ni_commutes (pmon_assoc_ll c a) g) as q.
197 apply iso_shift_left' in q.
198 unfold fmor in q at 2.
203 set (ni_commutes (pmon_assoc c d) f) as q.
205 apply iso_shift_left' in q.
206 unfold fmor in q at 1; simpl in q.
210 rewrite <- pmon_coherent_l.
211 setoid_rewrite <- associativity.
212 setoid_rewrite juggle3.
213 set (iso_comp2 ((pmon_assoc_ll c a) d)) as q.
215 setoid_rewrite right_identity.
218 set (ni_commutes (pmon_assoc_ll c b) g) as q.
220 apply iso_shift_left' in q.
221 unfold fmor in q at 1; simpl in q.
225 set (ni_commutes (pmon_assoc c c0) f) as q.
226 unfold fmor in q; simpl in q.
228 apply iso_shift_left' in q.
232 rewrite pmon_coherent_l.
233 setoid_rewrite <- associativity.
234 setoid_rewrite juggle3.
235 set (iso_comp2 ((pmon_assoc c c0) b)) as q.
237 setoid_rewrite right_identity.
239 setoid_rewrite pmon_coherent_l.
241 repeat setoid_rewrite associativity.
242 apply comp_respects; [ reflexivity | idtac ].
243 repeat setoid_rewrite <- associativity.
245 setoid_rewrite (fmor_preserves_comp (c⋊-)).
246 apply (fmor_respects (c⋊-)).
247 apply centralmor_first.
248 set (pmon_coherent_l b c d) as q.
249 apply isos_forward_equal_then_backward_equal in q.
253 set (ni_commutes (pmon_assoc_ll d c) f) as q.
254 apply iso_shift_right' in q.
255 unfold fmor in q at 1; simpl in q.
259 set (ni_commutes (pmon_assoc_rr c a) g) as q.
261 unfold fmor in q at 2; simpl in q.
262 apply iso_shift_left' in q.
266 setoid_rewrite juggle3.
267 set (pmon_coherent_r d c a) as q.
268 apply isos_forward_equal_then_backward_equal in q.
269 setoid_rewrite iso_inv_inv in q.
272 setoid_rewrite <- pmon_coherent_l.
273 set (iso_comp1 (((pmon_assoc_ll d c) a))) as q.
276 setoid_rewrite right_identity.
277 setoid_rewrite juggle3.
278 setoid_rewrite (centralmor_second(CentralMorphism:=cm)).
280 apply iso_shift_left.
281 setoid_rewrite pmon_coherent_r.
282 set (pmon_coherent_l c d b) as q.
283 apply isos_forward_equal_then_backward_equal in q.
286 apply iso_shift_right.
287 setoid_rewrite iso_inv_inv.
288 repeat setoid_rewrite <- associativity.
290 set (ni_commutes (pmon_assoc_ll c0 c) f) as x.
291 setoid_rewrite <- pmon_coherent_l.
293 unfold fmor in x at 2; simpl in x.
297 set (ni_commutes (pmon_assoc_rr c b) g) as x.
299 unfold fmor in x at 2; simpl in x.
300 setoid_rewrite pmon_coherent_l.
301 setoid_rewrite <- pmon_coherent_r.
302 repeat setoid_rewrite associativity.
305 setoid_rewrite <- associativity.
306 setoid_rewrite juggle3.
307 setoid_rewrite pmon_coherent_r.
308 set (iso_comp1 ((pmon_assoc c0 b) c)) as x.
311 setoid_rewrite right_identity.
315 Section Center_is_Monoidal.
317 Context `(pm:PreMonoidalCat(I:=pmI)).
319 Definition Center_bobj : Center pm -> Center pm -> Center pm.
320 apply PreMonoidalSubCategory_bobj.
324 Definition Center_is_Binoidal : BinoidalCat (Center pm) Center_bobj.
325 apply PreMonoidalSubCategory_is_Binoidal.
327 apply first_preserves_centrality; auto.
329 apply second_preserves_centrality; auto.
332 Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal (exist _ pmI I).
333 apply PreMonoidalSubCategory_PreMonoidal.
336 Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal.
337 apply Build_MonoidalCat.
338 apply Build_CommutativeCat.
340 apply Build_CentralMorphism; unfold hom;
341 intros; destruct f; destruct a; destruct c; destruct d; destruct b; destruct g; simpl in *.
342 apply centralmor_second.
343 apply centralmor_second.
346 End Center_is_Monoidal.