English
Under exactness assumptions and epi conditions, the middle component 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₁.map' 1 2)) (h₀ : Epi (app' φ 0))
(h₁ : Epi (app' φ 2)) : Epi (app' φ 1) :=
by
let ψ : mk₃ (R₁.map' 0 1) (R₁.map' 1 2) (0 : _ ⟶ R₁.obj' 0) ⟶ mk₃ (R₂.map' 0 1) (R₂.map' 1 2) (0 : _ ⟶ R₁.obj' 0) :=
homMk₃ (app' φ 0) (app' φ 1) (app' φ 2) (𝟙 _) (naturality' φ 0 1) (naturality' φ 1 2) (by simp)
refine
epi_of_epi_of_epi_of_mono' ψ (exact₂_mk _ (by simp) ?_) (hR₂.exact 0).exact_toComposableArrows (by simp) h₀ h₁
(by dsimp [ψ]; infer_instance)
rw [ShortComplex.exact_iff_epi _ (by simp)]
exact hR₁'
