English
The nth group cohomology is isomorphic to Ext^n in the derived category: groupCohomologyIsoExt A n secures the isomorphism of the two constructions.
Русский
n-я когомология группы изоморфна Ext^n в производной категории: groupCohomologyIsoExt задаёт этот изоморфизм.
LaTeX
$$$$ groupCohomology A n \\cong (\\mathrm{Ext}\\ k(\\mathrm{Rep} kG) n).obj A. $$$$
Lean4
/-- The `n`th group cohomology of a `k`-linear `G`-representation `A` is isomorphic to
`Extⁿ(k, A)` (taken in `Rep k G`), where `k` is a trivial `k`-linear `G`-representation. -/
def groupCohomologyIsoExt [Group G] [DecidableEq G] (A : Rep k G) (n : ℕ) :
groupCohomology A n ≅ ((Ext k (Rep k G) n).obj (Opposite.op <| Rep.trivial k G k)).obj A :=
isoOfQuasiIsoAt (HomotopyEquiv.ofIso (inhomogeneousCochainsIso A)).hom n ≪≫ (Rep.barResolution.extIso k G A n).symm
