Theorems · Definition · group theory

groupCohomology.coindIso

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {S : Subgroup G} →
        (A : Rep.{u, u, u} k ↥S) →
          (n : ℕ) → groupCohomology (Rep.coind.{u, u, u, u} S.subtype A) n ≅ groupCohomology A n

Shapiro's lemma: given a subgroup S ≤ G and an S-representation A, we have Hⁿ(G, Coind_S^G(A)) ≅ Hⁿ(S, A).

Defined in: Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
Cited by: 0 results in Mathlib
Foundations: Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Group

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Groupstatement and proof · cited by 6,238
CategoryTheory.Isostatement · cited by 3,963
Subgroupstatement and proof · cited by 3,593
ModuleCatstatement and proof · cited by 1,429
ComplexShape.upproof · cited by 1,123
CategoryTheory.Iso.symmproof · cited by 993
Repstatement and proof · cited by 843
CategoryTheory.Iso.transproof · cited by 566
CategoryTheory.Functor.mapIsoproof · cited by 224
Subgroup.subtypestatement and proof · cited by 185
HomologicalComplex.homologyFunctorproof · cited by 70

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.