ofComplex_d_1_0 — Mathlib

English

In an abelian category with enough projectives, the differential at position (1,0) in the projective resolution of Z coincides with the differential induced by the canonical projection π Z.

Русский

В абелевой категории с достаточным числом проективных объектов разностный морфизм в позиции (1,0) в проективной резолюции Z совпадает с дифференциалом, индуцированным каноническим проекционным отображением πZ.

LaTeX

$$$(d^{\mathrm{ofComplex}(Z)})_{1,0} = d\\bigl(\\mathrm{Projective}.\\pi Z\\bigr)$$$

Lean4

theorem ofComplex_d_1_0 : (ofComplex Z).d 1 0 = d (Projective.π Z) := by simp [ofComplex]

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