hasImageMapsOfHasStrongEpiImages — Mathlib

English

If the category has strong epi images, then image maps exist: HasImageMaps C.

Русский

Если категория имеет сильные образы эпиморфий, то существуют отображения образов: HasImageMaps C.

LaTeX

$$$\mathrm{HasImageMaps}(C)$$$

Lean4

/-- A category with strong epi images has image maps. -/
instance (priority := 100) hasImageMapsOfHasStrongEpiImages [HasStrongEpiImages C] : HasImageMaps C where
  has_image_map {f} {g}
    st :=
    HasImageMap.mk
      {
        map :=
          (CommSq.mk
              (show (st.left ≫ factorThruImage g.hom) ≫ image.ι g.hom = factorThruImage f.hom ≫ image.ι f.hom ≫ st.right
                by simp)).lift }

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