monoFactorisation — Mathlib

English

For any morphism f: G ⟶ H in ModuleCat, one can factor f as m ∘ e with m the mono image inclusion and e the canonical map to image f.

Русский

Для любой стрелки f: G ⟶ H в ModuleCat существует факторизация f = m ∘ e, где m — включение образа и e — каноническое отображение к образу.

LaTeX

$$$f = m \\circ e \\quad\\text{with } m = \\mathrm{image.ι}_f,\\; e = \\mathrm{factorThruImage}(f)$$$

Lean4

/-- The factorisation of any morphism in `ModuleCat R` through a mono. -/
def monoFactorisation : MonoFactorisation f where
  I := image f
  m := image.ι f
  e := factorThruImage f

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