strongEpi_of_strongEpiMonoFactorisation

English

If there is a single strong epi-mono factorisation F of f and F' is an image factorisation of f, then the epi part of F' is strong epi.

Русский

Если существует единственная сильная эпиморфно-моногруппация F для f и F' является факторизацией образа f, то эпиморфная часть F' сильная epi.

LaTeX

$$$\text{StrongEpi}(F'.e)$$$

Lean4

/-- If there is a single strong epi-mono factorisation of `f`, then every image factorisation is a
strong epi-mono factorisation. -/
theorem strongEpi_of_strongEpiMonoFactorisation {X Y : C} {f : X ⟶ Y} (F : StrongEpiMonoFactorisation f)
    {F' : MonoFactorisation f} (hF' : IsImage F') : StrongEpi F'.e :=
  by
  rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']
  apply strongEpi_comp

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