truncLE'_d_eq_toCycles — Mathlib

English

In the boundary-noted case, the differential equals the conjugated differential composed with toCycles maps and their inverses.

Русский

В случае на границе д разности дифференциал равен сопряженной разности через карты toCycles и их обратные.

LaTeX

$$$(K.truncLE' e).d i j = (K.truncLE'XIso e hi' (e.not_boundaryLE_prev hij)).hom \circ K.toCycles i' j' \circ (K.truncLE'XIso e hj' hj).inv$$$

Lean4

theorem truncLE'_d_eq_toCycles {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.toCycles i' j' ≫ (K.truncLE'XIsoCycles e hj' hj).inv :=
  Quiver.Hom.op_inj
    (by
      simpa [truncLE', truncLE'XIso, truncLE'XIsoCycles] using
        K.op.truncGE'_d_eq_fromOpcycles e.op hij hj' hi' (by simpa))

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