imageSubobject_arrow_comp_eq_zero

English

If f ≫ g = 0 in a category with HasZeroMorphisms, and there is epi on factorThruImageSubobject f, then (imageSubobject f).arrow ≫ g = 0.

Русский

Если gh = 0 и существует эпиморфизм factorThruImageSubobject f, то (imageSubobject f).arrow ∘ g = 0.

LaTeX

$$$[HasZeroMorphisms\ C] \Rightarrow [Epi(\mathrm{factorThruImageSubobject} f)] \Rightarrow (\mathrm{imageSubobject} f).\mathrm{arrow} \circ g = 0 \text{ when } f \circ g = 0$$$

Lean4

theorem imageSubobject_arrow_comp_eq_zero [HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage f]
    [Epi (factorThruImageSubobject f)] (h : f ≫ g = 0) : (imageSubobject f).arrow ≫ g = 0 :=
  zero_of_epi_comp (factorThruImageSubobject f) <| by simp [h]

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