cochainsFunctor — Mathlib

English

The cochains functorial construction assigns to each G-representation its cochain complex of modules over k.

Русский

Коконструкции коцепан присваивают каждому G-представлению его когомологический комплекс модулей над k.

LaTeX

$$$\text{cochainsFunctor}: \Rep(k,G) \to \mathrm{CochainComplex}(\ModuleCat(k))\;\mathbb{N}$$$

Lean4

/-- The functor sending a representation to its complex of inhomogeneous cochains. -/
@[simps]
noncomputable def cochainsFunctor : Rep k G ⥤ CochainComplex (ModuleCat k) ℕ
    where
  obj A := inhomogeneousCochains A
  map f := cochainsMap (MonoidHom.id _) f
  map_id _ := cochainsMap_id
  map_comp φ ψ := cochainsMap_comp (MonoidHom.id G) (MonoidHom.id G) φ ψ

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