Theorems · Definition · group theory
groupCohomology.cocyclesMk
{k G : Type u} →
[inst : CommRing k] →
[inst_1 : Group G] →
{A : Rep.{u, u, u} k G} →
{n : ℕ} →
(f : (Fin n → G) → ↑A) →
(CategoryTheory.ConcreteCategory.hom (inhomogeneousCochains.d A n)) f = 0 → ↑(groupCohomology.cocycles A n)Make an n-cocycle out of an element of the kernel of the nth differential.
- 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.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- RingHom.idstatement · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- LinearMapstatement · cited by 10,215
- Groupstatement and proof · cited by 6,238
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- ModuleCatstatement · cited by 1,429
- ModuleCat.carrierstatement · cited by 997
- Repstatement and proof · cited by 843
- Rep.Vstatement and proof · cited by 695
- ModuleCat.ofstatement · cited by 594
- groupCohomology.inhomogeneousCochainsproof · cited by 83
Cited by7
Results whose statement or proof uses this declaration.
- groupCohomology.δ_applystatement · cited by 2
- groupCohomology.cocyclesMkOfCompEqDproof · cited by 2
- groupCohomology.cocyclesMk₁_eqstatement and proof · cited by 2
- groupCohomology.cocyclesMk₀_eqstatement and proof · cited by 1
- groupCohomology.cocyclesMk₂_eqstatement and proof · cited by 1
- groupCohomology.iCocycles_mkstatement · cited by 1
- groupCohomology.cocyclesMk.congr_simpstatement and proof · cited by 0