d_comp_d

Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

URI: https://scilib.ai/kg/mathlib#groupHomology.inhomogeneousChains.d_comp_d

English

The differential squares to zero: d_{n+1} ∘ d_{n} = 0 for the inhomogeneous chain complex.

Русский

Квадрат дифференциала обнуляется: d_{n+1} ∘ d_{n} = 0 для цепного комплекса с неоднородными цепями.

LaTeX

$$$d_A(n+1) \circ d_A(n) = 0$$$

Lean4

theorem d_comp_d : d A (n + 1) ≫ d A n = 0 := by
  simpa [ChainComplex.of] using ((inhomogeneousChains A).d_comp_d (n + 2) (n + 1) n)

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

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

Разделы

Аффилиация

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