English
If f: X → Y is mono, then the forward morphism of the image-mono-source iso composed with f equals the image inclusion: imageMonoIsoSource(f).hom ≫ f = image.ι f.
Русский
Пусть f: X → Y моно. Тогда композиция образ-моноисточника по направлению с f равна включению образа: imageMonoIsoSource(f).hom ≫ f = image.ι f.
LaTeX
$$$ (\\mathrm{imageMonoIsoSource}(f)).\\mathrm{hom} \\circ f = \\mathrm{image}.\\iota(f) $$$
Lean4
@[reassoc (attr := simp)]
theorem imageMonoIsoSource_hom_self [Mono f] : (imageMonoIsoSource f).hom ≫ f = image.ι f :=
by
simp only [← imageMonoIsoSource_inv_ι f]
rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]
-- This is the proof that `factorThruImage f` is an epimorphism
-- from https://en.wikipedia.org/wiki/Image_%28category_theory%29, which is in turn taken from:
-- Mitchell, Barry (1965), Theory of categories, MR 0202787, p.12, Proposition 10.1
