src/NaturalIsomorphisms_ch7_5.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
   7 (*******************************************************************************)
   8 (* Chapter 7.5: Natural Isomorphisms                                           *)
   9 (*******************************************************************************)
  10
  11 (* Definition 7.10 *)
  12 Class NaturalIsomorphism `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
  13 { ni_iso      : forall A, Fobj1 A ≅ Fobj2 A
  14 ; ni_commutes : forall `(f:A~>B), #(ni_iso A) >>> F2 \ f ~~ F1 \ f >>> #(ni_iso B)
  15 }.
  16 Implicit Arguments ni_iso      [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2].
  17 Implicit Arguments ni_commutes [Ob Hom Ob0 Hom0 C1 C2 Fobj1 Fobj2 F1 F2 A B].
  18 (* FIXME: coerce to NaturalTransformation instead *)
  19 Coercion ni_iso : NaturalIsomorphism >-> Funclass.
  20 Notation "F <~~~> G" := (@NaturalIsomorphism _ _ _ _ _ _ _ _ F G) : category_scope.
  21
  22 (* FIXME: Lemma 7.11: natural isos are natural transformations in which every morphism is an iso *)
  23
  24 (* every natural iso is invertible, and that inverse is also a natural iso *)
  25 Definition ni_inv `(N:NaturalIsomorphism(F1:=F1)(F2:=F2)) : NaturalIsomorphism F2 F1.
  26   intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F2 F1 (fun A => iso_inv _ _ (ni_iso N A))).
  27   abstract (intros; simpl;
  28             set (ni_commutes N f) as qqq;
  29             symmetry in qqq;
  30             apply iso_shift_left' in qqq;
  31             setoid_rewrite qqq;
  32             repeat setoid_rewrite <- associativity;
  33             setoid_rewrite iso_comp2;
  34             setoid_rewrite left_identity;
  35             reflexivity).
  36   Defined.
  37
  38 Definition ni_id
  39   `{C1:Category}`{C2:Category}
  40   {Fobj}(F:Functor C1 C2 Fobj)
  41   : NaturalIsomorphism F F.
  42   intros; apply (Build_NaturalIsomorphism _ _ _ _ _ _ _ _ F F (fun A => iso_id (F A))).
  43   abstract (intros; simpl; setoid_rewrite left_identity; setoid_rewrite right_identity; reflexivity).
  44   Defined.
  45
  46 (* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
  47 Instance ni_associativity
  48   `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
  49   {Fobj1}(F1:Functor C1 C2 Fobj1)
  50   {Fobj2}(F2:Functor C2 C3 Fobj2)
  51   {Fobj3}(F3:Functor C3 C4 Fobj3)
  52   :
  53   ((F1 >>>> F2) >>>> F3) <~~~> (F1 >>>> (F2 >>>> F3)) :=
  54   { ni_iso := fun A => iso_id (F3 (F2 (F1 A))) }.
  55   abstract (intros;
  56             simpl;
  57             setoid_rewrite left_identity;
  58             setoid_rewrite right_identity;
  59             reflexivity).
  60   Defined.
  61
  62 Definition ni_comp `{C:Category}`{D:Category}
  63    {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
  64    {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
  65    {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
  66    (N1:NaturalIsomorphism F1 F2)
  67    (N2:NaturalIsomorphism F2 F3)
  68    : NaturalIsomorphism F1 F3.
  69    intros.
  70      destruct N1 as [ ni_iso1 ni_commutes1 ].
  71      destruct N2 as [ ni_iso2 ni_commutes2 ].
  72    exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)).
  73    abstract (intros; simpl;
  74              setoid_rewrite <- associativity;
  75              setoid_rewrite <- ni_commutes1;
  76              setoid_rewrite associativity;
  77              setoid_rewrite <- ni_commutes2;
  78              reflexivity).
  79    Defined.
  80
  81 Definition ni_respects1
  82   `{A:Category}`{B:Category}
  83   {Fobj}(F:Functor A B Fobj)
  84   `{C:Category}
  85   {G0obj}(G0:Functor B C G0obj)
  86   {G1obj}(G1:Functor B C G1obj)
  87   : (G0 <~~~> G1) -> ((F >>>> G0) <~~~> (F >>>> G1)).
  88   intro phi.
  89   destruct phi as [ phi_niso phi_comm ].
  90   refine {| ni_iso := (fun a => phi_niso (Fobj a)) |}.
  91   intros; simpl; apply phi_comm.
  92   Defined.
  93
  94 Definition ni_respects2
  95   `{A:Category}`{B:Category}
  96   {F0obj}(F0:Functor A B F0obj)
  97   {F1obj}(F1:Functor A B F1obj)
  98   `{C:Category}
  99   {Gobj}(G:Functor B C Gobj)
 100   : (F0 <~~~> F1) -> ((F0 >>>> G) <~~~> (F1 >>>> G)).
 101   intro phi.
 102   destruct phi as [ phi_niso phi_comm ].
 103   refine {| ni_iso := fun a => (@functors_preserve_isos _ _ _ _ _ _ _ G) _ _ (phi_niso a) |}.
 104   intros; simpl.
 105   setoid_rewrite fmor_preserves_comp.
 106   apply fmor_respects.
 107   apply phi_comm.
 108   Defined.
 109
 110 Definition ni_respects
 111   `{A:Category}`{B:Category}
 112   {F0obj}(F0:Functor A B F0obj)
 113   {F1obj}(F1:Functor A B F1obj)
 114   `{C:Category}
 115   {G0obj}(G0:Functor B C G0obj)
 116   {G1obj}(G1:Functor B C G1obj)
 117   : (F0 <~~~> F1) -> (G0 <~~~> G1) -> ((F0 >>>> G0) <~~~> (F1 >>>> G1)).
 118   intro phi.
 119   intro psi.
 120   destruct psi as [ psi_niso psi_comm ].
 121   destruct phi as [ phi_niso phi_comm ].
 122   refine {| ni_iso :=
 123       (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))) |}.
 124   abstract (intros; simpl;
 125             setoid_rewrite <- associativity;
 126             setoid_rewrite fmor_preserves_comp;
 127             setoid_rewrite <- phi_comm;
 128             setoid_rewrite <- fmor_preserves_comp;
 129             setoid_rewrite associativity;
 130             apply comp_respects; try reflexivity;
 131             apply psi_comm).
 132   Defined.
 133
 134 (*
 135  * Some structures (like monoidal and premonoidal functors) use the isomorphism
 136  * component of a natural isomorphism in an "informative" way; these structures
 137  * should use NaturalIsomorphism.
 138  *
 139  * However, in other situations the actual iso used is irrelevant; all
 140  * that matters is the fact that a natural family of them exists.  In
 141  * these cases we can speed up Coq (and the extracted program)
 142  * considerably by making the family of isos belong to [Prop] rather
 143  * than [Type].  IsomorphicFunctors does this -- it's essentially a
 144  * copy of NaturalIsomorphism which lives in [Prop].
 145  *)
 146
 147 (* Definition 7.10 *)
 148 Definition IsomorphicFunctors `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}(F1:Functor C1 C2 Fobj1)(F2:Functor C1 C2 Fobj2) :=
 149   exists  ni_iso      : (forall A, Fobj1 A ≅ Fobj2 A),
 150                          forall `(f:A~>B), #(ni_iso A) >>> F2 \ f ~~ F1 \ f >>> #(ni_iso B).
 151 Notation "F ≃ G" := (@IsomorphicFunctors _ _ _ _ _ _ _ _ F G) : category_scope.
 152
 153 Definition if_id `{C:Category}`{D:Category}{Fobj}(F:Functor C D Fobj) : IsomorphicFunctors F F.
 154   exists (fun A => iso_id (F A)).
 155   abstract (intros;
 156             simpl;
 157             etransitivity;
 158             [ apply left_identity |
 159             symmetry;
 160             apply right_identity]).
 161   Qed.
 162
 163 (* every natural iso is invertible, and that inverse is also a natural iso *)
 164 Definition if_inv
 165   `{C1:Category}`{C2:Category}{Fobj1 Fobj2:C1->C2}{F1:Functor C1 C2 Fobj1}{F2:Functor C1 C2 Fobj2}
 166    (N:IsomorphicFunctors F1 F2) : IsomorphicFunctors F2 F1.
 167   intros.
 168     destruct N as [ ni_iso ni_commutes ].
 169     exists (fun A => iso_inv _ _ (ni_iso A)).
 170   intros; simpl.
 171     symmetry.
 172     set (ni_commutes _ _ f) as qq.
 173     symmetry in qq.
 174     apply iso_shift_left' in qq.
 175     setoid_rewrite qq.
 176     repeat setoid_rewrite <- associativity.
 177     setoid_rewrite iso_comp2.
 178     setoid_rewrite left_identity.
 179     reflexivity.
 180   Qed.
 181
 182 Definition if_comp `{C:Category}`{D:Category}
 183    {F1Obj}{F1:@Functor _ _ C _ _ D F1Obj}
 184    {F2Obj}{F2:@Functor _ _ C _ _ D F2Obj}
 185    {F3Obj}{F3:@Functor _ _ C _ _ D F3Obj}
 186    (N1:IsomorphicFunctors F1 F2)
 187    (N2:IsomorphicFunctors F2 F3)
 188    : IsomorphicFunctors F1 F3.
 189    intros.
 190      destruct N1 as [ ni_iso1 ni_commutes1 ].
 191      destruct N2 as [ ni_iso2 ni_commutes2 ].
 192    exists (fun A => iso_comp (ni_iso1 A) (ni_iso2 A)).
 193    abstract (intros; simpl;
 194              setoid_rewrite <- associativity;
 195              setoid_rewrite <- ni_commutes1;
 196              setoid_rewrite associativity;
 197              setoid_rewrite <- ni_commutes2;
 198              reflexivity).
 199    Qed.
 200
 201 (* two different choices of composition order are naturally isomorphic (strictly, in fact) *)
 202 Definition if_associativity
 203   `{C1:Category}`{C2:Category}`{C3:Category}`{C4:Category}
 204   {Fobj1}(F1:Functor C1 C2 Fobj1)
 205   {Fobj2}(F2:Functor C2 C3 Fobj2)
 206   {Fobj3}(F3:Functor C3 C4 Fobj3)
 207   :
 208   ((F1 >>>> F2) >>>> F3) ≃ (F1 >>>> (F2 >>>> F3)).
 209   exists (fun A => iso_id (F3 (F2 (F1 A)))).
 210   abstract (intros;
 211             simpl;
 212             setoid_rewrite left_identity;
 213             setoid_rewrite right_identity;
 214             reflexivity).
 215   Defined.
 216
 217 Definition if_left_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 C2 Fobj1) : (functor_id _ >>>> F1) ≃ F1.
 218   exists (fun a => iso_id (F1 a)).
 219   abstract (intros; unfold functor_comp; simpl;
 220             setoid_rewrite left_identity;
 221             setoid_rewrite right_identity;
 222             reflexivity).
 223   Defined.
 224
 225 Definition if_right_identity `{C1:Category}`{C2:Category} {Fobj1}(F1:Functor C1 C2 Fobj1) : (F1 >>>> functor_id _) ≃ F1.
 226   exists (fun a => iso_id (F1 a)).
 227   abstract (intros; unfold functor_comp; simpl;
 228             setoid_rewrite left_identity;
 229             setoid_rewrite right_identity;
 230             reflexivity).
 231   Defined.
 232
 233 Definition if_respects
 234   `{A:Category}`{B:Category}
 235   {F0obj}(F0:Functor A B F0obj)
 236   {F1obj}(F1:Functor A B F1obj)
 237   `{C:Category}
 238   {G0obj}(G0:Functor B C G0obj)
 239   {G1obj}(G1:Functor B C G1obj)
 240   : (F0 ≃ F1) -> (G0 ≃ G1) -> ((F0 >>>> G0) ≃ (F1 >>>> G1)).
 241   intro phi.
 242   intro psi.
 243   destruct psi as [ psi_niso psi_comm ].
 244   destruct phi as [ phi_niso phi_comm ].
 245   exists (fun a => iso_comp ((@functors_preserve_isos _ _ _ _ _ _ _ G0) _ _ (phi_niso a)) (psi_niso (F1obj a))).
 246   abstract (intros; simpl;
 247             setoid_rewrite <- associativity;
 248             setoid_rewrite fmor_preserves_comp;
 249             setoid_rewrite <- phi_comm;
 250             setoid_rewrite <- fmor_preserves_comp;
 251             setoid_rewrite associativity;
 252             apply comp_respects; try reflexivity;
 253             apply psi_comm).
 254   Defined.
 255
 256 Section ni_prod_comp.
 257 Require Import ProductCategories_ch1_6_1.
 258   Context
 259   `{C1:Category}`{C2:Category}
 260   `{D1:Category}`{D2:Category}
 261    {F1Obj}(F1:@Functor _ _ C1 _ _ D1 F1Obj)
 262    {F2Obj}(F2:@Functor _ _ C2 _ _ D2 F2Obj)
 263   `{E1:Category}`{E2:Category}
 264    {G1Obj}(G1:@Functor _ _ D1 _ _ E1 G1Obj)
 265    {G2Obj}(G2:@Functor _ _ D2 _ _ E2 G2Obj).
 266
 267   Definition ni_prod_comp_iso A : (((F1 >>>> G1) **** (F2 >>>> G2)) A) ≅ (((F1 **** F2) >>>> (G1 **** G2)) A).
 268     unfold functor_fobj.
 269     unfold functor_product_fobj.
 270     simpl.
 271     apply iso_id.
 272     Defined.
 273
 274   Lemma ni_prod_comp : (F1 >>>> G1) **** (F2 >>>> G2) <~~~> (F1 **** F2) >>>> (G1 **** G2).
 275     refine {| ni_iso := ni_prod_comp_iso |}.
 276     intros.
 277     destruct A.
 278     destruct B.
 279     simpl.
 280     setoid_rewrite left_identity.
 281     setoid_rewrite right_identity.
 282     split; reflexivity.
 283     Defined.
 284 End ni_prod_comp.
 285