English
If f is an isomorphism, then image.preComp f g is an isomorphism (assuming HasEqualizers).
Русский
Если f изоморфизм, то image.preComp f g является изоморфизмом (при условии существования равнозначных пределов).
LaTeX
$$$ \\text{IsIso}(\\mathrm{image.preComp}(f,g)) $$$
Lean4
instance hasImage_comp_iso [HasImage f] [IsIso g] : HasImage (f ≫ g) :=
HasImage.mk
{ F := (Image.monoFactorisation f).compMono g
isImage :=
{ lift := fun F' => image.lift F'.ofCompIso
lift_fac := fun F' =>
by
rw [← Category.comp_id (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m), ← IsIso.inv_hom_id g, ←
Category.assoc]
refine congrArg (· ≫ g) ?_
have :
(image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g =
image.lift (MonoFactorisation.ofCompIso F') ≫ ((MonoFactorisation.ofCompIso F').m) :=
by simp only [MonoFactorisation.ofCompIso_I, Category.assoc, MonoFactorisation.ofCompIso_m]
rw [this, image.lift_fac (MonoFactorisation.ofCompIso F'), image.as_ι] } }
