isIso_map' — Mathlib

English

In a balanced preadditive category, if a short exact sequence S is exact and two adjacent maps vanish, then the middle map S.map'(k+1, k+2) is an isomorphism.

Русский

В сбалансированной прeддобавительной категории, если последовательность S точна и два соседних отображения обнуляются, то середины отображение S.map'(k+1, k+2) изоморфик.

LaTeX

$$$S.Exact \wedge S.map'(k, k+1)=0 \wedge S.map'(k+2, k+3)=0 \Rightarrow IsIso\bigl(S.map'(k+1, k+2)\bigr)$$$

Lean4

theorem isIso_map' {C : Type*} [Category C] [Preadditive C] [Balanced C] {n : ℕ} {S : ComposableArrows C n}
    (hS : S.Exact) (k : ℕ) (hk : k + 3 ≤ n) (h₀ : S.map' k (k + 1) = 0) (h₁ : S.map' (k + 2) (k + 3) = 0) :
    IsIso (S.map' (k + 1) (k + 2)) := by
  have := (hS.exact k).mono_g h₀
  have := (hS.exact (k + 1)).epi_f h₁
  apply isIso_of_mono_of_epi

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