mono_of_cancel_zero — Mathlib

English

The sum of morphisms commutes with composition on the right: (∑ f_j) ≫ g = ∑ (f_j ≫ g).

Русский

Суммирование морфизмов коммутирует с композицией справа: (∑ f_j) ≫ g = ∑ (f_j ≫ g).

LaTeX

$$$\left(\sum_{j \in s} f_j\right) \circ g = \sum_{j \in s} (f_j \circ g)$$$

Lean4

theorem mono_of_cancel_zero {Q R : C} (f : Q ⟶ R) (h : ∀ {P : C} (g : P ⟶ Q), g ≫ f = 0 → g = 0) : Mono f where
  right_cancellation := fun {Z} g₁ g₂ hg =>
    sub_eq_zero.1 <| h _ <| (map_sub (rightComp Z f) g₁ g₂).trans <| sub_eq_zero.2 hg

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