shortExact_iff_unop

Mathlib.Algebra.Homology.ShortComplex.ShortExact

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

English

There is a natural equivalence between S.ShortExact and S.unop.ShortExact via unop.

Русский

Существует естественная эквивалентность между S.ShortExact и S.unop.ShortExact через unop.

LaTeX

$$$ShortExact(S) \iff ShortExact(S^{unop})$$$

Lean4

theorem shortExact_iff_unop (S : ShortComplex Cᵒᵖ) : S.ShortExact ↔ S.unop.ShortExact :=
  S.unop.shortExact_iff_op.symm

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

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

Разделы

Аффилиация

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