image_eq_image — Mathlib

English

If r: c.Rel i j and r': c.Rel i' j, then the image subobjects of the differentials d i j and d i' j are isomorphic, hence equal after a suitable isomorphism: imageSubobject(d i j) = imageSubobject(d i' j).

Русский

Если r: Rel i j и r': Rel i' j, то образы дифференциалов d i j и d i' j совпадают после применения подходящего изоморфизма: imageSubobject(d i j) = imageSubobject(d i' j).

LaTeX

$$$\\\\text{imageSubobject}(C.d i j) = \\\\text{imageSubobject}(C.d i' j)$$$

Lean4

theorem image_eq_image [HasImages V] [HasEqualizers V] {i i' j : ι} (r : c.Rel i j) (r' : c.Rel i' j) :
    imageSubobject (C.d i j) = imageSubobject (C.d i' j) :=
  by
  rw [← eqToHom_comp_d C r r']
  apply imageSubobject_iso_comp

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