mono_of_mono_f — Mathlib

English

If a chain map φ has each component φ.f i mono, then φ is mono.

Русский

Если у цепного отображателя φ каждое компонентное отображение φ.f i моно, тогда φ является моно.

LaTeX

$$$\\\\forall {K L} \\\\; (\\\\phi : K \\\\longrightarrow L), \\\\; (\\\\forall i, Mono(\\\\phi.f i)) \\\\Rightarrow Mono\\\\phi$$$

Lean4

theorem mono_of_mono_f {K L : HomologicalComplex V c} (φ : K ⟶ L) (hφ : ∀ i, Mono (φ.f i)) : Mono φ where
  right_cancellation g h
    eq := by
    ext i
    rw [← cancel_mono (φ.f i)]
    exact congr_hom eq i

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