Theorems · Definition · group theory
groupCohomology.iCocycles
{k G : Type u} →
[inst : CommRing k] →
[inst_1 : Group G] →
(A : Rep.{u, u, u} k G) → (n : ℕ) → groupCohomology.cocycles A n ⟶ (groupCohomology.inhomogeneousCochains A).X nThe natural inclusion of the n-cocycles Zⁿ(G, A) into the n-cochains Cⁿ(G, A).
- Cited by
- 27 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
- HomologicalComplex.iCyclesproof · cited by 80
- groupCohomology.cocyclesstatement · cited by 63
Cited by27
Results whose statement or proof uses this declaration.
- groupCohomology.cocyclesIso₀_hom_comp_fstatement · cited by 6
- groupCohomology.isoCocycles₁_hom_comp_istatement · cited by 5
- groupCohomology.isoCocycles₂_hom_comp_istatement · cited by 5
- groupCohomology.map_H0Iso_hom_fproof · cited by 3
- groupCohomology.π_comp_H0IsoOfIsTrivial_homstatement and proof · cited by 2
- groupCohomology.isoCocycles₁_inv_comp_iCocyclesstatement · cited by 2
- groupCohomology.cocyclesIso₀_hom_comp_f_assocstatement and proof · cited by 2
- groupCohomology.cocyclesIso₀_inv_comp_iCocyclesstatement and proof · cited by 2
- groupCohomology.isoCocycles₂_inv_comp_iCocyclesstatement · cited by 2
- groupCohomology.cocyclesMap_cocyclesIso₀_hom_fproof · cited by 2
- groupCohomology.cocyclesMk₁_eqproof · cited by 2
- groupCohomology.isoCocycles₁_hom_comp_i_assocstatement and proof · cited by 1