1 Generalizable All Variables.
2 Require Import Preamble.
3 Require Import General.
4 Require Import Categories_ch1_3.
5 Require Import Functors_ch1_4.
7 (******************************************************************************)
8 (* Chapter 1.5: Isomorphisms                                                  *)
9 (******************************************************************************)
11 Class Isomorphism `{C:Category}{a b:C}(f:a~>b)(g:b~>a) : Prop :=
12 { iso_cmp1  : f >>> g ~~ id a
13 ; iso_cmp2  : g >>> f ~~ id b
14 }.
15 (* TO DO: show isos are unique when they exist *)
17 Class Isomorphic
18 `{ C           :  Category                                   }
19 ( a b          :  C                                          ) :=
20 { iso_forward  :  a~>b
21 ; iso_backward :  b~>a
22 ; iso_comp1    :  iso_forward >>> iso_backward ~~ id a
23 ; iso_comp2    :  iso_backward >>> iso_forward ~~ id b
24 (* TO DO: merge this with Isomorphism *)
25 }.
26 Implicit Arguments iso_forward  [ C a b Ob Hom ].
27 Implicit Arguments iso_backward [ C a b Ob Hom ].
28 Implicit Arguments iso_comp1    [ C a b Ob Hom ].
29 Implicit Arguments iso_comp2    [ C a b Ob Hom ].
30 Notation "a ≅ b" := (Isomorphic a b)    : isomorphism_scope.
31 (* the sharp symbol "casts" an isomorphism to the morphism in the forward direction *)
32 Notation "# f" := (@iso_forward _ _ _ _ _ f) : isomorphism_scope.
33 Open Scope isomorphism_scope.
35 (* the inverse of an isomorphism is an isomorphism *)
36 Definition iso_inv `{C:Category}(a b:C)(is:Isomorphic a b) : Isomorphic b a.
37   intros; apply (Build_Isomorphic _ _ _ _ _ (iso_backward _) (iso_forward _));
38   [ apply iso_comp2 | apply iso_comp1 ].
39   Defined.
40 Notation "f '⁻¹'" := (@iso_inv _ _ _ _ _ f) : isomorphism_scope.
42 (* identity maps are isomorphisms *)
43 Definition iso_id `{C:Category}(A:C) : Isomorphic A A.
44   intros; apply (Build_Isomorphic _ _ C A A (id A) (id A)); auto.
45   Defined.
47 (* the composition of two isomorphisms is an isomorphism *)
48 Definition id_comp `{C:Category}{a b c:C}(i1:Isomorphic a b)(i2:Isomorphic b c) : Isomorphic a c.
49   intros; apply (@Build_Isomorphic _ _ C a c (#i1 >>> #i2) (#i2⁻¹ >>> #i1⁻¹));
50     setoid_rewrite juggle3;
51     [ setoid_rewrite (iso_comp1 i2) | setoid_rewrite (iso_comp2 i1) ];
52     setoid_rewrite right_identity;
53     [ setoid_rewrite (iso_comp1 i1) | setoid_rewrite (iso_comp2 i2) ];
54     reflexivity.
55   Defined.
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.
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.
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.
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.
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.
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.
117 Lemma iso_inv_inv `{C:Category}{a}{b}(i:a ≅ b) : #(i⁻¹)⁻¹ ~~ #i.
118   unfold iso_inv; simpl.
119   reflexivity.
120   Qed.