map_cochainsFunctor_shortExact — Mathlib

English

The cochain functor sends a short exact sequence of representations to a short exact sequence of cochains, preserving exactness degreewise.

Русский

Коочейн-функтор отправляет короткую точную последовательность представлений в короткую точную последовательность коочеинов, сохраняя точность на каждом уровне.

LaTeX

$$$\\text{map\_cochainsFunctor\_shortExact}$ preserves short exactness degreewise.$$

Lean4

theorem map_cochainsFunctor_shortExact : ShortExact (X.map (cochainsFunctor k G)) :=
  HomologicalComplex.shortExact_of_degreewise_shortExact _ fun i =>
    { exact :=
        by
        have : LinearMap.range X.f.hom.hom = LinearMap.ker X.g.hom.hom :=
          (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker
        simp [moduleCat_exact_iff_range_eq_ker, LinearMap.range_compLeft, LinearMap.ker_compLeft, this]
      mono_f :=
        letI := hX.mono_f;
        cochainsMap_id_f_map_mono X.f i
      epi_g :=
        letI := hX.epi_g;
        cochainsMap_id_f_map_epi X.g i }

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