map_chainsFunctor_shortExact — Mathlib

English

If X is a short exact sequence of representations, then applying the chains functor at each G-action preserves a short exact sequence in homology; i.e., the induced long exact sequence in group homology remains exact after applying the chains functor.

Русский

Если X — короткая точная последовательность представлений, то применение функции цепей с учётом действия группы G сохраняет короткую точную последовательность в гомологии; то есть полученная длинная точная последовательность по групповой гомологии сохраняется после применения цепей.

LaTeX

$$$(X.ShortExact) \Rightarrow (X.map(\mathrm{groupHomology}.\mathrm{chainsFunctor} \, k \, G)).ShortExact$$$

Lean4

theorem map_chainsFunctor_shortExact : ShortExact (X.map (chainsFunctor k G)) :=
  letI := hX.mono_f
  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, ker_mapRange,
          range_mapRange_linearMap X.f.hom.hom (LinearMap.ker_eq_bot.2 <| (ModuleCat.mono_iff_injective _).1 _), this]
      mono_f := chainsMap_id_f_map_mono X.f i
      epi_g :=
        letI := hX.epi_g;
        chainsMap_id_f_map_epi X.g i }

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