hasImageMapOfIsIso — Mathlib

English

For arrows f,g with Image, F,G : ImageMap sq, F.map = G.map.

Русский

Для стрелок f,g с образами, при F,G : ImageMap sq, сопоставления карт одинаковы: F.map = G.map.

LaTeX

$$$ F.map = G.map $$$

Lean4

instance (priority := 100) hasImageMapOfIsIso {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f ⟶ g)
    [IsIso sq] : HasImageMap sq :=
  HasImageMap.mk
    { map := image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq))
      map_ι := by
        erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m, image.lift_fac,
          Category.assoc, ← Comma.comp_right, IsIso.hom_inv_id, Comma.id_right, Category.comp_id] }

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