cochainsMap_id_f_map_mono — Mathlib

English

The nth group cohomology is isomorphic to the nth homology of Hom(P, A) for any projective resolution P of the trivial G-representation k.

Русский

n-я когомология группы изоморфна n-й гомологии Hom(P,A) для любого проектного разрешения P тривиального представления k.

LaTeX

$$$$ groupCohomology A n \\cong \\mathrm{H}^n(\\mathrm{Hom}(P, A)). $$$$

Lean4

instance cochainsMap_id_f_map_mono {A B : Rep k G} (φ : A ⟶ B) [Mono φ] (i : ℕ) :
    Mono ((cochainsMap (MonoidHom.id G) φ).f i) :=
  cochainsMap_f_map_mono (MonoidHom.id G) φ (fun x => ⟨x, rfl⟩) i

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