Theorems · Definition · group theory
groupHomology.indIso
{k G : Type u} →
[inst : CommRing k] →
[inst_1 : Group G] →
(S : Subgroup G) →
[DecidableEq G] → (A : Rep.{u, u, u} k ↥S) → (n : ℕ) → groupHomology (Rep.ind S.subtype A) n ≅ groupHomology A nShapiro's lemma: given a subgroup S ≤ G and an S-representation A, we have
Hₙ(G, Ind_S^G(A)) ≅ Hₙ(S, A).
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingGroupDecidableEq
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
- CategoryTheory.Iso.symmproof · cited by 993
- Repstatement and proof · cited by 843
- ComplexShape.downproof · cited by 605
- 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.