English
There is a periodic chain complex in ModuleCat k associated to a finite group G and a representation A, built from A and the norm map and the action of g.
Русский
Существует периодический цепной комплекс в ModuleCat k, связанный с конечной группой G и представлением A, построенный из A, нормы и действия g.
LaTeX
$$$ \text{chainComplex} = \text{HomologicalComplex}(A, \text{norm}, \text{applyAsHom}(A,g)) $$$
Lean4
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the periodic chain complex in `Rep k G` given by
`0 ⟶ A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A --N--> A ⟶ ...` where `N` is the norm map.
Its cohomology is the group cohomology of `A`. -/
noncomputable abbrev moduleCatCochainComplex : CochainComplex (ModuleCat k) ℕ :=
HomologicalComplex.alternatingConst A.V (φ := (applyAsHom A g - 𝟙 A).hom) (ψ := A.norm.hom) (by ext; simp)
(by ext; simp) fun _ _ => ComplexShape.up_nat_odd_add
