epi_of_epi_of_epi_of_epi — Mathlib

English

If the right-hand piece is exact and the outer maps are epi, the middle map is epi.

Русский

Если правая часть точна и внешние стрелки эпиморфны, средняя стрелка эпиморфна.

LaTeX

$$$R_2.Exact \land \mathrm{Epi}(R_1.map' 1 2) \land \mathrm{Epi}(app'\,\varphi\,0) \land \mathrm{Epi}(app'\,\varphi\,2) \Rightarrow \mathrm{Epi}(app'\,\varphi\,1)$$$

Lean4

theorem epi_of_epi_of_epi_of_epi (hR₂ : R₂.Exact) (hR₁' : Epi R₁.g) (h₀ : Epi φ.τ₁) (h₁ : Epi φ.τ₃) : Epi φ.τ₂ :=
  Abelian.epi_of_epi_of_epi_of_epi (ShortComplex.mapToComposableArrows φ) hR₂.exact_toComposableArrows hR₁' h₀ h₁

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