English
Given a subgroup S ≤ G and a k(S)-representation A, there is a natural isomorphism of complexes between coinvariants of the restricted resolution and the induced representation, i.e., coinvariantsTensorResProjectiveResolutionIso.
Русский
Для подгруппы S ≤ G и k-представления A на S существует естественный изоморфизм комплексoв между тензорной коинвариантами ограниченного резолюционного комплекса и индуцированным представлением.
LaTeX
$$$\\text{coinvariantsTensorObj } A \\; ((Action.res _ S).mapProjectiveResolution P) \\cong \\; P^{\\text{coinvariantsTensorObj}} (\\mathrm{ind}\n S.\\mathrm{subtype} A).$$$
Lean4
/-- Given a projective resolution `P` of `k` as a `k`-linear `G`-representation, a subgroup
`S ≤ G`, and a `k`-linear `S`-representation `A`, this is an isomorphism of complexes
`(A ⊗ Res(S)(P))_S ≅ (Ind_S^G(A) ⊗ P)_G`. -/
noncomputable abbrev coinvariantsTensorResProjectiveResolutionIso (P : ProjectiveResolution (Rep.trivial k G k)) :
((Action.res _ S.subtype).mapProjectiveResolution P).complex.coinvariantsTensorObj A ≅
P.complex.coinvariantsTensorObj (ind S.subtype A) :=
(NatIso.mapHomologicalComplex (coinvariantsTensorIndNatIso S.subtype A).symm _).app _
