src/PreMonoidalCenter.v

   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.
  14
  15 (******************************************************************************)
  16 (* Facts about the center of a Binoidal or PreMonoidal Category               *)
  17 (******************************************************************************)
  18
  19 Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
  20   : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
  21   intros.
  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));
  30               reflexivity).
  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));
  38               reflexivity).
  39   Qed.
  40
  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.
  52   Qed.
  53
  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⁻¹.
  56   intro cm.
  57   apply Build_CentralMorphism; intros; simpl.
  58     etransitivity.
  59     symmetry.
  60     apply right_identity.
  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)).
  74     apply iso_comp2.
  75     symmetry.
  76     etransitivity; [ idtac | apply (fmor_preserves_id (-⋉d)) ].
  77     apply (fmor_respects (-⋉d)).
  78     apply iso_comp1.
  79
  80     etransitivity.
  81     symmetry.
  82     apply left_identity.
  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⋊-)).
  95     apply iso_comp1.
  96     symmetry.
  97     etransitivity; [ idtac | apply (fmor_preserves_id (c⋊-)) ].
  98     apply (fmor_respects (c⋊-)).
  99     apply iso_comp2.
 100     Qed.
 101
 102 Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
 103   intro cm.
 104   apply Build_CentralMorphism; simpl; intros.
 105
 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.
 109   rewrite q.
 110   clear q.
 111
 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.
 115   rewrite q.
 116   clear q.
 117
 118   set (ni_commutes (pmon_assoc_ll b c) g) as q.
 119   apply symmetry in q.
 120   apply iso_shift_left' in q.
 121   rewrite q.
 122   clear q.
 123
 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.
 129   setoid_rewrite q.
 130   clear q.
 131   setoid_rewrite right_identity.
 132   unfold fmor at 2.
 133   simpl.
 134   setoid_rewrite (centralmor_first(CentralMorphism:=cm)).
 135
 136   repeat setoid_rewrite <- associativity.
 137   apply comp_respects.
 138   apply comp_respects; [ idtac | reflexivity ].
 139   set (ni_commutes (pmon_assoc_ll a c) g) as q.
 140   apply symmetry in q.
 141   apply iso_shift_left' in q.
 142   setoid_rewrite q.
 143   clear 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.
 148   setoid_rewrite q.
 149   clear 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 ].
 155
 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.
 159   apply q.
 160
 161   setoid_rewrite pmon_coherent_r.
 162   unfold iso_inv.
 163   simpl.
 164   set (@isos_forward_equal_then_backward_equal) as q.
 165   unfold iso_inv in q; simpl in q.
 166   apply q.
 167   apply pmon_coherent_l.
 168
 169   (* *)
 170
 171   set (ni_commutes (pmon_assoc_rr a c) g) as q.
 172   symmetry in q.
 173   apply iso_shift_left' in q.
 174   unfold fmor in q at 2.
 175   simpl in q.
 176   setoid_rewrite q.
 177   clear q.
 178
 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.
 182   rewrite q.
 183   clear q.
 184
 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.
 189   rewrite q.
 190   clear q.
 191
 192   setoid_rewrite juggle3.
 193   set (iso_comp1 ((pmon_assoc d c) a)) as q.
 194   setoid_rewrite q.
 195   clear q.
 196   setoid_rewrite right_identity.
 197
 198   set (ni_commutes (pmon_assoc_rr b c) g) as q.
 199   symmetry in q.
 200   apply iso_shift_left' in q.
 201   unfold fmor in q at 2.
 202   simpl in q.
 203   setoid_rewrite q.
 204   clear q.
 205
 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.
 209   rewrite q.
 210   clear q.
 211
 212   set (pmon_coherent_r c0 b c) as q.
 213   rewrite q.
 214   clear q.
 215
 216   setoid_rewrite juggle3.
 217   setoid_rewrite juggle3.
 218   set (iso_comp1 ((pmon_assoc c0 c) b)) as q.
 219   setoid_rewrite q.
 220   clear q.
 221   setoid_rewrite right_identity.
 222
 223   setoid_rewrite pmon_coherent_r.
 224   repeat setoid_rewrite associativity.
 225   apply comp_respects; [ reflexivity | idtac ].
 226   repeat setoid_rewrite <- associativity.
 227   apply comp_respects.
 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.
 234   symmetry.
 235   apply q.
 236   Qed.
 237
 238 Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f).
 239   intro cm.
 240   apply Build_CentralMorphism; simpl; intros.
 241
 242   set (ni_commutes (pmon_assoc_ll c a) g) as q.
 243   symmetry in q.
 244   apply iso_shift_left' in q.
 245   unfold fmor in q at 2.
 246   simpl in q.
 247   setoid_rewrite q.
 248   clear q.
 249
 250   set (ni_commutes (pmon_assoc c d) f) as q.
 251   apply symmetry in q.
 252   apply iso_shift_left' in q.
 253   unfold fmor in q at 1; simpl in q.
 254   rewrite q.
 255   clear q.
 256
 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.
 261   setoid_rewrite q.
 262   setoid_rewrite right_identity.
 263   clear q.
 264
 265   set (ni_commutes (pmon_assoc_ll c b) g) as q.
 266   apply symmetry in q.
 267   apply iso_shift_left' in q.
 268   unfold fmor in q at 1; simpl in q.
 269   setoid_rewrite q.
 270   clear q.
 271
 272   set (ni_commutes (pmon_assoc c c0) f) as q.
 273   unfold fmor in q; simpl in q.
 274   symmetry in q.
 275   apply iso_shift_left' in q.
 276   rewrite q.
 277   clear q.
 278
 279   rewrite pmon_coherent_l.
 280   setoid_rewrite <- associativity.
 281   setoid_rewrite juggle3.
 282   set (iso_comp2 ((pmon_assoc c c0) b)) as q.
 283   setoid_rewrite q.
 284   setoid_rewrite right_identity.
 285   clear q.
 286   setoid_rewrite pmon_coherent_l.
 287
 288   repeat setoid_rewrite associativity.
 289   apply comp_respects; [ reflexivity | idtac ].
 290   repeat setoid_rewrite <- associativity.
 291   apply comp_respects.
 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.
 297   apply q.
 298
 299   (* *)
 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.
 303   rewrite q.
 304   clear q.
 305
 306   set (ni_commutes (pmon_assoc_rr c a) g) as q.
 307   apply symmetry in q.
 308   unfold fmor in q at 2; simpl in q.
 309   apply iso_shift_left' in q.
 310   rewrite q.
 311   clear q.
 312
 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.
 317   setoid_rewrite q.
 318   clear q.
 319   setoid_rewrite <- pmon_coherent_l.
 320   set (iso_comp1 (((pmon_assoc_ll d c) a))) as q.
 321   setoid_rewrite q.
 322   clear q.
 323   setoid_rewrite right_identity.
 324   setoid_rewrite juggle3.
 325   setoid_rewrite (centralmor_second(CentralMorphism:=cm)).
 326   symmetry.
 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.
 331   setoid_rewrite q.
 332   clear q.
 333   apply iso_shift_right.
 334   setoid_rewrite iso_inv_inv.
 335   repeat setoid_rewrite <- associativity.
 336
 337   set (ni_commutes (pmon_assoc_ll c0 c) f) as x.
 338   setoid_rewrite <- pmon_coherent_l.
 339   symmetry in x.
 340   unfold fmor in x at 2; simpl in x.
 341   setoid_rewrite <- x.
 342   clear x.
 343
 344   set (ni_commutes (pmon_assoc_rr c b) g) as x.
 345   symmetry in 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.
 350   setoid_rewrite x.
 351   clear x.
 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.
 356   setoid_rewrite x.
 357   clear x.
 358   setoid_rewrite right_identity.
 359   reflexivity.
 360   Qed.
 361
 362 Section Center_is_Monoidal.
 363
 364   Context `(pm:PreMonoidalCat(I:=pmI)).
 365
 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.
 370     Defined.
 371
 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.
 380     Defined.
 381
 382   Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal.
 383     apply Build_MonoidalCat.
 384     apply Build_CommutativeCat.
 385     intros.
 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)).
 390     Defined.
 391
 392 End Center_is_Monoidal.