English
Let C be a HomologicalComplex in a category V with images and equalizers. For any indices i, j and any relation r that relates i and j (r ∈ c.Rel i j), the image subobject of the j-th forward differential equals the image subobject of the i-to-j differential: imageSubobject (C.dTo j) = imageSubobject (C.d i j).
Русский
Пусть C – гомологический комплекс в категории V, удовлетворяющий существованию образов и равныеравнивания. Для любых i, j, если r относится к i, j, то образ соответствующего прямого дифференциала совпадает: imageSubobject (C.dTo j) = imageSubobject (C.d i j).
LaTeX
$$$\\operatorname{imageSubobject}(C.dTo\,j)=\\operatorname{imageSubobject}(C.d\,i\\,j)$$$
Lean4
theorem image_to_eq_image [HasImages V] [HasEqualizers V] {i j : ι} (r : c.Rel i j) :
imageSubobject (C.dTo j) = imageSubobject (C.d i j) :=
by
rw [C.dTo_eq r]
apply imageSubobject_iso_comp
