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 ProductCategories_ch1_6_1.
7 Require Import InitialTerminal_ch2_2.
8 Require Import Subcategories_ch7_1.
9 Require Import NaturalTransformations_ch7_4.
10 Require Import NaturalIsomorphisms_ch7_5.
11 Require Import Coherence_ch7_8.
12 Require Import BinoidalCategories.
13 Require Import PreMonoidalCategories.
14 Require Import MonoidalCategories_ch_7_8.
16 (******************************************************************************)
17 (* Facts about the center of a Binoidal or PreMonoidal Category *)
18 (******************************************************************************)
20 Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
21 : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
23 apply Build_CentralMorphism; intros.
24 abstract (setoid_rewrite <- (fmor_preserves_comp(bin_first c0));
25 setoid_rewrite associativity;
26 setoid_rewrite centralmor_first;
27 setoid_rewrite <- associativity;
28 setoid_rewrite centralmor_first;
29 setoid_rewrite associativity;
30 setoid_rewrite <- (fmor_preserves_comp(bin_first d));
32 abstract (setoid_rewrite <- (fmor_preserves_comp(bin_second d));
33 setoid_rewrite <- associativity;
34 setoid_rewrite centralmor_second;
35 setoid_rewrite associativity;
36 setoid_rewrite centralmor_second;
37 setoid_rewrite <- associativity;
38 setoid_rewrite <- (fmor_preserves_comp(bin_second c0));
42 (* the central morphisms of a category constitute a subcategory *)
43 Definition Center `(bc:BinoidalCat) : SubCategory bc (fun _ => True) (fun _ _ _ _ f => CentralMorphism f).
44 apply Build_SubCategory; intros.
45 apply Build_CentralMorphism; intros.
46 abstract (setoid_rewrite (fmor_preserves_id(bin_first c));
47 setoid_rewrite (fmor_preserves_id(bin_first d));
48 setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
49 abstract (setoid_rewrite (fmor_preserves_id(bin_second c));
50 setoid_rewrite (fmor_preserves_id(bin_second d));
51 setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
52 apply central_morphisms_compose; auto.
56 Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
58 apply Build_CentralMorphism; simpl; intros.
60 set (ni_commutes (pmon_assoc_rr c c0) f) as q.
61 apply iso_shift_right' in q.
62 unfold fmor in q at 1; simpl in q.
66 set (ni_commutes (pmon_assoc_rr c d) f) as q.
67 apply iso_shift_right' in q.
68 unfold fmor in q at 1; simpl in q.
72 set (ni_commutes (pmon_assoc_ll b c) g) as q.
74 apply iso_shift_left' in q.
78 setoid_rewrite pmon_coherent_r at 1.
79 setoid_rewrite pmon_coherent_l at 1.
80 setoid_rewrite juggle3.
81 setoid_rewrite juggle3.
82 set (@iso_comp2 _ _ _ _ _ ((pmon_assoc C b c0) c)) as q.
85 setoid_rewrite right_identity.
88 setoid_rewrite (centralmor_first(CentralMorphism:=cm)).
90 repeat setoid_rewrite <- associativity.
92 apply comp_respects; [ idtac | reflexivity ].
93 set (ni_commutes (pmon_assoc_ll a c) g) as q.
95 apply iso_shift_left' in q.
98 repeat setoid_rewrite associativity.
99 setoid_rewrite pmon_coherent_l.
100 set (pmon_coherent_l(PreMonoidalCat:=C) c a d) as q.
101 apply isos_forward_equal_then_backward_equal in q.
104 setoid_rewrite <- pmon_coherent_r.
105 setoid_rewrite iso_comp1.
106 setoid_rewrite right_identity.
107 unfold fmor at 3; simpl.
108 apply comp_respects; [ idtac | reflexivity ].
110 set (pmon_coherent_r a c c0) as q.
111 apply isos_forward_equal_then_backward_equal in q.
112 setoid_rewrite iso_inv_inv in q.
115 setoid_rewrite pmon_coherent_r.
118 set (@isos_forward_equal_then_backward_equal) as q.
119 unfold iso_inv in q; simpl in q.
121 apply pmon_coherent_l.
125 set (ni_commutes (pmon_assoc_rr a c) g) as q.
127 apply iso_shift_left' in q.
128 unfold fmor in q at 2.
133 set (ni_commutes (pmon_assoc _ d c) f) as q.
134 apply iso_shift_right' in q.
135 unfold fmor in q at 1; simpl in q.
139 set (pmon_coherent_r d a c) as q.
140 apply isos_forward_equal_then_backward_equal in q.
141 rewrite iso_inv_inv in q.
142 unfold iso_inv in q; simpl in q.
146 setoid_rewrite juggle3.
147 setoid_rewrite (iso_comp1 ((pmon_assoc C d c) a)).
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 setoid_rewrite (iso_comp1 ((pmon_assoc C c0 c) b)).
171 setoid_rewrite right_identity.
173 setoid_rewrite pmon_coherent_r.
174 repeat setoid_rewrite associativity.
175 apply comp_respects; [ reflexivity | idtac ].
176 repeat setoid_rewrite <- associativity.
178 setoid_rewrite (fmor_preserves_comp (-⋉c)).
179 apply (fmor_respects (-⋉c)).
180 apply centralmor_second.
181 set (pmon_coherent_r d b c) as q.
182 apply isos_forward_equal_then_backward_equal in q.
183 rewrite iso_inv_inv in q.
188 Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f).
190 apply Build_CentralMorphism; simpl; intros.
192 set (ni_commutes (pmon_assoc_ll c a) g) as q.
194 apply iso_shift_left' in q.
195 unfold fmor in q at 2.
200 set (ni_commutes (pmon_assoc _ c d) f) as q.
202 apply iso_shift_left' in q.
203 unfold fmor in q at 1; simpl in q.
207 rewrite <- pmon_coherent_l.
208 setoid_rewrite <- associativity.
209 setoid_rewrite juggle3.
210 set (iso_comp2 ((pmon_assoc_ll c a) d)) as q.
212 setoid_rewrite right_identity.
215 set (ni_commutes (pmon_assoc_ll c b) g) as q.
217 apply iso_shift_left' in q.
218 unfold fmor in q at 1; simpl in q.
222 set (ni_commutes (pmon_assoc _ c c0) f) as q.
223 unfold fmor in q; simpl in q.
225 apply iso_shift_left' in q.
229 rewrite pmon_coherent_l.
230 setoid_rewrite <- associativity.
231 setoid_rewrite juggle3.
232 set (iso_comp2 ((pmon_assoc _ c c0) b)) as q.
234 setoid_rewrite right_identity.
236 setoid_rewrite pmon_coherent_l.
238 repeat setoid_rewrite associativity.
239 apply comp_respects; [ reflexivity | idtac ].
240 repeat setoid_rewrite <- associativity.
242 setoid_rewrite (fmor_preserves_comp (c⋊-)).
243 apply (fmor_respects (c⋊-)).
244 apply centralmor_first.
245 set (pmon_coherent_l b c d) as q.
246 apply isos_forward_equal_then_backward_equal in q.
250 set (ni_commutes (pmon_assoc_ll d c) f) as q.
251 apply iso_shift_right' in q.
252 unfold fmor in q at 1; simpl in q.
256 set (ni_commutes (pmon_assoc_rr c a) g) as q.
258 unfold fmor in q at 2; simpl in q.
259 apply iso_shift_left' in q.
263 setoid_rewrite juggle3.
264 set (pmon_coherent_r d c a) as q.
265 apply isos_forward_equal_then_backward_equal in q.
266 setoid_rewrite iso_inv_inv in q.
269 setoid_rewrite <- pmon_coherent_l.
270 set (iso_comp1 (((pmon_assoc_ll d c) a))) as q.
273 setoid_rewrite right_identity.
274 setoid_rewrite juggle3.
275 setoid_rewrite (centralmor_second(CentralMorphism:=cm)).
277 apply iso_shift_left.
278 setoid_rewrite pmon_coherent_r.
279 set (pmon_coherent_l c d b) as q.
280 apply isos_forward_equal_then_backward_equal in q.
283 apply iso_shift_right.
284 setoid_rewrite iso_inv_inv.
285 repeat setoid_rewrite <- associativity.
287 set (ni_commutes (pmon_assoc_ll c0 c) f) as x.
288 setoid_rewrite <- pmon_coherent_l.
290 unfold fmor in x at 2; simpl in x.
294 set (ni_commutes (pmon_assoc_rr c b) g) as x.
296 unfold fmor in x at 2; simpl in x.
297 setoid_rewrite pmon_coherent_l.
298 setoid_rewrite <- pmon_coherent_r.
299 repeat setoid_rewrite associativity.
302 setoid_rewrite <- associativity.
303 setoid_rewrite juggle3.
304 setoid_rewrite pmon_coherent_r.
305 set (iso_comp1 ((pmon_assoc C c0 b) c)) as x.
308 setoid_rewrite right_identity.
312 Section CenterMonoidal.
314 Context `(mc:PreMonoidalCat(I:=pI)).
316 Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
319 destruct a as [a apf].
320 destruct b as [b bpf].
321 exists (a ⊗ b); auto.
324 Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) :
325 (a~~{(Center mc) ×× (Center mc)}~~>b) ->
326 ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)).
327 destruct a as [[a1 a1'] [a2 a2']].
328 destruct b as [[b1 b1'] [b2 b2']].
330 destruct f as [[f1 f1'] [f2 f2']].
334 exists (f1 ⋉ a2 >>> b1 ⋊ f2).
335 apply central_morphisms_compose.
336 apply first_preserves_centrality; auto.
337 apply second_preserves_centrality; auto.
340 Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
341 refine {| fmor := CenterMonoidal_F_fmor |}.
343 destruct a as [[a1 a1'] [a2 a2']].
344 destruct b as [[b1 b1'] [b2 b2']].
345 destruct f as [[f1 f1'] [f2 f2']].
346 destruct f' as [[g1 g1'] [g2 g2']].
350 set (fmor_respects(-⋉a2)) as q; apply q; auto.
351 set (fmor_respects(b1⋊-)) as q; apply q; auto.
353 destruct a as [[a1 a1'] [a2 a2']].
355 setoid_rewrite (fmor_preserves_id (-⋉a2)).
356 setoid_rewrite (fmor_preserves_id (a1⋊-)).
359 destruct a as [[a1 a1'] [a2 a2']].
360 destruct b as [[b1 b1'] [b2 b2']].
361 destruct c as [[c1 c1'] [c2 c2']].
362 destruct f as [[f1 f1'] [f2 f2']].
363 destruct g as [[g1 g1'] [g2 g2']].
365 setoid_rewrite juggle3.
366 setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
367 setoid_rewrite <- juggle3.
368 setoid_rewrite <- fmor_preserves_comp.
372 Definition center_I : Center mc := exist _ pI I.
374 Definition center_cancelr : (func_rlecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc).
375 Definition center_cancelr_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj A center_I) ≅ A.
378 set (ni_iso (pmon_cancelr mc) x) as q.
379 (*refine {| iso_forward := #q ; iso_backward := iso_backward q |}.*)
382 refine {| ni_iso := center_cancelr_niso |}.
386 Definition center_cancell : (func_llecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc).
387 Definition center_cancell_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj center_I A) ≅ A.
390 refine {| ni_iso := center_cancell_niso |}.
394 Definition center_assoc :
395 ((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F)
396 <~~~> func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F)).
398 Definition center_assoc_niso : ∀A : (Center mc ×× Center mc) ×× Center mc,
399 ((((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F) A))
400 ≅ ((func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F))) A).
404 refine {| ni_iso := center_assoc_niso |}.
408 Instance CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I) :=
409 { mon_cancelr := center_cancelr
410 ; mon_cancell := center_cancell
411 ; mon_assoc := center_assoc