unop — Mathlib

English

If S is a short exact sequence, then the unop version S.unop is also short exact.

Русский

Если S — краткая точная последовательность, то ее развернутая версия S.unop также точна.

LaTeX

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

Lean4

theorem unop {S : ShortComplex Cᵒᵖ} (h : S.ShortExact) : S.unop.ShortExact
    where
  exact := h.exact.unop
  mono_f := by
    have := h.epi_g
    dsimp
    infer_instance
  epi_g := by
    have := h.mono_f
    dsimp
    infer_instance

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