isIso_homologyFunctor_map_of_epi_of_isIso_of_mono

English

If φ: S1 → S2 satisfies epi on τ1, iso on τ2, and mono on τ3, then the induced map on the homology functor is an isomorphism.

Русский

Если φ: S1 → S2 удовлетворяет условиям: эпиморфизм на τ1, изоморфизм на τ2 и моно на τ3, то отображение на гомологии функтором является изоморфизмом.

LaTeX

$$$\text{epi}(\tau_1) \land \text{IsIso}(\tau_2) \land \text{Mono}(\tau_3) \Rightarrow \mathrm{IsIso}\big( (\mathrm{homologyFunctor}(C)).map(\phi) \big)$$$

Lean4

instance isIso_homologyFunctor_map_of_epi_of_isIso_of_mono (φ : S₁ ⟶ S₂) [CategoryWithHomology C] [Epi φ.τ₁]
    [IsIso φ.τ₂] [Mono φ.τ₃] : IsIso ((homologyFunctor C).map φ) :=
  (inferInstance : IsIso (homologyMap φ))

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