English
Let k be a commutative ring, G a group, and A a G-representation over k. For each natural number n, there is a functor F_n from the category of G-representations to the category of k-modules given by F_n(A) = H^n(G, A), and F_n acts on morphisms φ: A → B by sending φ to the induced map H^n(G, A) → H^n(G, B). In particular, H^n(G, -) is functorial in A.
Русский
Пусть k — коммутативное кольцо, G — группа, A — представление G над k. Для каждого n существует фактorizованный через F_n ∶ Rep(k, G) → Mod_k такой, что F_n(A) = H^n(G, A) и для любого моноидного морфизма φ: A → B получаем индуцированное отображение H^n(G, A) → H^n(G, B). Это означает, что когомологии группы зависят функториально от представления.
LaTeX
$$$F_n:\mathrm{Rep}(k,G)\to \mathrm{Mod}_k\quad\text{defined by}\quad F_n(A)=H^n(G,A),\; F_n(\varphi)=H^n(G,\varphi).$$$
Lean4
/-- The functor sending a `G`-representation `A` to `Hⁿ(G, A)`. -/
@[simps]
noncomputable def functor (n : ℕ) : Rep k G ⥤ ModuleCat k
where
obj A := groupCohomology A n
map φ := map (MonoidHom.id _) φ n
map_id _ := HomologicalComplex.homologyMap_id _ _
map_comp _
_ := by
simp only [← HomologicalComplex.homologyMap_comp]
rfl
