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