isIso_homologyMap'_of_epi_of_isIso_of_mono

English

Let φ: S1 → S2 be a morphism of short complexes. If φ satisfies epi on τ1, isomorphism on τ2, and mono on τ3, then the induced homology map' φ h1 h2 is an isomorphism.

Русский

Пусть φ: S1 → S2 — морфизм короткого комплекса. Если φ удовлетворяет условию: эпиморфизм на τ1, изоморфизм на τ2 и моно на τ3, то индуцированное отображение гомологии homologyMap' φ h1 h2 — изоморфизм.

LaTeX

$$$\operatorname{epi}(\tau_1) \land \operatorname{IsIso}(\tau_2) \land \operatorname{Mono}(\tau_3) \Rightarrow \mathrm{IsIso}(\mathrm{homologyMap}'(\phi,h_1,h_2))$$$

Lean4

instance isIso_homologyMap'_of_epi_of_isIso_of_mono (φ : S₁ ⟶ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData)
    [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : IsIso (homologyMap' φ h₁ h₂) :=
  by
  dsimp only [homologyMap']
  infer_instance

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