epi_of_mono_of_epi_of_mono — Mathlib

English

From exactness and mono conditions on the outer arrows, the middle arrow is mono.

Русский

Из точности и условий моно на внешних стрелках следует, что средняя стрелка моно.

LaTeX

$$$R_1.Exact \land \mathrm{Mono}(R_2.f) \land \mathrm{Mono}(\varphi.\tau_1) \land \mathrm{Mono}(\varphi.\tau_3) \Rightarrow \mathrm{Mono}(\varphi.\tau_2)$$$

Lean4

theorem epi_of_mono_of_epi_of_mono (hR₁ : R₁.Exact) (hR₂' : Mono R₂.f) (h₀ : Epi φ.τ₂) (h₁ : Mono φ.τ₃) : Epi φ.τ₁ :=
  Abelian.epi_of_mono_of_epi_of_mono' (ShortComplex.mapToComposableArrows φ) hR₁.exact_toComposableArrows (by simp) hR₂'
    h₀ h₁

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