src/MonoidalCategories_ch7_8.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 ProductCategories_ch1_6_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 (* TO DO: show that the endofunctors on any given category form a monoidal category *)
  20
  21 (*
  22  * Unlike Awodey, I define a monoidal category to be a premonoidal
  23  * category in which all morphisms are central.  This is partly to
  24  * have a clean inheritance hierarchy, but also because Coq bogs down
  25  * on product categories for some inexplicable reason.
  26  *)
  27 Class MonoidalCat `(pm:PreMonoidalCat) :=
  28 { mon_pm          := pm
  29 ; mon_commutative :> CommutativeCat pm
  30 }.
  31 Coercion mon_pm          : MonoidalCat >-> PreMonoidalCat.
  32 Coercion mon_commutative : MonoidalCat >-> CommutativeCat.
  33
  34 (* a monoidal functor is just a premonoidal functor between premonoidal categories which happen to be monoidal *)
  35 Definition MonoidalFunctor `(m1:MonoidalCat) `(m2:MonoidalCat) {fobj}(F:Functor m1 m2 fobj) := PreMonoidalFunctor m1 m2 F.
  36
  37 Definition MonoidalFunctorsCompose
  38   `{PM1   :MonoidalCat(C:=C1)}
  39   `{PM2   :MonoidalCat(C:=C2)}
  40    {fobj12:C1 -> C2                    }
  41    {PMFF12:Functor C1 C2 fobj12        }
  42    (PMF12 :MonoidalFunctor PM1 PM2 PMFF12)
  43   `{PM3   :MonoidalCat(C:=C3)}
  44    {fobj23:C2 -> C3                    }
  45    {PMFF23:Functor C2 C3 fobj23        }
  46    (PMF23 :MonoidalFunctor PM2 PM3 PMFF23)
  47    := PreMonoidalFunctorsCompose PMF12 PMF23.
  48
  49 Class MonoidalNaturalIsomorphism
  50  `{C1:MonoidalCat}`{C2:MonoidalCat}
  51  `(F1:!MonoidalFunctor(fobj:=fobj1) C1 C2 Func1)
  52  `(F2:!MonoidalFunctor(fobj:=fobj2) C1 C2 Func2) :=
  53 { mni_ni        : NaturalIsomorphism F1 F2
  54 ; mni_commutes1 : forall A B,
  55                    #(ni_iso (mf_first(PreMonoidalFunctor:=F1) B) A)  >>> #(ni_iso mni_ni (A⊗B)) ~~
  56                    #(ni_iso mni_ni _) ⋉ _ >>> _ ⋊ #(ni_iso mni_ni _) >>> #(ni_iso (mf_first(PreMonoidalFunctor:=F2) B) A)
  57 ; mni_commutes2 : forall A B,
  58                    #(ni_iso (mf_second(PreMonoidalFunctor:=F1) A) B)  >>> #(ni_iso mni_ni (A⊗B)) ~~
  59                    #(ni_iso mni_ni _) ⋉ _ >>> _ ⋊ #(ni_iso mni_ni _) >>> #(ni_iso (mf_second(PreMonoidalFunctor:=F2) A) B)
  60 }.
  61 Notation "F <~~⊗~~> G" := (@MonoidalNaturalIsomorphism _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ F _ _ G) : category_scope.
  62
  63 (* an equivalence of categories via monoidal functors, but the natural iso isn't necessarily a monoidal natural iso *)
  64 Structure MonoidalEquivalence `{C1:MonoidalCat} `{C2:MonoidalCat} :=
  65 { meqv_forward_fobj  : C1 -> C2
  66 ; meqv_forward       : Functor C1 C2 meqv_forward_fobj
  67 ; meqv_forward_mon   : PreMonoidalFunctor _ _ meqv_forward
  68 ; meqv_backward_fobj : C2 -> C1
  69 ; meqv_backward      : Functor C2 C1 meqv_backward_fobj
  70 ; meqv_backward_mon  : PreMonoidalFunctor _ _ meqv_backward
  71 ; meqv_comp1         : meqv_forward  >>>> meqv_backward ≃ functor_id _
  72 ; meqv_comp2         : meqv_backward >>>> meqv_forward  ≃ functor_id _
  73 }.
  74
  75 (* a monoidally-natural equivalence of categories *)
  76 (*
  77 Structure MonoidalNaturalEquivalence `{C1:MonoidalCat} `{C2:MonoidalCat} :=
  78 { mneqv_forward_fobj  : C1 -> C2
  79 ; mneqv_forward       : Functor C1 C2 mneqv_forward_fobj
  80 ; mneqv_forward_mon   : PreMonoidalFunctor _ _ mneqv_forward
  81 ; mneqv_backward_fobj : C2 -> C1
  82 ; mneqv_backward      : Functor C2 C1 mneqv_backward_fobj
  83 ; mneqv_backward_mon  : PreMonoidalFunctor _ _ mneqv_backward
  84 ; mneqv_comp1         : mneqv_forward_mon  >>⊗>> mneqv_backward_mon <~~⊗~~> premonoidal_id _
  85 ; mneqv_comp2         : mneqv_backward_mon >>⊗>> mneqv_forward_mon  <~~⊗~~> premonoidal_id _
  86 }.
  87 *)
  88
  89 Section BinoidalCat_from_Bifunctor.
  90   Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
  91   Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
  92   apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
  93     @fmor _ _ _ _ _ _ _ F (pair_obj a0 a) (pair_obj b a) (pair_mor (pair_obj a0 a) (pair_obj b a) f (id a)))); intros; simpl;
  94     [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
  95     | abstract (set (fmor_preserves_id(F)) as q; apply q)
  96     | abstract (etransitivity;
  97       [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
  98       | set (fmor_respects(F)) as q; apply q ];
  99       split; simpl; auto) ].
 100   Defined.
 101   Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
 102   apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
 103     @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
 104     [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
 105     | abstract (set (fmor_preserves_id(F)) as q; apply q)
 106     | abstract (etransitivity;
 107       [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
 108       | set (fmor_respects(F)) as q; apply q ];
 109       split; simpl; auto) ].
 110   Defined.
 111
 112   Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
 113    refine {| bin_first  := BinoidalCat_from_Bifunctor_first
 114            ; bin_second := BinoidalCat_from_Bifunctor_second
 115           |}.
 116    Defined.
 117
 118   Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
 119   abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
 120     etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
 121     etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
 122     apply (fmor_respects(F));
 123     split;
 124       [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
 125       | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
 126   Defined.
 127
 128   (* if this binoidal structure has all of the natural isomorphisms of a premonoidal category, then it's monoidal *)
 129   Context {pmI}(pm:PreMonoidalCat BinoidalCat_from_Bifunctor pmI).
 130
 131   Instance PreMonoidalCat_from_bifunctor_is_Monoidal : MonoidalCat pm :=
 132   { mon_commutative := Bifunctors_Create_Commutative_Binoidal_Categories
 133   }.
 134
 135 End BinoidalCat_from_Bifunctor.
 136
 137
 138 (* we can go the other way: given a monoidal category, its left/right functors can be combined into a bifunctor *)
 139 Section Bifunctor_from_MonoidalCat.
 140   Context `(M:MonoidalCat).
 141
 142
 143   Definition Bifunctor_from_MonoidalCat_fobj : M ×× M -> M.
 144     intro x.
 145     destruct x.
 146     exact (bin_obj' o o0).
 147     Defined.
 148
 149   Definition Bifunctor_from_MonoidalCat_fmor {a}{b}(f:a~~{M××M}~~>b)
 150     : (Bifunctor_from_MonoidalCat_fobj a)~~{M}~~>(Bifunctor_from_MonoidalCat_fobj b).
 151     destruct a; destruct b; destruct f.
 152     simpl in *.
 153     apply (h ⋉ _ >>> _ ⋊ h0).
 154     Defined.
 155
 156   Instance Bifunctor_from_MonoidalCat : Functor (M ×× M) M Bifunctor_from_MonoidalCat_fobj :=
 157     { fmor := fun x y f => Bifunctor_from_MonoidalCat_fmor f }.
 158     intros; simpl.
 159     destruct a; destruct b; destruct f; destruct f'; simpl in *.
 160     destruct H.
 161     apply comp_respects.
 162       apply (fmor_respects (-⋉o0)); auto.
 163       apply (fmor_respects (o1⋊-)); auto.
 164     intros; destruct a; simpl in *.
 165       setoid_rewrite (fmor_preserves_id (-⋉o0)).
 166       setoid_rewrite left_identity.
 167       apply fmor_preserves_id.
 168     intros; destruct a; destruct b; destruct c; destruct f; destruct g; simpl in *.
 169       setoid_rewrite <- fmor_preserves_comp.
 170       setoid_rewrite juggle3 at 1.
 171       assert (CentralMorphism h1).
 172         apply mon_commutative.
 173       setoid_rewrite <- (centralmor_first(CentralMorphism:=H)).
 174       setoid_rewrite <- juggle3.
 175       reflexivity.
 176       Defined.
 177
 178 End Bifunctor_from_MonoidalCat.
 179
 180
 181 Class DiagonalCat `(mc:MonoidalCat) :=
 182 { copy          :  forall (a:mc),   a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
 183 ; copy_natural1 :  forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> f ⋉ a >>> b ⋊ f ~~ f >>> copy _
 184 ; copy_natural2 :  forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> a ⋊ f >>> f ⋉ b ~~ f >>> copy _
 185 (* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
 186 }.
 187
 188 Class CartesianCat `(mc:MonoidalCat) :=
 189 { car_terminal  :> TerminalObject mc (pmon_I mc)
 190 ; car_diagonal  :  DiagonalCat mc
 191 ; car_law1      :  forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (drop a  ⋉ a) >>> (#(pmon_cancell _))
 192 ; car_law2      :  forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ drop  a) >>> (#(pmon_cancelr _))
 193 ; car_mn        := mc
 194 }.
 195 Coercion car_diagonal : CartesianCat >-> DiagonalCat.
 196 Coercion car_terminal : CartesianCat >-> TerminalObject.
 197 Coercion car_mn       : CartesianCat >-> MonoidalCat.