Commit 2025-12-20 08:12 6e8b5904

feat(RepresentationTheory/Homological/GroupCohomology): cohomology of finite cyclic groups (#32898) Let k be a commutative ring, G a group and A a k-linear G-representation. Given endomorphisms φ, ψ : A ⟶ A such that φ ∘ ψ = ψ ∘ φ = 0. Denote by Chains(A, φ, ψ) the periodic chain complex ... ⟶ A --φ--> A --ψ--> A --φ--> A --ψ--> A ⟶ 0 and by Cochains(A, φ, ψ) the periodic cochain complex 0 ⟶ A --ψ--> A --φ--> A --ψ--> A --φ--> A ⟶ .... When G is finite and generated by g : G, then P := Chains(k[G], N, ρ(g) - Id) (with ρ the left regular representation) is a projective resolution of k as a trivial representation. In this PR we show that for A : Rep k G, Hom(P, A) is isomorphic to Cochains(A, N, ρ_A(g) - Id) as a complex of k-modules, and hence the cohomology of this complex computes group cohomology.