Theorems · Definition · group theory

groupHomology.H0IsoOfIsTrivial

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → [A.IsTrivial] → groupHomology.H0 A ≅ ModuleCat.of k ↑A

When the representation on A is trivial, then H₀(G, A) is all of A.

Defined in: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
Cited by: 5 results in Mathlib
Foundations: Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Group Rep.IsTrivial

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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
ModuleCatstatement · cited by 1,429
CategoryTheory.Iso.symmproof · cited by 993
Repstatement and proof · cited by 843
Rep.Vstatement · cited by 695
ModuleCat.ofstatement · cited by 594
CategoryTheory.Iso.transproof · cited by 566
groupHomology.inhomogeneousChainsproof · cited by 90
Rep.IsTrivialstatement and proof · cited by 37
groupHomology.H0statement · cited by 25

Cited by5

Results whose statement or proof uses this declaration.

groupHomology.π_comp_H0IsoOfIsTrivial_homstatement · cited by 2
groupHomology.π_comp_H0IsoOfIsTrivial_hom_applystatement and proof · cited by 0
groupHomology.H0IsoOfIsTrivial.congr_simpstatement and proof · cited by 0
groupHomology.H0IsoOfIsTrivial_inv_eq_πstatement · cited by 0
groupHomology.π_comp_H0IsoOfIsTrivial_hom_assocstatement and proof · cited by 0