epi_of_epi_f — Mathlib

English

If φ.f i is epi for every i, then φ is epi.

Русский

Если каждый φ.f i эпиморфен, то φ эпиморфен.

LaTeX

$$$\\\\forall {K L} \\\\; (\\\\phi : K \\\\longrightarrow L), \\\\; (\\\\forall i, Epi(\\\\phi.f i)) \\\\Rightarrow Epi\\\\phi$$$

Lean4

theorem epi_of_epi_f {K L : HomologicalComplex V c} (φ : K ⟶ L) (hφ : ∀ i, Epi (φ.f i)) : Epi φ where
  left_cancellation g h
    eq := by
    ext i
    rw [← cancel_epi (φ.f i)]
    exact congr_hom eq i

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