English
Let C be an abelian category and R1, R2 be composable arrows in C^2 with φ : R1 ⟶ R2. If R1.map' 0 2 = 0, R1.map' 1 2 is epi, R2 is exact, the induced map app' φ 0 is epi, and app' φ 1 is mono, then app' φ 2 is mono.
Русский
Пусть C — абелева категория, R1, R2 — композиционные стрелы в C^2, и φ : R1 ⟶ R2. Если R1.map' 0 2 = 0, R1.map' 1 2 есть эпиморфизм, R2 точна, а отображения app' φ 0 и app' φ 1 заданы как эпиморфизм и моно соответственно, то app' φ 2 моно.
LaTeX
$$$\bigl(R_1.map' 0 2 = 0\bigr) \land \mathrm{Epi}\bigl(R_1.map' 1 2\bigr) \land R_2.Exact \land \mathrm{Epi}\bigl(app'\,\varphi\,0\bigr) \land \mathrm{Mono}\bigl(app'\,\varphi\,1\bigr) \Rightarrow \mathrm{Mono}\bigl(app'\,\varphi\,2\bigr)$$$
Lean4
theorem mono_of_epi_of_epi_mono' (hR₁ : R₁.map' 0 2 = 0) (hR₁' : Epi (R₁.map' 1 2)) (hR₂ : R₂.Exact)
(h₀ : Epi (app' φ 0)) (h₁ : Mono (app' φ 1)) : Mono (app' φ 2) :=
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
mono_of_epi_of_mono_of_mono' ψ ?_ (exact₂_mk _ (by simp) ?_) (hR₂.exact 0).exact_toComposableArrows h₀ h₁
(by dsimp [ψ]; infer_instance)
· dsimp
rw [← Functor.map_comp]
exact hR₁
· rw [ShortComplex.exact_iff_epi _ (by simp)]
exact hR₁'
