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 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.
  15
  16 (******************************************************************************)
  17 (* Facts about the center of a Binoidal or PreMonoidal Category               *)
  18 (******************************************************************************)
  19
  20 Lemma central_morphisms_compose `{bc:BinoidalCat}{a b c}(f:a~>b)(g:b~>c)
  21   : CentralMorphism f -> CentralMorphism g -> CentralMorphism (f >>> g).
  22   intros.
  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));
  31               reflexivity).
  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));
  39               reflexivity).
  40   Qed.
  41
  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.
  53   Qed.
  54
  55
  56 Lemma first_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (f ⋉ c).
  57   intro cm.
  58   apply Build_CentralMorphism; simpl; intros.
  59
  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.
  63   rewrite q.
  64   clear q.
  65
  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.
  69   rewrite q.
  70   clear q.
  71
  72   set (ni_commutes (pmon_assoc_ll b c) g) as q.
  73   apply symmetry in q.
  74   apply iso_shift_left' in q.
  75   rewrite q.
  76   clear q.
  77
  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.
  83   setoid_rewrite q.
  84   clear q.
  85   setoid_rewrite right_identity.
  86   unfold fmor at 2.
  87   simpl.
  88   setoid_rewrite (centralmor_first(CentralMorphism:=cm)).
  89
  90   repeat setoid_rewrite <- associativity.
  91   apply comp_respects.
  92   apply comp_respects; [ idtac | reflexivity ].
  93   set (ni_commutes (pmon_assoc_ll a c) g) as q.
  94   apply symmetry in q.
  95   apply iso_shift_left' in q.
  96   setoid_rewrite q.
  97   clear 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.
 102   setoid_rewrite q.
 103   clear 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 ].
 109
 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.
 113   apply q.
 114
 115   setoid_rewrite pmon_coherent_r.
 116   unfold iso_inv.
 117   simpl.
 118   set (@isos_forward_equal_then_backward_equal) as q.
 119   unfold iso_inv in q; simpl in q.
 120   apply q.
 121   apply pmon_coherent_l.
 122
 123   (* *)
 124
 125   set (ni_commutes (pmon_assoc_rr a c) g) as q.
 126   symmetry in q.
 127   apply iso_shift_left' in q.
 128   unfold fmor in q at 2.
 129   simpl in q.
 130   setoid_rewrite q.
 131   clear q.
 132
 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.
 136   rewrite q.
 137   clear q.
 138
 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.
 143   rewrite q.
 144   clear q.
 145
 146   setoid_rewrite juggle3.
 147   setoid_rewrite (iso_comp1 ((pmon_assoc C d c) a)).
 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   setoid_rewrite (iso_comp1 ((pmon_assoc C c0 c) b)).
 171   setoid_rewrite right_identity.
 172
 173   setoid_rewrite pmon_coherent_r.
 174   repeat setoid_rewrite associativity.
 175   apply comp_respects; [ reflexivity | idtac ].
 176   repeat setoid_rewrite <- associativity.
 177   apply comp_respects.
 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.
 184   symmetry.
 185   apply q.
 186   Qed.
 187
 188 Lemma second_preserves_centrality `{C:PreMonoidalCat}{a}{b}(f:a~~{C}~~>b){c} : CentralMorphism f -> CentralMorphism (c ⋊ f).
 189   intro cm.
 190   apply Build_CentralMorphism; simpl; intros.
 191
 192   set (ni_commutes (pmon_assoc_ll c a) g) as q.
 193   symmetry in q.
 194   apply iso_shift_left' in q.
 195   unfold fmor in q at 2.
 196   simpl in q.
 197   setoid_rewrite q.
 198   clear q.
 199
 200   set (ni_commutes (pmon_assoc _ c d) f) as q.
 201   apply symmetry in q.
 202   apply iso_shift_left' in q.
 203   unfold fmor in q at 1; simpl in q.
 204   rewrite q.
 205   clear q.
 206
 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.
 211   setoid_rewrite q.
 212   setoid_rewrite right_identity.
 213   clear q.
 214
 215   set (ni_commutes (pmon_assoc_ll c b) g) as q.
 216   apply symmetry in q.
 217   apply iso_shift_left' in q.
 218   unfold fmor in q at 1; simpl in q.
 219   setoid_rewrite q.
 220   clear q.
 221
 222   set (ni_commutes (pmon_assoc _ c c0) f) as q.
 223   unfold fmor in q; simpl in q.
 224   symmetry in q.
 225   apply iso_shift_left' in q.
 226   rewrite q.
 227   clear q.
 228
 229   rewrite pmon_coherent_l.
 230   setoid_rewrite <- associativity.
 231   setoid_rewrite juggle3.
 232   set (iso_comp2 ((pmon_assoc _ c c0) b)) as q.
 233   setoid_rewrite q.
 234   setoid_rewrite right_identity.
 235   clear q.
 236   setoid_rewrite pmon_coherent_l.
 237
 238   repeat setoid_rewrite associativity.
 239   apply comp_respects; [ reflexivity | idtac ].
 240   repeat setoid_rewrite <- associativity.
 241   apply comp_respects.
 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.
 247   apply q.
 248
 249   (* *)
 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.
 253   rewrite q.
 254   clear q.
 255
 256   set (ni_commutes (pmon_assoc_rr c a) g) as q.
 257   apply symmetry in q.
 258   unfold fmor in q at 2; simpl in q.
 259   apply iso_shift_left' in q.
 260   rewrite q.
 261   clear q.
 262
 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.
 267   setoid_rewrite q.
 268   clear q.
 269   setoid_rewrite <- pmon_coherent_l.
 270   set (iso_comp1 (((pmon_assoc_ll d c) a))) as q.
 271   setoid_rewrite q.
 272   clear q.
 273   setoid_rewrite right_identity.
 274   setoid_rewrite juggle3.
 275   setoid_rewrite (centralmor_second(CentralMorphism:=cm)).
 276   symmetry.
 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.
 281   setoid_rewrite q.
 282   clear q.
 283   apply iso_shift_right.
 284   setoid_rewrite iso_inv_inv.
 285   repeat setoid_rewrite <- associativity.
 286
 287   set (ni_commutes (pmon_assoc_ll c0 c) f) as x.
 288   setoid_rewrite <- pmon_coherent_l.
 289   symmetry in x.
 290   unfold fmor in x at 2; simpl in x.
 291   setoid_rewrite <- x.
 292   clear x.
 293
 294   set (ni_commutes (pmon_assoc_rr c b) g) as x.
 295   symmetry in 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.
 300   setoid_rewrite x.
 301   clear x.
 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.
 306   setoid_rewrite x.
 307   clear x.
 308   setoid_rewrite right_identity.
 309   reflexivity.
 310   Qed.
 311
 312 Section CenterMonoidal.
 313
 314   Context `(mc:PreMonoidalCat(I:=pI)).
 315
 316   Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
 317     intro.
 318     destruct X as [a b].
 319     destruct a as [a apf].
 320     destruct b as [b bpf].
 321     exists (a ⊗ b); auto.
 322     Defined.
 323
 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']].
 329     intro f.
 330     destruct f as [[f1 f1'] [f2 f2']].
 331     simpl in *.
 332     unfold hom.
 333     simpl.
 334     exists (f1 ⋉ a2 >>> b1 ⋊ f2).
 335     apply central_morphisms_compose.
 336     apply first_preserves_centrality; auto.
 337     apply second_preserves_centrality; auto.
 338     Defined.
 339
 340   Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
 341     refine {| fmor := CenterMonoidal_F_fmor |}.
 342     intros.
 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']].
 347     simpl in *.
 348     destruct H.
 349     apply comp_respects.
 350     set (fmor_respects(-⋉a2)) as q; apply q; auto.
 351     set (fmor_respects(b1⋊-)) as q; apply q; auto.
 352     intros.
 353     destruct a as [[a1 a1'] [a2 a2']].
 354     simpl in *.
 355     setoid_rewrite (fmor_preserves_id (-⋉a2)).
 356     setoid_rewrite (fmor_preserves_id (a1⋊-)).
 357     apply left_identity.
 358     intros.
 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']].
 364     simpl in *.
 365     setoid_rewrite juggle3.
 366     setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
 367     setoid_rewrite <- juggle3.
 368     setoid_rewrite <- fmor_preserves_comp.
 369     reflexivity.
 370     Defined.
 371
 372   Definition center_I : Center mc := exist _ pI I.
 373
 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.
 376       intros.
 377       destruct A; simpl.
 378       set (ni_iso (pmon_cancelr mc) x) as q.
 379       (*refine {| iso_forward := #q ; iso_backward := iso_backward q |}.*)
 380       admit.
 381       Defined.
 382     refine {| ni_iso := center_cancelr_niso |}.
 383     admit.
 384     Defined.
 385
 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.
 388       admit.
 389       Defined.
 390     refine {| ni_iso := center_cancell_niso |}.
 391     admit.
 392     Defined.
 393
 394   Definition center_assoc :
 395     ((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F)
 396     <~~~> func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F)).
 397
 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).
 401       admit.
 402       Defined.
 403
 404     refine {| ni_iso := center_assoc_niso |}.
 405     admit.
 406     Defined.
 407
 408   Instance CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I) :=
 409   { mon_cancelr := center_cancelr
 410   ; mon_cancell := center_cancell
 411   ; mon_assoc   := center_assoc
 412   }.
 413     admit.
 414     admit.
 415     Defined.
 416
 417 End CenterMonoidal.