exact

Mathlib.Algebra.Homology.ShortComplex.Exact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.Splitting.exact

← MathLib Explorer

English

A short complex equipped with a splitting is exact.

Русский

Короткий комплекс, снабжённый расщеплением, является точным.

LaTeX

$$S\text{Splitting} \Rightarrow S\text{Exact}$$

Lean4

/-- A short complex equipped with a splitting is exact. -/
theorem exact [HasZeroObject C] (s : S.Splitting) : S.Exact :=
  ⟨s.homologyData, isZero_zero _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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