chainsMap_f_map_mono — Mathlib

English

If f is surjective, and φ is epi, then each i-th chain map component is epi.

Русский

Если f сюрьективен и φ эпиморфизм, то i-й компонент цепной карты эпиморфизм.

LaTeX

$$∀ i, Epi ((chainsMap f φ).f i)$$

Lean4

theorem chainsMap_f_map_mono (hf : Function.Injective f) [Mono φ] (i : ℕ) : Mono ((chainsMap f φ).f i) := by
  simpa [ModuleCat.mono_iff_injective] using
    (mapRange_injective φ.hom (map_zero _) <| (Rep.mono_iff_injective φ).1 inferInstance).comp
      (mapDomain_injective hf.comp_left)

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