coindIso — Mathlib

English

If the second argument Y is projective, then higher Tor groups vanish: Tor_{n+1}(X,Y)=0 for all n.

Русский

Если второе аргумент Y проективно, то высшие группы Tor исчезают: Tor_{n+1}(X,Y)=0 для всех n.

LaTeX

$$IsZero( Tor k G (n+1) .obj X .obj Y )$$

Lean4

/-- Shapiro's lemma: given a subgroup `S ≤ G` and an `S`-representation `A`, we have
`Hⁿ(G, Coind_S^G(A)) ≅ Hⁿ(S, A).` -/
noncomputable def coindIso [DecidableEq G] (A : Rep k S) (n : ℕ) :
    groupCohomology (coind S.subtype A) n ≅ groupCohomology A n :=
  (HomologicalComplex.homologyFunctor _ _ _).mapIso
      (inhomogeneousCochainsIso (coind S.subtype A) ≪≫
        (linearYonedaObjResProjectiveResolutionIso (barResolution k G) A).symm) ≪≫
    (groupCohomologyIso A n ((Action.res _ _).mapProjectiveResolution <| barResolution k G)).symm

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