factorThru — Mathlib

English

There is a canonical X ⟶ P given P and a factorization h via P; i.e., factorThrough returns a map X ⟶ P.

Русский

Существует канонический морфизм X ⟶ P, задаваемый через P и факторизацию h (через P).

LaTeX

$$$P \\mapsto \\mathrm{factorThru}(X,Y,P,f,h) : X \\to P$$$

Lean4

/-- `P.factorThru f h` provides a factorisation of `f : X ⟶ Y` through some `P : Subobject Y`,
given the evidence `h : P.Factors f` that such a factorisation exists. -/
def factorThru {X Y : C} (P : Subobject Y) (f : X ⟶ Y) (h : Factors P f) : X ⟶ P :=
  Classical.choose ((factors_iff _ _).mp h)

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