mono_of_epi_of_epi_of_mono — Mathlib

English

Let hR1 : R1.Exact, hR2 : R2.Exact, hR1' : Epi (R1.map' 1 2), h0 : Epi (app' φ 0), h1 : Mono (app' φ 1). Then Mono (app' φ 2).

Русский

Пусть R1 и R2 образуют точную структуру и существуют эпиморфизмы на соответствующих стрелках, затем моно на последнем компоненте φ.

LaTeX

$$$R_1.Exact \land R_2.Exact \land \mathrm{Epi}(R_1.map'\ 1\ 2) \land \mathrm{Epi}(app'\,\varphi\,0) \land \mathrm{Mono}(app'\,\varphi\,1) \Rightarrow \mathrm{Mono}(app'\,\varphi\,2)$$$

Lean4

theorem mono_of_epi_of_epi_of_mono (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (hR₁' : Epi (R₁.map' 1 2)) (h₀ : Epi (app' φ 0))
    (h₁ : Mono (app' φ 1)) : Mono (app' φ 2) :=
  mono_of_epi_of_epi_mono' φ (by simpa only [map'_comp R₁ 0 1 2] using hR₁.toIsComplex.zero 0) hR₁' hR₂ h₀ h₁

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