epi_homologyMap_of_epi_cyclesMap'

English

If cyclesMap φ is epi, then homologyMap φ is epi.

Русский

Если cyclesMap φ эпиморфизм, то homologyMap φ эпиморфизм.

LaTeX

$$Epi (homologyMap φ)$$

Lean4

theorem epi_homologyMap_of_epi_cyclesMap' [S₁.HasHomology] [S₂.HasHomology] (h : Epi (cyclesMap φ)) :
    Epi (homologyMap φ) :=
  by
  have : Epi (S₁.homologyπ ≫ homologyMap φ) := by
    rw [homologyπ_naturality φ]
    apply epi_comp
  exact epi_of_epi S₁.homologyπ (homologyMap φ)

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