of_iso

Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.ExactAt.of_iso

← MathLib Explorer

English

If K is exact at i and K ≅ L, then L is exact at i.

Русский

Если K точна в i и K эквивалентен L, то L точна в i.

LaTeX

$$$$ K.ExactAt(i) \implies L.ExactAt(i) $$$$

Lean4

theorem of_iso (hK : K.ExactAt i) {L : HomologicalComplex C c} (e : K ≅ L) : L.ExactAt i :=
  by
  rw [exactAt_iff] at hK ⊢
  exact ShortComplex.exact_of_iso ((shortComplexFunctor C c i).mapIso e) hK

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

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

Разделы

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

Аффилиация

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