shortComplex_exact

Mathlib.CategoryTheory.Sites.MayerVietorisSquare

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact

English

The Mayer–Vietoris short complex is exact: S.shortComplex.Exact.

Русский

Короткий комплекс MV точен: S.shortComplex.Exact.

LaTeX

$$S.shortComplex.Exact$$

Lean4

theorem shortComplex_exact : S.shortComplex.Exact :=
  ShortComplex.exact_of_g_is_cokernel _ S.isPushoutAddCommGrpFreeSheaf.isColimitCokernelCofork

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

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

Разделы

Аффилиация

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