functor — Mathlib

English

The functor groups homology Hn with action by f, associating to each A the module Hn(A) and to each morphism φ the induced map on homology Hn(φ).

Русский

Функтор сопоставляет гомологии Hn действие по f, переходя от A к модулю Hn(A) и отображение φ к индуцированному отображению на гомологии Hn(φ).

LaTeX

$$$ \text{functor}(n): \mathrm{Rep}\;k\;G \;\to\; \mathrm{ModuleCat}\;k $$$

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 := groupHomology A n
  map {A B} φ := map (MonoidHom.id _) φ n
  map_id A := by simp [map, groupHomology]
  map_comp f
    g := by
    simp only [← HomologicalComplex.homologyMap_comp, ← chainsMap_comp]
    rfl

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