src/MonoidalCategories_ch7_8.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
  15 (******************************************************************************)
  16 (* Chapter 7.8: Monoidal Categories                                           *)
  17 (******************************************************************************)
  18
  19 Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
  20 { mon_f         := F
  21 ; mon_i         := I
  22 ; mon_c         := C
  23 ; mon_first     := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
  24 ; mon_second    := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
  25 ; mon_cancelr   :  (func_rlecnac I >>>> F) <~~~> functor_id C
  26 ; mon_cancell   :  (func_llecnac I >>>> F) <~~~> functor_id C
  27 ; mon_assoc     :  ((F **** (functor_id C)) >>>> F) <~~~> func_cossa >>>> ((((functor_id C) **** F) >>>> F))
  28 ; mon_pentagon  :  Pentagon mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
  29 ; mon_triangle  :  Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
  30                                                  (fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
  31 }.
  32 (* Coq manual on coercions: ... only the oldest one is valid and the
  33  * others are ignored. So the order of declaration of coercions is
  34  * important. *)
  35 Coercion mon_c   : MonoidalCat >-> Category.
  36 Coercion mon_f   : MonoidalCat >-> Functor.
  37 Implicit Arguments mon_f [Ob Hom C Fobj F I].
  38 Implicit Arguments mon_i [Ob Hom C Fobj F I].
  39 Implicit Arguments mon_c [Ob Hom C Fobj F I].
  40 Implicit Arguments MonoidalCat [Ob Hom ].
  41
  42 (* TO DO: show that the endofunctors on any given category form a monoidal category *)
  43 Section MonoidalFunctor.
  44   Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
  45   Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
  46   { mf_f         := mf_F where "f ⊕⊕ g" := (@fmor _ _ _ _ _ _ _ m2 _ _ (pair_mor (pair_obj _ _) (pair_obj _ _) f g))
  47   ; mf_coherence :  (mf_F **** mf_F) >>>> (mon_f m2) <~~~> (mon_f m1) >>>> mf_F
  48   ; mf_phi       := fun a b => #(mf_coherence (pair_obj a b))
  49   ; mf_id        :  (mon_i m2) ≅ (mf_F (mon_i m1))
  50   ; mf_cancelr   :  forall a,    #(mon_cancelr(MonoidalCat:=m2) (mf_F a)) ~~
  51                                   (id (mf_F a)) ⊕⊕ #mf_id >>> mf_phi a (mon_i _) >>> mf_F \ #(mon_cancelr a)
  52   ; mf_cancell   :  forall b,    #(mon_cancell (mf_F b)) ~~
  53                                  #mf_id ⊕⊕ (id (mf_F b)) >>> mf_phi (mon_i _) b >>> mf_F \ #(mon_cancell b)
  54   ; mf_assoc     :  forall a b c, (mf_phi a b) ⊕⊕ (id (mf_F c)) >>> (mf_phi _ c) >>>
  55                                   (mf_F \ #(mon_assoc (pair_obj (pair_obj a b) c) )) ~~
  56                                           #(mon_assoc (pair_obj (pair_obj _ _) _) )  >>>
  57                                   (id (mf_F a)) ⊕⊕ (mf_phi b c) >>> (mf_phi a _)
  58   }.
  59 End MonoidalFunctor.
  60 Coercion mf_f : MonoidalFunctor >-> Functor.
  61 Implicit Arguments mf_coherence [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
  62 Implicit Arguments mf_id        [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
  63
  64 Section MonoidalFunctorsCompose.
  65   Context `(m1:MonoidalCat).
  66   Context `(m2:MonoidalCat).
  67   Context `(m3:MonoidalCat).
  68   Context  {f1obj}(f1:@Functor _ _ m1 _ _ m2 f1obj).
  69   Context  {f2obj}(f2:@Functor _ _ m2 _ _ m3 f2obj).
  70   Context  (mf1:MonoidalFunctor m1 m2 f1).
  71   Context  (mf2:MonoidalFunctor m2 m3 f2).
  72
  73   Lemma mf_compose_coherence : (f1 >>>> f2) **** (f1 >>>> f2) >>>> m3 <~~~> m1 >>>> (f1 >>>> f2).
  74     set (mf_coherence mf1) as mc1.
  75     set (mf_coherence mf2) as mc2.
  76     set (@ni_comp) as q.
  77     set (q _ _ _ _ _ _ _ ((f1 >>>> f2) **** (f1 >>>> f2) >>>> m3) _ ((f1 **** f1 >>>> m2) >>>> f2) _ (m1 >>>> (f1 >>>> f2))) as qq.
  78     apply qq; clear qq; clear q.
  79     apply (@ni_comp _ _ _ _ _ _ _ _ _ (f1 **** f1 >>>> (f2 **** f2 >>>> m3)) _ _).
  80     apply (@ni_comp _ _ _ _ _ _ _ _ _ ((f1 **** f1 >>>> f2 **** f2) >>>> m3) _ _).
  81     eapply ni_respects.
  82       apply ni_prod_comp.
  83       apply ni_id.
  84     apply ni_associativity.
  85     apply ni_inv.
  86     eapply ni_comp.
  87       apply (ni_associativity (f1 **** f1) m2 f2).
  88       apply (ni_respects (F0:=f1 **** f1)(F1:=f1 **** f1)(G0:=(m2 >>>> f2))(G1:=(f2 **** f2 >>>> m3))).
  89         apply ni_id.
  90         apply ni_inv.
  91         apply mc2.
  92     apply ni_inv.
  93     eapply ni_comp.
  94       eapply ni_inv.
  95       apply (ni_associativity m1 f1 f2).
  96       apply ni_respects.
  97         apply ni_inv.
  98         apply mc1.
  99         apply ni_id.
 100   Defined.
 101
 102   Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
 103   { mf_id        := id_comp         (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
 104   ; mf_coherence := mf_compose_coherence
 105   }.
 106   admit.
 107   admit.
 108   admit.
 109   Defined.
 110
 111 End MonoidalFunctorsCompose.
 112
 113 Section MonoidalCat_is_PreMonoidal.
 114   Context `(M:MonoidalCat).
 115   Definition mon_bin_M := BinoidalCat_from_Bifunctor (mon_f M).
 116   Existing Instance mon_bin_M.
 117
 118   Lemma mon_pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a).
 119     intros.
 120     set (fun c => mon_assoc (pair_obj (pair_obj a c) b)) as qq.
 121     simpl in qq.
 122     apply Build_NaturalIsomorphism with (ni_iso:=qq).
 123     abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
 124                     (pair_mor (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
 125                     (pair_mor (pair_obj a A) (pair_obj a B) (id a) f) (id b))) as qr;
 126              apply qr).
 127     Defined.
 128
 129   Lemma mon_pmon_assoc_rr   :  forall a b, (bin_first  (a⊗b)) <~~~> (bin_first  a >>>> bin_first  b).
 130     intros.
 131     set (fun c:C => mon_assoc (pair_obj (pair_obj c a) b)) as qq.
 132     simpl in qq.
 133     apply ni_inv.
 134     apply Build_NaturalIsomorphism with (ni_iso:=qq).
 135     abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
 136                     (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
 137                     (pair_mor (pair_obj _ _) (pair_obj _ _) f (id a)) (id b))) as qr;
 138               etransitivity; [ idtac | apply qr ];
 139               apply comp_respects; try reflexivity;
 140               unfold mon_f;
 141               simpl;
 142               apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
 143               split; try reflexivity;
 144               symmetry;
 145               simpl;
 146               set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
 147               simpl in qqqq;
 148               apply qqqq).
 149    Defined.
 150
 151   Lemma mon_pmon_assoc_ll   :  forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a).
 152     intros.
 153     set (fun c:C => mon_assoc (pair_obj (pair_obj a b) c)) as qq.
 154     simpl in qq.
 155     set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (Fobj (pair_obj a b) ⋊-) (b ⋊- >>>> a ⋊-)) as qqq.
 156     set (qqq qq) as q'.
 157     apply q'.
 158     clear q'.
 159     clear qqq.
 160     abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
 161                     (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
 162                     (pair_mor (pair_obj _ _) (pair_obj _ _) (id a) (id b)) f)) as qr;
 163               etransitivity; [ apply qr | idtac ];
 164               apply comp_respects; try reflexivity;
 165               unfold mon_f;
 166               simpl;
 167               apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
 168               split; try reflexivity;
 169               simpl;
 170               set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
 171               simpl in qqqq;
 172               apply qqqq).
 173     Defined.
 174
 175   Lemma mon_pmon_cancelr : (bin_first I0) <~~~> functor_id C.
 176     set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_first I0) (functor_id C)) as qq.
 177     set (mon_cancelr) as z.
 178     simpl in z.
 179     simpl in qq.
 180     set (qq z) as zz.
 181     apply zz.
 182     abstract (intros;
 183               set (ni_commutes mon_cancelr) as q; simpl in *;
 184               apply q).
 185     Defined.
 186
 187   Lemma mon_pmon_cancell : (bin_second I0) <~~~> functor_id C.
 188     set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_second I0) (functor_id C)) as qq.
 189     set (mon_cancell) as z.
 190     simpl in z.
 191     simpl in qq.
 192     set (qq z) as zz.
 193     apply zz.
 194     abstract (intros;
 195               set (ni_commutes mon_cancell) as q; simpl in *;
 196               apply q).
 197     Defined.
 198
 199   Lemma mon_pmon_triangle : forall a b, #(mon_pmon_cancelr a) ⋉ b ~~ #(mon_pmon_assoc _ _ _) >>> a ⋊ #(mon_pmon_cancell b).
 200     intros.
 201     set mon_triangle as q.
 202     simpl in q.
 203     apply q.
 204     Qed.
 205
 206   Lemma mon_pmon_pentagon a b c d : (#(mon_pmon_assoc a c b ) ⋉ d)  >>>
 207                                      #(mon_pmon_assoc a d _ )   >>>
 208                                 (a ⋊ #(mon_pmon_assoc b d c))
 209                                   ~~ #(mon_pmon_assoc _ d c )   >>>
 210                                      #(mon_pmon_assoc a _ b ).
 211     set (@pentagon _ _ _ _ _ _ _ mon_pentagon) as x.
 212     simpl in x.
 213     unfold bin_obj.
 214     unfold mon_first in x.
 215     simpl in *.
 216     apply x.
 217     Qed.
 218
 219   Definition MonoidalCat_is_PreMonoidal : PreMonoidalCat (BinoidalCat_from_Bifunctor (mon_f M)) (mon_i M).
 220     refine {| pmon_assoc                 := mon_pmon_assoc
 221             ; pmon_cancell               := mon_pmon_cancell
 222             ; pmon_cancelr               := mon_pmon_cancelr
 223             ; pmon_triangle              := {| triangle := mon_pmon_triangle |}
 224             ; pmon_pentagon              := {| pentagon := mon_pmon_pentagon |}
 225             ; pmon_assoc_ll              := mon_pmon_assoc_ll
 226             ; pmon_assoc_rr              := mon_pmon_assoc_rr
 227             |}.
 228     abstract (set (coincide mon_triangle) as qq; simpl in *; apply qq).
 229     abstract (intros; simpl; reflexivity).
 230     abstract (intros; simpl; reflexivity).
 231     Defined.
 232
 233   Lemma MonoidalCat_all_central : forall a b (f:a~~{M}~~>b), CentralMorphism f.
 234     intros;
 235     set (@fmor_preserves_comp _ _ _ _ _ _ _ M) as fc.
 236     apply Build_CentralMorphism;
 237     intros; simpl in *.
 238     etransitivity.
 239       apply fc.
 240       symmetry.
 241       etransitivity.
 242       apply fc.
 243       apply (fmor_respects M).
 244       simpl.
 245       setoid_rewrite left_identity;
 246       setoid_rewrite right_identity;
 247       split; reflexivity.
 248     etransitivity.
 249       apply fc.
 250       symmetry.
 251       etransitivity.
 252       apply fc.
 253       apply (fmor_respects M).
 254       simpl.
 255       setoid_rewrite left_identity;
 256       setoid_rewrite right_identity;
 257       split; reflexivity.
 258     Qed.
 259
 260 End MonoidalCat_is_PreMonoidal.
 261
 262 Hint Extern 1 => apply MonoidalCat_all_central.
 263 Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
 264
 265 (* Later: generalize to premonoidal categories *)
 266 Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
 267 {  copy_nt      :  forall a, functor_id _ ~~~> func_diagonal >>>> F
 268 ;  copy         :  forall (a:mc),   a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
 269                 := fun a => nt_component _ _ (copy_nt a) a
 270 (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
 271 }.
 272
 273 Class CartesianCat `(mc:MonoidalCat) :=
 274 { car_terminal  : Terminal mc
 275 ; car_one       : (@one _ _ _ car_terminal) ≅ (mon_i mc)
 276 ; car_diagonal  : DiagonalCat mc
 277 ; car_law1      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
 278 ; car_law2      : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
 279 ; car_mn        := mc
 280 }.
 281 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
 282 Coercion car_terminal : CartesianCat >-> Terminal.
 283 Coercion car_mn       : CartesianCat >-> MonoidalCat.