feat(category_theory/images): instance for precomposition by iso (#6931)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/limits/shapes/images.lean

@@ -226,6 +226,15 @@ lemma has_image.uniq
   l = image.lift F' :=
 (cancel_mono F'.m).1 (by simp [w])
 
+/-- If `has_image g`, then `has_image (f ≫ g)` when `f` is an isomorphism. -/
+instance {X Y Z : C} (f : X ⟶ Y) [is_iso f] (g : Y ⟶ Z) [has_image g] : has_image (f ≫ g) :=
+{ exists_image := ⟨{
+  F :=
+  { I := image g,
+    m := image.ι g,
+    e := f ≫ factor_thru_image g, },
+  is_image := { lift := λ F', image.lift { I := F'.I, m := F'.m, e := inv f ≫ F'.e, }, }, }⟩ }
+
 end
 
 section
@@ -341,6 +350,11 @@ image.lift
   m := image.ι g,
   e := f ≫ factor_thru_image g }
 
+@[simp, reassoc]
+lemma image.pre_comp_ι [has_image g] [has_image (f ≫ g)] :
+  image.pre_comp f g ≫ image.ι g = image.ι (f ≫ g) :=
+by simp [image.pre_comp]
+
 @[simp, reassoc]
 lemma image.factor_thru_image_pre_comp [has_image g] [has_image (f ≫ g)] :
   factor_thru_image (f ≫ g) ≫ image.pre_comp f g = f ≫ factor_thru_image g :=
@@ -368,12 +382,12 @@ variables [has_equalizers C]
 `image.pre_comp f g` is an isomorphism when `f` is an isomorphism
 (we need `C` to have equalizers to prove this).
 -/
-instance image.is_iso_precomp_iso (f : X ≅ Y) [has_image g] [has_image (f.hom ≫ g)] :
-  is_iso (image.pre_comp f.hom g) :=
+instance image.is_iso_precomp_iso (f : X ⟶ Y) [is_iso f] [has_image g] [has_image (f ≫ g)] :
+  is_iso (image.pre_comp f g) :=
 ⟨⟨image.lift
-  { I := image (f.hom ≫ g),
-    m := image.ι (f.hom ≫ g),
-    e := f.inv ≫ factor_thru_image (f.hom ≫ g) },
+  { I := image (f ≫ g),
+    m := image.ι (f ≫ g),
+    e := inv f ≫ factor_thru_image (f ≫ g) },
   ⟨by { ext, simp [image.pre_comp], }, by { ext, simp [image.pre_comp], }⟩⟩⟩
 
 -- Note that in general we don't have the other comparison map you might expect