complex_d_comp_π_f_zero

Mathlib.CategoryTheory.Preadditive.Projective.Resolution

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero

English

The composition d 1 0 followed by π.f 0 is zero in a projective resolution.

Русский

Составление d(1,0) затем π.f(0) равно нулю в проективном разрешении.

LaTeX

$$$ P.complex.d\\;1\\;0 \\;\\circ\\; P.\\pi.f\\;0 = 0. $$$

Lean4

@[reassoc (attr := simp)]
theorem complex_d_comp_π_f_zero : P.complex.d 1 0 ≫ P.π.f 0 = 0 := by rw [← P.π.comm 1 0, single_obj_d, comp_zero]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru