hasImage_iso_comp — Mathlib

English

For f,f' with HasImage, if h: f = f', then image.eqToHom h is an isomorphism.

Русский

Для f,f' с образами, если h: f = f', то image.eqToHom h является изоморфизмом.

LaTeX

$$$ \\mathrm{IsIso}(\\mathrm{image}.\\mathrm{eqToHom}(h)) $$$

Lean4

instance hasImage_iso_comp [IsIso f] [HasImage g] : HasImage (f ≫ g) :=
  HasImage.mk
    { F := (Image.monoFactorisation g).isoComp f
      isImage :=
        { lift := fun F' => image.lift (F'.ofIsoComp f)
          lift_fac := fun F' => by
            dsimp
            have : (MonoFactorisation.ofIsoComp f F').m = F'.m := rfl
            rw [← this, image.lift_fac (MonoFactorisation.ofIsoComp f F')] } }

Похожие утверждения