d_eq — Mathlib

English

The differential in the inhomogeneous cochains equals the conjugation of barComplex's differential by freeLiftLEquiv and the toModuleIso map.

Русский

Дифференциал в несобиратьных косинфках равен сопряжению дифференциала barComplex через freeLiftLEquiv и карту toModuleIso.

LaTeX

$$$ d_A(n) = (\mathrm{freeLiftLEquiv}(\mathrm{Fin}\ n\to G) A)^{-1} \; \circ \; ((\mathrm{barComplex} k G).linearYonedaObj k A).d\; n\,(n+1) \; \circ \; (\mathrm{freeLiftLEquiv}(\mathrm{Fin}(n+1)\to G) A).toModuleIso.hom $$$

Lean4

theorem d_eq :
    d A n =
      (freeLiftLEquiv (Fin n → G) A).toModuleIso.inv ≫
        ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫ (freeLiftLEquiv (Fin (n + 1) → G) A).toModuleIso.hom :=
  by
  ext
  simp [d_hom_apply, map_add, barComplex.d_single (k := k)]

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