factorThruImageSubobject — Mathlib

English

There is a canonical factorisation of f through imageSubobject f via factorThruImage f followed by the inverse of imageSubobject f, yielding a morphism X → imageSubobject f.

Русский

Существует каноническое разложение f через imageSubobject f: X → imageSubobject f через factorThruImage f затем обратное imageSubobject f.

LaTeX

$$$\mathrm{factorThruImageSubobject} f = \mathrm{factorThruImage} f \;\circ \; (\mathrm{imageSubobject} f)^{-1}$$$

Lean4

/-- A factorisation of `f : X ⟶ Y` through `imageSubobject f`. -/
def factorThruImageSubobject : X ⟶ imageSubobject f :=
  factorThruImage f ≫ (imageSubobjectIso f).inv

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