epi_of_mono_of_epi_of_mono — Mathlib

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).

Русский

Пусть существуют точность и моно-условие, аналогично предыдущему; выводим эпиморфизм для φ 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₂.Exact) (hR₂' : Mono (R₂.map' 0 1)) (h₀ : Epi (app' φ 1))
    (h₁ : Mono (app' φ 2)) : Epi (app' φ 0) :=
  epi_of_mono_of_epi_of_mono' φ hR₁ (by simpa only [map'_comp R₂ 0 1 2] using hR₂.toIsComplex.zero 0) hR₂' h₀ h₁

Похожие утверждения