explicitCokernelDesc_comp_eq_zero

English

Let X, Y, Z, W be objects in the category of Sem Normed Groups and f: X → Y, g: Y → Z, h: Z → W be morphisms such that f ∘ g = 0 and g ∘ h = 0. Then the explicit cokernel descent along cond, followed by h, is zero.

Русский

Пусть X, Y, Z, W — объекты в категориальном контексте SemiNormedGrp, и f: X → Y, g: Y → Z, h: Z → W таковы, что f ∘ g = 0 и g ∘ h = 0. Тогда явное cokernelDesc(cond), далее через h, равен нулю.

LaTeX

$$$ explicitCokernelDesc(cond) \circ h = 0 $$$

Lean4

theorem explicitCokernelDesc_comp_eq_zero {X Y Z W : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W}
    (cond : f ≫ g = 0) (cond2 : g ≫ h = 0) : explicitCokernelDesc cond ≫ h = 0 :=
  by
  rw [← cancel_epi (explicitCokernelπ f), ← Category.assoc, explicitCokernelπ_desc]
  simp [cond2]

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