English
Let hR1 : R1.Exact, hR2 : R2.Exact, hR2' : Mono (R2.map' 0 1), h0 : Epi (app' φ 1), h1 : Mono (app' φ 2). Then Epi (app' φ 0).
Русский
Пусть существует точная структура для R1 и R2, и R2.map' 0 1 моно, а также эпиморфизм на φ 1 и моно на φ 2; тогда φ 0 является эпиморфизмом.
LaTeX
$$$R_1.Exact \land R_2.Exact \land \mathrm{Mono}(R_2.map' 0 1) \land \mathrm{Epi}(app'\,\varphi\,1) \land \mathrm{Mono}(app'\,\varphi\,2) \Rightarrow \mathrm{Epi}(app'\,\varphi\,0)$$$
Lean4
theorem epi_of_mono_of_epi_of_mono' (hR₁ : R₁.Exact) (hR₂ : R₂.map' 0 2 = 0) (hR₂' : Mono (R₂.map' 0 1))
(h₀ : Epi (app' φ 1)) (h₁ : Mono (app' φ 2)) : Epi (app' φ 0) :=
by
let ψ : mk₃ (0 : R₁.obj' 0 ⟶ _) (R₁.map' 0 1) (R₁.map' 1 2) ⟶ mk₃ (0 : R₁.obj' 0 ⟶ _) (R₂.map' 0 1) (R₂.map' 1 2) :=
homMk₃ (𝟙 _) (app' φ 0) (app' φ 1) (app' φ 2) (by simp) (naturality' φ 0 1) (naturality' φ 1 2)
refine
epi_of_epi_of_epi_of_mono' ψ (hR₁.exact 0).exact_toComposableArrows (exact₂_mk _ (by simp) ?_) ?_
(by dsimp [ψ]; infer_instance) h₀ h₁
· rw [ShortComplex.exact_iff_mono _ (by simp)]
exact hR₂'
· dsimp
rw [← Functor.map_comp]
exact hR₂
