English
Postcomposing by an isomorphism gives an isomorphism between image subobjects: imageSubobject (f ≫ h) ≅ imageSubobject f when h is an isomorphism.
Русский
После композиции с изоморфизмом получается изоморфизм между образами подобъектов: imageSubobject(f ≫ h) ≅ imageSubobject f, если h — изоморфизм.
LaTeX
$$$(\mathrm{imageSubobject}(f \circ h)) \cong (\mathrm{imageSubobject} f)$, when $h$ is an isomorphism$$
Lean4
/-- The morphism `imageSubobject (h ≫ f) ⟶ imageSubobject f`
is an epimorphism when `h` is an epimorphism.
In general this does not imply that `imageSubobject (h ≫ f) = imageSubobject f`,
although it will when the ambient category is abelian.
-/
instance imageSubobject_comp_le_epi_of_epi {X' : C} (h : X' ⟶ X) [Epi h] (f : X ⟶ Y) [HasImage f] [HasImage (h ≫ f)] :
Epi (Subobject.ofLE _ _ (imageSubobject_comp_le h f)) :=
by
rw [ofLE_mk_le_mk_of_comm (image.preComp h f)]
· infer_instance
· simp
