Theorems · Definition · group theory
inhomogeneousCochains.d
{k G : Type u} →
[inst : CommRing k] →
[inst_1 : Monoid G] →
(A : Rep.{u_1, u, u} k G) → (n : ℕ) → ModuleCat.of k ((Fin n → G) → ↑A) ⟶ ModuleCat.of k ((Fin (n + 1) → G) → ↑A)The differential in the complex of inhomogeneous cochains used to calculate group cohomology.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homstatement · cited by 32,603
- CommRingstatement and proof · cited by 17,173
- Finset.sumproof · cited by 5,195
- Monoidstatement and proof · cited by 3,887
- Finset.univproof · cited by 3,473
- ModuleCatstatement · cited by 1,429
- Repstatement and proof · cited by 843
- Rep.Vstatement and proof · cited by 695
- ModuleCat.ofstatement · cited by 594
- Rep.ρproof · cited by 356
- ModuleCat.ofHomproof · cited by 200
Cited by19
Results whose statement or proof uses this declaration.
- groupCohomology.inhomogeneousCochainsproof · cited by 83
- groupCohomology.comp_d₀₁_eqproof · cited by 6
- groupCohomology.cocyclesMkstatement and proof · cited by 6
- groupCohomology.toCocycles_comp_isoCocycles₁_homproof · cited by 2
- groupCohomology.toCocycles_comp_isoCocycles₂_homproof · cited by 2
- inhomogeneousCochains.d_hom_applystatement and proof · cited by 1
- groupCohomology.iCocycles_mkstatement and proof · cited by 1
- groupCohomology.inhomogeneousCochains.d_defstatement and proof · cited by 0
- groupCohomology.cocyclesMk.congr_simpstatement and proof · cited by 0
- inhomogeneousCochains.d_eqstatement · cited by 0
- Rep.tateNorm_comp_dproof · cited by 0
- groupCohomology.eq_d₀₁_comp_inv_applystatement and proof · cited by 0