English
Let f, g, h: X → Y be morphisms in a category with zero morphisms, each having a cokernel. If w1: f = g and w2: g = h, then the composition of the cokernel isomorphisms equals the cokernel isomorphism corresponding to the transitive equality, i.e. cokernelIsoOfEq w1 ≫ cokernelIsoOfEq w2 = cokernelIsoOfEq (w1.trans w2).
Русский
Пусть f, g, h: X → Y — морфизмы в категории с нулевыми морфизмами, для которых существуют котокernelы. Если w1: f = g и w2: g = h, то композиция котокernel-изоморфизмов равна изоморфизму, соответствующему переходному равенству: cokernelIsoOfEq w1 ≫ cokernelIsoOfEq w2 = cokernelIsoOfEq (w1.trans w2).
LaTeX
$$$\forall {C} [Category C] [HasZeroMorphisms C] {X Y} (f g h : X ⟶ Y) [HasCokernel f] [HasCokernel g] [HasCokernel h] (w_1 : f = g) (w_2 : g = h),\; cokernelIsoOfEq w_1 \circ cokernelIsoOfEq w_2 = cokernelIsoOfEq (w_1.trans w_2)$$$
Lean4
@[simp]
theorem cokernelIsoOfEq_trans {f g h : X ⟶ Y} [HasCokernel f] [HasCokernel g] [HasCokernel h] (w₁ : f = g)
(w₂ : g = h) : cokernelIsoOfEq w₁ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq (w₁.trans w₂) := by cases w₁; cases w₂;
ext; simp [cokernelIsoOfEq]
