Theorems · Definition · group theory
groupCohomology.toCocycles
{k G : Type u} →
[inst : CommRing k] →
[inst_1 : Group G] →
(A : Rep.{u, u, u} k G) → (i j : ℕ) → (groupCohomology.inhomogeneousCochains A).X i ⟶ groupCohomology.cocycles A jThis is the map from i-cochains to j-cocycles induced by the differential in the complex of
inhomogeneous cochains.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- CommRingstatement and proof · cited by 17,173
- Groupstatement and proof · cited by 6,238
- HomologicalComplex.Xstatement · cited by 1,839
- ModuleCatstatement · cited by 1,429
- ComplexShape.upstatement · cited by 1,123
- Repstatement and proof · cited by 843
- groupCohomology.inhomogeneousCochainsstatement and proof · cited by 83
- groupCohomology.cocyclesstatement · cited by 63
- HomologicalComplex.toCyclesproof · cited by 19
Cited by6
Results whose statement or proof uses this declaration.
- groupCohomology.toCocycles_comp_isoCocycles₁_homstatement and proof · cited by 2
- groupCohomology.toCocycles_comp_isoCocycles₂_homstatement and proof · cited by 2
- groupCohomology.toCocycles_comp_isoCocycles₁_hom_applystatement and proof · cited by 0
- groupCohomology.toCocycles_comp_isoCocycles₁_hom_assocstatement and proof · cited by 0
- groupCohomology.toCocycles_comp_isoCocycles₂_hom_applystatement and proof · cited by 0
- groupCohomology.toCocycles_comp_isoCocycles₂_hom_assocstatement and proof · cited by 0