factorThru_eq_zero — Mathlib

English

Let C be a category with zero morphisms. For any subobject P of Y and any morphism f: X → Y that factors through P via h, the induced map P.factorThru f h: X → P is zero if and only if f = 0.

Русский

Пусть C — категория с нулевыми морфизмами. Пусть P ⊆ Y — подпредмет, а f: X → Y факторизуется через P с помощью h. Тогда соответствующее отображение P.factorThru f h: X → P равно нулю тогда и только тогда, когда f = 0.

LaTeX

$$$P\!\text{.factorThru}(f,h) = 0 \iff f = 0$$$

Lean4

@[simp]
theorem factorThru_eq_zero [HasZeroMorphisms C] {X Y : C} {P : Subobject Y} {f : X ⟶ Y} {h : Factors P f} :
    P.factorThru f h = 0 ↔ f = 0 := by
  fconstructor
  · intro w
    replace w := w =≫ P.arrow
    simpa using w
  · rintro rfl
    ext
    simp

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