mono_τ₂_of_exact_of_mono — Mathlib

English

If S₁ → S₂ is exact and φ.τ₁, φ.τ₃ are mono, then φ.τ₂ is mono.

Русский

Пусть отображение φ между короткими комплексами образует точное отображение; если φ.τ₁ и φ.τ₃ моно, то φ.τ₂ тоже моно.

LaTeX

$$Mono(φ.τ₂)$$

Lean4

theorem mono_τ₂_of_exact_of_mono {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.Exact) [Mono S₁.f] [Mono S₂.f]
    [Mono φ.τ₁] [Mono φ.τ₃] : Mono φ.τ₂ := by
  rw [mono_iff_cancel_zero]
  intro A x₂ hx₂
  obtain ⟨x₁, hx₁⟩ : ∃ x₁, x₁ ≫ S₁.f = x₂ :=
    ⟨_, h₁.lift_f x₂ (by simp only [← cancel_mono φ.τ₃, assoc, zero_comp, ← φ.comm₂₃, reassoc_of% hx₂])⟩
  suffices x₁ = 0 by rw [← hx₁, this, zero_comp]
  simp only [← cancel_mono φ.τ₁, ← cancel_mono S₂.f, assoc, φ.comm₁₂, zero_comp, reassoc_of% hx₁, hx₂]

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