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