English
In a derived diagram with four positions, if the first and third maps are epi and the last is mono, then the middle epi holds for certain projections.
Русский
В диаграмме из четырех позиций, если первые и третьи стрелки — эпиморфизмы, а последняя — моно, то среди стрелок посредине тоже выполняется эпиморфизм для определенных проекций.
LaTeX
$$$\\\\forall φ: R_1 \\to R_2, \\\\text{R1.Exact}, \\\\text{R2.Exact}, \\\\mathrm{Epi}(app' φ 0), \\\\mathrm{Epi}(app' φ 2), \\\\mathrm{Mono}(app' φ 3) \\\\Rightarrow \\\\mathrm{Epi}(app' φ 1).$$$
Lean4
theorem epi_of_epi_of_epi_of_mono (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (h₀ : Epi (app' φ 0)) (h₂ : Epi (app' φ 2))
(h₃ : Mono (app' φ 3)) : Epi (app' φ 1) :=
epi_of_epi_of_epi_of_mono' φ (hR₁.exact 1).exact_toComposableArrows (hR₂.exact 0).exact_toComposableArrows
(by simpa only [R₂.map'_comp 1 2 3] using hR₂.toIsComplex.zero 1) h₀ h₂ h₃
