exact_iff

Mathlib.Algebra.Homology.ShortComplex.Exact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.QuasiIso.exact_iff

← MathLib Explorer

English

Exactness is invariant under quasi-isomorphisms.

Русский

Точность сохраняется под квази-изоморфизмами.

LaTeX

$$$ S_1.Exact \\iff S_2.Exact \\text{ for quasi-iso } φ $$$

Lean4

theorem exact_iff {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] [QuasiIso φ] :
    S₁.Exact ↔ S₂.Exact := by
  simp only [exact_iff_isZero_homology]
  exact Iso.isZero_iff (asIso (homologyMap φ))

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

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

Разделы

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

Аффилиация

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