exact_iff_of_iso

Mathlib.Algebra.Homology.ExactSequence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ComposableArrows.exact_iff_of_iso

English

Let e: S1 ≅ S2 be an isomorphism. Then S1.Exact ↔ S2.Exact.

Русский

Пусть e: S1 ≅ S2 — изоморфизм. Тогда S1.Exact эквивално S2.Exact.

LaTeX

$$$S_1 \cong S_2 \Rightarrow (S_1^{{\mathrm{Exact}}} \iff S_2^{{\mathrm{Exact}}})$$$

Lean4

theorem exact_iff_of_iso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) : S₁.Exact ↔ S₂.Exact :=
  ⟨exact_of_iso e, exact_of_iso e.symm⟩

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

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

Разделы

Аффилиация

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