cochainsMap_f_map_mono — Mathlib

English

There is an instance stating that for a given φ: A ⟶ B with Mono φ, the i-th component of cochainsMap with identity on G is mono.

Русский

Существует инстанс, утверждающий, что для данного φ: A ⟶ B с Mono φ, i-я компонента cochainsMap с тождественным действием на G моно.

LaTeX

$$$$ \\text{cochainsMap}_{\\mathrm{Id}_G} φ \\text{ is mono for all i}. $$$$

Lean4

theorem cochainsMap_f_map_mono (hf : Function.Surjective f) [Mono φ] (i : ℕ) : Mono ((cochainsMap f φ).f i) := by
  simpa [ModuleCat.mono_iff_injective] using
    ((Rep.mono_iff_injective φ).1 inferInstance).comp_left.comp <|
      LinearMap.funLeft_injective_of_surjective k A _ hf.comp_left

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