d_comp_diagonalSuccIsoFree_inv_eq

English

The differential commutes with diagonalSuccIsoFree in the sense that d commutes with the inverse of the diagonalSuccIsoFree isomorphism.

Русский

Дифференциал коммутирует с диагональным переходом через диагональный переход, сопряжённый с обратной диагональной изоморфией.

LaTeX

$$$d\\;\\circ\\; (\\mathrm{diagonalSuccIsoFree})^{-1} = (\\mathrm{diagonalSuccIsoFree})^{-1} \\circ (\\text{standardComplex}.d)$$$

Lean4

theorem d_comp_diagonalSuccIsoFree_inv_eq :
    d k G n ≫ (diagonalSuccIsoFree k G n).inv =
      (diagonalSuccIsoFree k G (n + 1)).inv ≫ (standardComplex k G).d (n + 1) n :=
  free_ext _ _ fun i => by
    simpa [diagonalSuccIsoFree_inv_hom_single_single (k := k), d_single (k := k), standardComplex.d_eq,
      standardComplex.d_of (k := k) (Fin.partialProd i), Fin.sum_univ_succ, Fin.partialProd_contractNth] using
      congr(single $(by ext j; exact (Fin.partialProd_succ' i j).symm) 1)

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