English
Let R1, R2 form an exact diagram with the indicated mono and epi conditions; then the middle morphism is mono.
Русский
Пусть R1 и R2 образуют точную схему с указанными условиями моно/эпиморфизмов; тогда средняя стрелка моно.
LaTeX
$$$R_1.Exact \land \mathrm{Mono}(R_2.map' 0 1) \land \mathrm{Mono}(app'\,\varphi\,0) \land \mathrm{Mono}(app'\,\varphi\,2) \Rightarrow \mathrm{Mono}(app'\,\varphi\,1)$$$
Lean4
theorem mono_of_mono_of_mono_of_mono (hR₁ : R₁.Exact) (hR₂' : Mono (R₂.map' 0 1)) (h₀ : Mono (app' φ 0))
(h₁ : Mono (app' φ 2)) : Mono (app' φ 1) :=
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
mono_of_epi_of_mono_of_mono' ψ (by simp) (hR₁.exact 0).exact_toComposableArrows (exact₂_mk _ (by simp) ?_)
(by dsimp [ψ]; infer_instance) h₀ h₁
rw [ShortComplex.exact_iff_mono _ (by simp)]
exact hR₂'
