English
If two image factorizations F and F' of f are given with an isomorphism isoExt hF hF' between them, then the Hom component of isoExt relates m and m' by F'.m = (isoExt hF hF').inv ≫ F.m.
Русский
Пусть два факторизации изображения F и F' факторизуют f; изоморфизм isoExt hF hF' связывает m и m' таким образом, что F'.m = (isoExt hF hF').inv ≫ F.m.
LaTeX
$$$(\mathrm{isoExt}(hF,hF')).\mathrm{hom} \;\; \; \; \; \; \; \; \; \; \; = \; F'.m \circ (\mathrm{isoExt}(hF,hF')).^{-1}.$$$
Lean4
/-- The morphism `m` in a factorisation `f = e ≫ m` through a monomorphism is uniquely
determined. -/
@[ext (iff := false)]
theorem ext {F F' : MonoFactorisation f} (hI : F.I = F'.I) (hm : F.m = eqToHom hI ≫ F'.m) : F = F' :=
by
obtain ⟨_, Fm, _, Ffac⟩ := F; obtain ⟨_, Fm', _, Ffac'⟩ := F'
cases hI
replace hm : Fm = Fm' := by simpa using hm
congr
apply (cancel_mono Fm).1
rw [Ffac, hm, Ffac']
