factorThru_add_sub_factorThru_left

English

In a balanced category, a morphism f:X→Y is epi if and only if the subobject generated by f is the top subobject of Y.

Русский

В сбалансированной категории морфизм f является эпиморфизмом тогда и только тогда, когда подпредмет, порожденный f, равен верхнему подпредмету Y.

LaTeX

$$$\text{Epi } f \iff \operatorname{Subobject}.mk f = \top$$$

Lean4

@[simp]
theorem factorThru_add_sub_factorThru_left {X Y : C} {P : Subobject Y} (f g : X ⟶ Y) (w : P.Factors (f + g))
    (wf : P.Factors f) :
    P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g (factors_right_of_factors_add f g w wf) :=
  by
  ext
  simp

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