epi_τ₂_of_exact_of_epi — Mathlib

English

If S₁ → S₂ is given with S₁.g, S₂.g epi, and φ.τ₁, φ.τ₃ epi, then φ.τ₂ is epi.

Русский

Если S₁ → S₂ имеет эпиморфизмg на обеих сторонах и φ.τ₁, φ.τ₃ эпиморфны, тогда φ.τ₂ эпиморфен.

LaTeX

$$Epi(φ.τ₂)$$

Lean4

theorem epi_τ₂_of_exact_of_epi {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₂ : S₂.Exact) [Epi S₁.g] [Epi S₂.g] [Epi φ.τ₁]
    [Epi φ.τ₃] : Epi φ.τ₂ := by
  have : Mono S₁.op.f := by dsimp; infer_instance
  have : Mono S₂.op.f := by dsimp; infer_instance
  have : Mono (opMap φ).τ₁ := by dsimp; infer_instance
  have : Mono (opMap φ).τ₃ := by dsimp; infer_instance
  have := mono_τ₂_of_exact_of_mono (opMap φ) h₂.op
  exact unop_epi_of_mono (opMap φ).τ₂

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