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