feat(natural_isomorphism): componentwise isos are isos (#671)

Author: kim-em

src/category_theory/isomorphism.lean

@@ -92,11 +92,16 @@ def inv (f : X ⟶ Y) [is_iso f] := is_iso.inv f
 
 namespace is_iso
 
-@[simp] def hom_inv_id (f : X ⟶ Y) [is_iso f] : f ≫ category_theory.inv f = 𝟙 X :=
+@[simp] lemma hom_inv_id (f : X ⟶ Y) [is_iso f] : f ≫ category_theory.inv f = 𝟙 X :=
 is_iso.hom_inv_id' f
-@[simp] def inv_hom_id (f : X ⟶ Y) [is_iso f] : category_theory.inv f ≫ f = 𝟙 Y :=
+@[simp] lemma inv_hom_id (f : X ⟶ Y) [is_iso f] : category_theory.inv f ≫ f = 𝟙 Y :=
 is_iso.inv_hom_id' f
 
+@[simp] lemma hom_inv_id_assoc {Z} (f : X ⟶ Y) [is_iso f] (g : X ⟶ Z) : f ≫ category_theory.inv f ≫ g = g :=
+by rw [←category.assoc, hom_inv_id, category.id_comp]
+@[simp] lemma inv_hom_id_assoc {Z} (f : X ⟶ Y) [is_iso f] (g : Y ⟶ Z) : category_theory.inv f ≫ f ≫ g = g :=
+by rw [←category.assoc, inv_hom_id, category.id_comp]
+
 instance (X : C) : is_iso (𝟙 X) :=
 { inv := 𝟙 X }
 

src/category_theory/natural_isomorphism.lean

@@ -71,14 +71,16 @@ begin erw [nat_trans.naturality, ←category.assoc, is_iso.hom_inv_id, category.
   (α.hom.app X) ≫ (G.map f) ≫ (α.inv.app Y) = F.map f :=
 begin erw [nat_trans.naturality, ←category.assoc, is_iso.hom_inv_id, category.id_comp] end
 
+instance is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_iso α :=
+{ inv :=
+  { app := λ X, inv (α.app X),
+    naturality' := λ X Y f,
+    by simpa using congr_arg (λ f, inv (α.app X) ≫ (f ≫ inv (α.app Y))) (α.naturality f).symm } }
+
 def of_components (app : ∀ X : C, (F.obj X) ≅ (G.obj X))
   (naturality : ∀ {X Y : C} (f : X ⟶ Y), (F.map f) ≫ ((app Y).hom) = ((app X).hom) ≫ (G.map f)) :
   F ≅ G :=
-{ hom  := { app := λ X, ((app X).hom), },
-  inv  :=
-  { app := λ X, ((app X).inv),
-    naturality' := λ X Y f,
-    by simpa using congr_arg (λ f, (app X).inv ≫ (f ≫ (app Y).inv)) (naturality f).symm } }
+as_iso { app := λ X, (app X).hom }
 
 @[simp] def of_components.app (app' : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
   app (of_components app' naturality) X = app' X :=