feat(category_theory/images): unique image (#3921)

Show that the strong-epi mono factorisation of a morphism is unique.

Author: b-mehta

src/category_theory/limits/shapes/images.lean

@@ -541,4 +541,26 @@ instance has_image_maps_of_has_strong_epi_images [has_strong_epi_images C] :
 
 end has_strong_epi_images
 
+variables [has_strong_epi_mono_factorisations.{v} C]
+variables {X Y : C} {f : X ⟶ Y}
+
+/--
+If `C` has strong epi mono factorisations, then the image is unique up to isomorphism, in that if
+`f` factors as a strong epi followed by a mono, this factorisation is essentially the image
+factorisation.
+-/
+def image.iso_strong_epi_mono {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [strong_epi e] [mono m] :
+  I' ≅ image f :=
+is_image.iso_ext {strong_epi_mono_factorisation . I := I', m := m, e := e}.to_mono_is_image (image.is_image f)
+
+@[simp]
+lemma image.iso_strong_epi_mono_hom_comp_ι {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [strong_epi e] [mono m] :
+  (image.iso_strong_epi_mono e m comm).hom ≫ image.ι f = m :=
+is_image.lift_fac _ _
+
+@[simp]
+lemma image.iso_strong_epi_mono_inv_comp_mono {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [strong_epi e] [mono m] :
+  (image.iso_strong_epi_mono e m comm).inv ≫ m = image.ι f :=
+image.lift_fac _
+
 end category_theory.limits