hasRightHomology_of_epi_of_isIso_of_mono'

English

If S2 has right homology and φ: S1 ⟶ S2 is epi on τ1, iso on τ2, and mono on τ3, then S1 has right homology.

Русский

Если S2 имеет правую гомологию и φ: S1 ⟶ S2 имеет эпиморфизм на τ1, изоморфизм на τ2 и мономорфизм на τ3, то S1 имеет правую гомологию.

LaTeX

$$$\\text{HasRightHomology}(S_1)$$$

Lean4

theorem hasRightHomology_of_epi_of_isIso_of_mono' (φ : S₁ ⟶ S₂) [HasRightHomology S₂] [Epi φ.τ₁] [IsIso φ.τ₂]
    [Mono φ.τ₃] : HasRightHomology S₁ :=
  HasRightHomology.mk' (RightHomologyData.ofEpiOfIsIsoOfMono' φ S₂.rightHomologyData)

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