unop

Mathlib.Algebra.Homology.ShortComplex.Exact

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.Exact.unop

English

If a Short Complex S is exact, then its unop (opposite of the opposite) is exact.

Русский

Если кратчайший комплекс S точен, то S.unop точен.

LaTeX

$$$ S.Exact \\Rightarrow S.unop.Exact $$$

Lean4

theorem unop {S : ShortComplex Cᵒᵖ} (h : S.Exact) : S.unop.Exact :=
  by
  obtain ⟨h, z⟩ := h
  exact ⟨⟨h.unop, (IsZero.of_iso z h.iso.symm).unop⟩⟩

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

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

Разделы

Аффилиация

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