δ₀

Mathlib.Algebra.Homology.ExactSequence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.Exact.δ₀

English

If S is a ComposableArrows C (n+2) and S.Exact holds, then S.δ₀.Exact holds.

Русский

Если S — композиционные стрелки C (n+2) и S.Exact, тогда S.δ₀.Exact.

LaTeX

$$$S \text{ in } \mathrm{ComposableArrows}(C, n+2) \text{ and } S.\mathrm{Exact} \Rightarrow S.\delta_0.\mathrm{Exact}$$$

Lean4

theorem δ₀ {S : ComposableArrows C (n + 2)} (hS : S.Exact) : S.δ₀.Exact :=
  by
  rw [exact_iff_δ₀] at hS
  exact hS.2

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

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

Разделы

Аффилиация

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