src/PreMonoidalCenter.v

   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.
  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) : 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.
  52   Qed.
  53
  54
  55 Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
  56   intro cm.
  57   apply Build_CentralMorphism; simpl; intros.
  58
  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.
  62   rewrite q.
  63   clear q.
  64
  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.
  68   rewrite q.
  69   clear q.
  70
  71   set (ni_commutes (pmon_assoc_ll b c) g) as q.
  72   apply symmetry in q.
  73   apply iso_shift_left' in q.
  74   rewrite q.
  75   clear q.
  76
  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.
  82   setoid_rewrite q.
  83   clear q.
  84   setoid_rewrite right_identity.
  85   unfold fmor at 2.
  86   simpl.
  87   setoid_rewrite (centralmor_first(CentralMorphism:=cm)).
  88
  89   repeat setoid_rewrite <- associativity.
  90   apply comp_respects.
  91   apply comp_respects; [ idtac | reflexivity ].
  92   set (ni_commutes (pmon_assoc_ll a c) g) as q.
  93   apply symmetry in q.
  94   apply iso_shift_left' in q.
  95   setoid_rewrite q.
  96   clear 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.
 101   setoid_rewrite q.
 102   clear 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 ].
 108
 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.
 112   apply q.
 113
 114   setoid_rewrite pmon_coherent_r.
 115   unfold iso_inv.
 116   simpl.
 117   set (@isos_forward_equal_then_backward_equal) as q.
 118   unfold iso_inv in q; simpl in q.
 119   apply q.
 120   apply pmon_coherent_l.
 121
 122   (* *)
 123
 124   set (ni_commutes (pmon_assoc_rr a c) g) as q.
 125   symmetry in q.
 126   apply iso_shift_left' in q.
 127   unfold fmor in q at 2.
 128   simpl in q.
 129   setoid_rewrite q.
 130   clear q.
 131
 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.
 135   rewrite q.
 136   clear q.
 137
 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.
 142   rewrite q.
 143   clear q.
 144
 145   setoid_rewrite juggle3.
 146   set (iso_comp1 ((pmon_assoc d c) a)) as q.
 147   setoid_rewrite q.
 148   clear q.
 149   setoid_rewrite right_identity.
 150
 151   set (ni_commutes (pmon_assoc_rr b c) g) as q.
 152   symmetry in q.
 153   apply iso_shift_left' in q.
 154   unfold fmor in q at 2.
 155   simpl in q.
 156   setoid_rewrite q.
 157   clear q.
 158
 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.
 162   rewrite q.
 163   clear q.
 164
 165   set (pmon_coherent_r c0 b c) as q.
 166   rewrite q.
 167   clear q.
 168
 169   setoid_rewrite juggle3.
 170   setoid_rewrite juggle3.
 171   set (iso_comp1 ((pmon_assoc c0 c) b)) as q.
 172   setoid_rewrite q.
 173   clear q.
 174   setoid_rewrite right_identity.
 175
 176   setoid_rewrite pmon_coherent_r.
 177   repeat setoid_rewrite associativity.
 178   apply comp_respects; [ reflexivity | idtac ].
 179   repeat setoid_rewrite <- associativity.
 180   apply comp_respects.
 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.
 187   symmetry.
 188   apply q.
 189   Qed.
 190
 191 Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f).
 192   intro cm.
 193   apply Build_CentralMorphism; simpl; intros.
 194
 195   set (ni_commutes (pmon_assoc_ll c a) g) as q.
 196   symmetry in q.
 197   apply iso_shift_left' in q.
 198   unfold fmor in q at 2.
 199   simpl in q.
 200   setoid_rewrite q.
 201   clear q.
 202
 203   set (ni_commutes (pmon_assoc c d) f) as q.
 204   apply symmetry in q.
 205   apply iso_shift_left' in q.
 206   unfold fmor in q at 1; simpl in q.
 207   rewrite q.
 208   clear q.
 209
 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.
 214   setoid_rewrite q.
 215   setoid_rewrite right_identity.
 216   clear q.
 217
 218   set (ni_commutes (pmon_assoc_ll c b) g) as q.
 219   apply symmetry in q.
 220   apply iso_shift_left' in q.
 221   unfold fmor in q at 1; simpl in q.
 222   setoid_rewrite q.
 223   clear q.
 224
 225   set (ni_commutes (pmon_assoc c c0) f) as q.
 226   unfold fmor in q; simpl in q.
 227   symmetry in q.
 228   apply iso_shift_left' in q.
 229   rewrite q.
 230   clear q.
 231
 232   rewrite pmon_coherent_l.
 233   setoid_rewrite <- associativity.
 234   setoid_rewrite juggle3.
 235   set (iso_comp2 ((pmon_assoc c c0) b)) as q.
 236   setoid_rewrite q.
 237   setoid_rewrite right_identity.
 238   clear q.
 239   setoid_rewrite pmon_coherent_l.
 240
 241   repeat setoid_rewrite associativity.
 242   apply comp_respects; [ reflexivity | idtac ].
 243   repeat setoid_rewrite <- associativity.
 244   apply comp_respects.
 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.
 250   apply q.
 251
 252   (* *)
 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.
 256   rewrite q.
 257   clear q.
 258
 259   set (ni_commutes (pmon_assoc_rr c a) g) as q.
 260   apply symmetry in q.
 261   unfold fmor in q at 2; simpl in q.
 262   apply iso_shift_left' in q.
 263   rewrite q.
 264   clear q.
 265
 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.
 270   setoid_rewrite q.
 271   clear q.
 272   setoid_rewrite <- pmon_coherent_l.
 273   set (iso_comp1 (((pmon_assoc_ll d c) a))) as q.
 274   setoid_rewrite q.
 275   clear q.
 276   setoid_rewrite right_identity.
 277   setoid_rewrite juggle3.
 278   setoid_rewrite (centralmor_second(CentralMorphism:=cm)).
 279   symmetry.
 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.
 284   setoid_rewrite q.
 285   clear q.
 286   apply iso_shift_right.
 287   setoid_rewrite iso_inv_inv.
 288   repeat setoid_rewrite <- associativity.
 289
 290   set (ni_commutes (pmon_assoc_ll c0 c) f) as x.
 291   setoid_rewrite <- pmon_coherent_l.
 292   symmetry in x.
 293   unfold fmor in x at 2; simpl in x.
 294   setoid_rewrite <- x.
 295   clear x.
 296
 297   set (ni_commutes (pmon_assoc_rr c b) g) as x.
 298   symmetry in 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.
 303   setoid_rewrite x.
 304   clear x.
 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.
 309   setoid_rewrite x.
 310   clear x.
 311   setoid_rewrite right_identity.
 312   reflexivity.
 313   Qed.
 314
 315 Section Center_is_Monoidal.
 316
 317   Context `(pm:PreMonoidalCat(I:=pmI)).
 318
 319   Definition Center_bobj : Center pm -> Center pm -> Center pm.
 320     apply PreMonoidalSubCategory_bobj.
 321     intros; auto.
 322     Defined.
 323
 324   Definition Center_is_Binoidal : BinoidalCat (Center pm) Center_bobj.
 325     apply PreMonoidalSubCategory_is_Binoidal.
 326     intros.
 327     apply first_preserves_centrality; auto.
 328     intros.
 329     apply second_preserves_centrality; auto.
 330     Defined.
 331
 332   Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal (exist _ pmI I).
 333     apply PreMonoidalSubCategory_PreMonoidal.
 334     Defined.
 335
 336   Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal.
 337     apply Build_MonoidalCat.
 338     apply Build_CommutativeCat.
 339     intros.
 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.
 344     Defined.
 345
 346 End Center_is_Monoidal.