English
For a morphism g: A → B in the opposite category, the op of the image inclusion from g.unop composed with imageUnopOp g equals the canonical factor-through image morphism.
Русский
Для морфизма g: A → B в противоположной категории, противоположность инъекции образа g.unop, композиция с imageUnopOp g равна каноническому морфизму через образ.
LaTeX
$$$ (\operatorname{imageUnopOp} \, g)^{\mathrm{hom}} \circ \operatorname{image} \iota\, g = \operatorname{factorThruImage}(g^{\mathrm{unop}})^{op} $$$
Lean4
theorem image_ι_op_comp_imageUnopOp_hom : (image.ι g.unop).op ≫ (imageUnopOp g).hom = factorThruImage g :=
by
simp only [imageUnopOp, Iso.trans, Iso.symm, Iso.op, cokernelOpOp_inv, cokernelEpiComp_hom, cokernelCompIsIso_hom,
Abelian.coimageIsoImage'_hom, ← Category.assoc, ← op_comp]
simp only [Category.assoc, Abelian.imageIsoImage_hom_comp_image_ι, kernel.lift_ι, Quiver.Hom.op_unop,
cokernelIsoOfEq_hom_comp_desc_assoc, cokernel.π_desc_assoc, cokernel.π_desc]
simp only [eqToHom_refl]
rw [IsIso.inv_id, Category.id_comp]
