mono_of_epi_of_mono_of_mono — Mathlib

English

In Abelian diagrams, certain Mono and Epi conditions propagate through pushouts and pullbacks, leading to Monos in middle arrows under exactness hypotheses.

Русский

В абелиевых диаграммах некоторые условия моно и эпиморфизм распространяются через пушоуты и пуллбаки, приводя моно в середине при условии точности.

LaTeX

$$$\\\\forall φ: R_1 \\to R_2, \\\\text{Exact}(R_1) , \\\\text{Exact}(R_2) \\\\Rightarrow \\\\mathrm{Mono}(app' φ 2) $$$

Lean4

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

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