isIso₂_of_shortExact_of_isIso₁₃

English

If two short exact sequences S1 and S2 are connected by a morphism φ whose τ1 and τ3 components are isomorphisms, then φ.τ₂ is an isomorphism.

Русский

Если две кратко точные последовательности S1 и S2 связаны морфизмом φ, причём компоненты φ.τ₁ и φ.τ₃ являются изоморфизмами, то φ.τ₂ тоже изоморфизм.

LaTeX

$$$ShortExact(S_1) \to ShortExact(S_2) \Rightarrow (IsIso(\varphi.τ_2))$$$

Lean4

theorem isIso₂_of_shortExact_of_isIso₁₃ [Balanced C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.ShortExact)
    (h₂ : S₂.ShortExact) [IsIso φ.τ₁] [IsIso φ.τ₃] : IsIso φ.τ₂ :=
  by
  have := h₁.mono_f
  have := h₂.mono_f
  have := h₁.epi_g
  have := h₂.epi_g
  have := mono_τ₂_of_exact_of_mono φ h₁.exact
  have := epi_τ₂_of_exact_of_epi φ h₂.exact
  apply isIso_of_mono_of_epi

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