Theorems · Definition · group theory
groupCohomology.H1Iso
{k G : Type u} →
[inst : CommRing k] →
[inst_1 : Group G] →
(A : Rep.{u, u, u} k G) → groupCohomology.H1 A ≅ (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.HThe 1st group cohomology of A, defined as the 1st cohomology of the complex of inhomogeneous
cochains, is isomorphic to cocycles₁ A ⧸ coboundaries₁ A, which is a simpler type.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
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
- CategoryTheory.Iso.transproof · cited by 566
- CategoryTheory.ShortComplex.LeftHomologyData.Hstatement · cited by 236
- HomologicalComplex.scproof · cited by 205
- CategoryTheory.ShortComplex.moduleCatLeftHomologyDatastatement and proof · cited by 106
- CategoryTheory.ShortComplex.leftHomologyDataproof · cited by 83
- groupCohomology.inhomogeneousCochainsproof · cited by 83
Cited by3
Results whose statement or proof uses this declaration.
- groupCohomology.π_comp_H1Iso_homstatement · cited by 2
- groupCohomology.π_comp_H1Iso_hom_applystatement and proof · cited by 0
- groupCohomology.π_comp_H1Iso_hom_assocstatement and proof · cited by 0