English
Given a square sq: f ⟶ g with F a MonoFactorisation of f.hom, and F' of g.hom, along with a map and a commuting condition, one gets a HasImageMap sq.
Русский
Для квадрата sq: f ⟶ g с MonoFactorisation F для f.hom и F' для g.hom и условиях совместимости, существет HasImageMap sq.
LaTeX
$$$ \\text{transport}(sq, F, F', map, map\\_ι) : HasImageMap\, sq $$$
Lean4
/-- `image.preComp f g` is an isomorphism when `f` is an isomorphism
(we need `C` to have equalizers to prove this).
-/
instance isIso_precomp_iso (f : X ⟶ Y) [IsIso f] [HasImage g] : IsIso (image.preComp f g) :=
⟨⟨image.lift
{ I := image (f ≫ g)
m := image.ι (f ≫ g)
e := inv f ≫ factorThruImage (f ≫ g) },
⟨by
ext
simp [image.preComp], by
ext
simp [image.preComp]⟩⟩⟩
-- Note that in general we don't have the other comparison map you might expect
-- `image f ⟶ image (f ≫ g)`.
