English
For a Rel i j in c, the differential (K.truncLE' e).d i j equals the conjugated differential through the XIso components when j is at a boundary position with hi', hj'.
Русский
Для отношения Rel i j в c производная (K.truncLE' e).d i j равна сопряженной производной через компоненты XIso, когда j в границе и заданы hi', hj'.
LaTeX
$$$(K.truncLE' e).d i j = (K.truncLE'XIso e hi' (e.not_boundaryLE_prev hij)).hom \circ K.d i' j' \circ (K.truncLE'XIso e hj' hj).inv$$$
Lean4
theorem truncLE'_d_eq {i j : ι} (hij : c.Rel i j) {i' j' : ι'} (hi' : e.f i = i') (hj' : e.f j = j')
(hj : ¬e.BoundaryLE j) :
(K.truncLE' e).d i j =
(K.truncLE'XIso e hi' (e.not_boundaryLE_prev hij)).hom ≫ K.d i' j' ≫ (K.truncLE'XIso e hj' hj).inv :=
Quiver.Hom.op_inj (by simpa using K.op.truncGE'_d_eq e.op hij hj' hi' (by simpa))
