src/Isomorphisms_ch1_5.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5
   6 (******************************************************************************)
   7 (* Chapter 1.5: Isomorphisms                                                  *)
   8 (******************************************************************************)
   9
  10 Class Isomorphism `{C:Category}{a b:C}(f:a~>b)(g:b~>a) : Prop :=
  11 { iso_cmp1  : f >>> g ~~ id a
  12 ; iso_cmp2  : g >>> f ~~ id b
  13 }.
  14 (* TO DO: show isos are unique when they exist *)
  15
  16 Class Isomorphic
  17 `{ C           :  Category                                   }
  18 ( a b          :  C                                          ) :=
  19 { iso_forward  :  a~>b
  20 ; iso_backward :  b~>a
  21 ; iso_comp1    :  iso_forward >>> iso_backward ~~ id a
  22 ; iso_comp2    :  iso_backward >>> iso_forward ~~ id b
  23 (* TO DO: merge this with Isomorphism *)
  24 }.
  25 Implicit Arguments iso_forward  [ C a b Ob Hom ].
  26 Implicit Arguments iso_backward [ C a b Ob Hom ].
  27 Implicit Arguments iso_comp1    [ C a b Ob Hom ].
  28 Implicit Arguments iso_comp2    [ C a b Ob Hom ].
  29 Notation "a ≅ b" := (Isomorphic a b)    : isomorphism_scope.
  30 (* the sharp symbol "casts" an isomorphism to the morphism in the forward direction *)
  31 Notation "# f" := (@iso_forward _ _ _ _ _ f) : isomorphism_scope.
  32 Open Scope isomorphism_scope.
  33
  34 (* the inverse of an isomorphism is an isomorphism *)
  35 Definition iso_inv `{C:Category}(a b:C)(is:Isomorphic a b) : Isomorphic b a.
  36   intros; apply (Build_Isomorphic _ _ _ _ _ (iso_backward _) (iso_forward _));
  37   [ apply iso_comp2 | apply iso_comp1 ].
  38   Defined.
  39 Notation "f '⁻¹'" := (@iso_inv _ _ _ _ _ f) : isomorphism_scope.
  40
  41 (* identity maps are isomorphisms *)
  42 Definition iso_id `{C:Category}(A:C) : Isomorphic A A.
  43   intros; apply (Build_Isomorphic _ _ C A A (id A) (id A)); auto.
  44   Defined.
  45
  46 (* the composition of two isomorphisms is an isomorphism *)
  47 Definition iso_comp `{C:Category}{a b c:C}(i1:Isomorphic a b)(i2:Isomorphic b c) : Isomorphic a c.
  48   intros; apply (@Build_Isomorphic _ _ C a c (#i1 >>> #i2) (#i2⁻¹ >>> #i1⁻¹));
  49     setoid_rewrite juggle3;
  50     [ setoid_rewrite (iso_comp1 i2) | setoid_rewrite (iso_comp2 i1) ];
  51     setoid_rewrite right_identity;
  52     [ setoid_rewrite (iso_comp1 i1) | setoid_rewrite (iso_comp2 i2) ];
  53     reflexivity.
  54   Defined.
  55 Notation "a >>≅>> b" := (iso_comp a b).
  56
  57 Definition functors_preserve_isos `{C1:Category}`{C2:Category}{Fo}(F:Functor C1 C2 Fo){a b:C1}(i:Isomorphic a b)
  58   : Isomorphic (F a) (F b).
  59   refine {| iso_forward  := F \ (iso_forward  i)
  60           ; iso_backward := F \ (iso_backward i)
  61           |}.
  62   setoid_rewrite fmor_preserves_comp.
  63     setoid_rewrite iso_comp1.
  64     apply fmor_preserves_id.
  65   setoid_rewrite fmor_preserves_comp.
  66     setoid_rewrite iso_comp2.
  67     apply fmor_preserves_id.
  68   Defined.
  69
  70 Lemma iso_shift_right `{C:Category} : forall {a b c:C}(f:b~>c)(g:a~>c)(i:Isomorphic b a), #i⁻¹ >>> f ~~ g -> f ~~ #i >>> g.
  71   intros.
  72   setoid_rewrite <- H.
  73   setoid_rewrite <- associativity.
  74   setoid_rewrite iso_comp1.
  75   symmetry.
  76   apply left_identity.
  77   Qed.
  78
  79 Lemma iso_shift_right' `{C:Category} : forall {a b c:C}(f:b~>c)(g:a~>c)(i:Isomorphic a b), #i >>> f ~~ g -> f ~~ #i⁻¹ >>> g.
  80   intros.
  81   setoid_rewrite <- H.
  82   setoid_rewrite <- associativity.
  83   setoid_rewrite iso_comp1.
  84   symmetry.
  85   apply left_identity.
  86   Qed.
  87
  88 Lemma iso_shift_left `{C:Category} : forall {a b c:C}(f:a~>b)(g:a~>c)(i:Isomorphic c b), f >>> #i⁻¹ ~~ g -> f ~~ g >>> #i.
  89   intros.
  90   setoid_rewrite <- H.
  91   setoid_rewrite associativity.
  92   setoid_rewrite iso_comp1.
  93   symmetry.
  94   apply right_identity.
  95   Qed.
  96
  97 Lemma iso_shift_left' `{C:Category} : forall {a b c:C}(f:a~>b)(g:a~>c)(i:Isomorphic b c), f >>> #i ~~ g -> f ~~ g >>> #i⁻¹.
  98   intros.
  99   setoid_rewrite <- H.
 100   setoid_rewrite associativity.
 101   setoid_rewrite iso_comp1.
 102   symmetry.
 103   apply right_identity.
 104   Qed.
 105
 106 Lemma isos_forward_equal_then_backward_equal `{C:Category}{a}{b}(i1 i2:a ≅ b) : #i1 ~~ #i2 ->  #i1⁻¹ ~~ #i2⁻¹.
 107   intro H.
 108   setoid_rewrite <- left_identity at 1.
 109   setoid_rewrite <- (iso_comp2 i2).
 110   setoid_rewrite associativity.
 111   setoid_rewrite <- H.
 112   setoid_rewrite iso_comp1.
 113   setoid_rewrite right_identity.
 114   reflexivity.
 115   Qed.
 116
 117 Lemma iso_inv_inv `{C:Category}{a}{b}(i:a ≅ b) : #(i⁻¹)⁻¹ ~~ #i.
 118   unfold iso_inv; simpl.
 119   reflexivity.
 120   Qed.
 121
 122 (* the next four lemmas are handy for setoid_rewrite; they let you avoid having to get the associativities right *)
 123 Lemma iso_comp2_right : forall `{C:Category}{a b}(i:a≅b) c (g:b~>c), iso_backward i >>> (iso_forward i >>> g) ~~ g.
 124   intros.
 125   setoid_rewrite <- associativity.
 126   setoid_rewrite iso_comp2.
 127   apply left_identity.
 128   Qed.
 129
 130 Lemma iso_comp2_left : forall `{C:Category}{a b}(i:a≅b) c (g:c~>b), (g >>> iso_backward i) >>> iso_forward i ~~ g.
 131   intros.
 132   setoid_rewrite associativity.
 133   setoid_rewrite iso_comp2.
 134   apply right_identity.
 135   Qed.
 136
 137 Lemma iso_comp1_right : forall `{C:Category}{a b}(i:a≅b) c (g:a~>c), iso_forward i >>> (iso_backward i >>> g) ~~ g.
 138   intros.
 139   setoid_rewrite <- associativity.
 140   setoid_rewrite iso_comp1.
 141   apply left_identity.
 142   Qed.
 143
 144 Lemma iso_comp1_left : forall `{C:Category}{a b}(i:a≅b) c (g:c~>a), (g >>> iso_forward i) >>> iso_backward i ~~ g.
 145   intros.
 146   setoid_rewrite associativity.
 147   setoid_rewrite iso_comp1.
 148   apply right_identity.
 149   Qed.