hasHomology_of_epi_of_isIso_of_mono'

English

If φ: S1 → S2 with epi, iso, mono conditions and S2 has Homology, then S1 has Homology.

Русский

Если φ: S1 → S2 удовлетворяет условиям epi/iso/mono и у S2 есть гомология, тогда у S1 есть гомология.

LaTeX

$$$HasHomology(S_1)$$$

Lean4

theorem hasHomology_of_epi_of_isIso_of_mono' (φ : S₁ ⟶ S₂) [HasHomology S₂] [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :
    HasHomology S₁ :=
  HasHomology.mk' (HomologyData.ofEpiOfIsIsoOfMono' φ S₂.homologyData)

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