Theorems · Theorem · group theory
groupCohomology.map_cochainsFunctor_shortExact
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)},
X.ShortExact → (X.map (groupCohomology.cochainsFunctor k G)).ShortExact- Cited by
- 9 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
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
- Set.univproof · cited by 3,945
- CategoryTheory.ShortComplexstatement and proof · cited by 1,850
- ModuleCatstatement and proof · cited by 1,429
- ComplexShape.upstatement and proof · cited by 1,123
- CochainComplexstatement · cited by 1,016
- LinearMap.rangeproof · cited by 893
- LinearMap.kerproof · cited by 848
- Repstatement and proof · cited by 843
- CategoryTheory.ShortComplex.gproof · cited by 658
- CategoryTheory.ShortComplex.fproof · cited by 653
Cited by12
Results whose statement or proof uses this declaration.
- groupCohomology.δproof · cited by 8
- groupCohomology.δ_applyproof · cited by 2
- groupCohomology.mapShortComplex₁proof · cited by 1
- groupCohomology.mapShortComplex₃proof · cited by 1
- groupCohomology.map_cochainsFunctor_eval_shortExactproof · cited by 1
- groupCohomology.epi_δ_of_isZeroproof · cited by 0
- groupCohomology.mapShortComplex₁_exactproof · cited by 0
- groupCohomology.mapShortComplex₂_exactproof · cited by 0
- groupCohomology.isIso_δ_of_isZeroproof · cited by 0
- groupCohomology.mapShortComplex₃_exactproof · cited by 0
- groupCohomology.mono_δ_of_isZeroproof · cited by 0
- groupCohomology.δ_naturalityproof · cited by 0