1 Generalizable All Variables.
2 Require Import Notations.
3 Require Import Categories_ch1_3.
4 Require Import Functors_ch1_4.
6 (******************************************************************************)
7 (* Chapter 1.5: Isomorphisms *)
8 (******************************************************************************)
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
14 (* TO DO: show isos are unique when they exist *)
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 *)
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.
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 ].
39 Notation "f '⁻¹'" := (@iso_inv _ _ _ _ _ f) : isomorphism_scope.
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.
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) ];
55 Notation "a >>≅>> b" := (iso_comp a b).
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)
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.
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.
73 setoid_rewrite <- associativity.
74 setoid_rewrite iso_comp1.
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.
82 setoid_rewrite <- associativity.
83 setoid_rewrite iso_comp1.
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.
91 setoid_rewrite associativity.
92 setoid_rewrite iso_comp1.
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⁻¹.
100 setoid_rewrite associativity.
101 setoid_rewrite iso_comp1.
103 apply right_identity.
106 Lemma isos_forward_equal_then_backward_equal `{C:Category}{a}{b}(i1 i2:a ≅ b) : #i1 ~~ #i2 -> #i1⁻¹ ~~ #i2⁻¹.
108 setoid_rewrite <- left_identity at 1.
109 setoid_rewrite <- (iso_comp2 i2).
110 setoid_rewrite associativity.
112 setoid_rewrite iso_comp1.
113 setoid_rewrite right_identity.
117 Lemma iso_inv_inv `{C:Category}{a}{b}(i:a ≅ b) : #(i⁻¹)⁻¹ ~~ #i.
118 unfold iso_inv; simpl.
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.
125 setoid_rewrite <- associativity.
126 setoid_rewrite iso_comp2.
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.
132 setoid_rewrite associativity.
133 setoid_rewrite iso_comp2.
134 apply right_identity.
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.
139 setoid_rewrite <- associativity.
140 setoid_rewrite iso_comp1.
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.
146 setoid_rewrite associativity.
147 setoid_rewrite iso_comp1.
148 apply right_identity.