factorThruKernelSubobject — Mathlib

English

The factorThrough map composes to give h from kernelSubobject f: factorThruKernelSubobject f h w ≫ (kernelSubobject f).arrow = h.

Русский

Композиция factorThrough с стрелой ядра восстанавливает исходную стрелу h.

LaTeX

$$$$ factorThruKernelSubobject\\ f\\ h\\ w \\;\\gg\; (kernelSubobject f).arrow = h $$$$

Lean4

/-- A factorisation of `h : W ⟶ X` through `kernelSubobject f`, assuming `h ≫ f = 0`. -/
def factorThruKernelSubobject {W : C} (h : W ⟶ X) (w : h ≫ f = 0) : W ⟶ kernelSubobject f :=
  (kernelSubobject f).factorThru h (kernelSubobject_factors f h w)

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