Theorems · Theorem · group theory
groupHomology.map_chainsFunctor_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 (groupHomology.chainsFunctor k G)).ShortExact- Cited by
- 8 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.
Cites32
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
- CategoryTheory.ShortComplexstatement and proof · cited by 1,850
- ModuleCatstatement and proof · cited by 1,429
- 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
- ComplexShape.downstatement and proof · cited by 605
- ChainComplexstatement · cited by 350
- ModuleCat.Hom.homproof · cited by 341
Cited by11
Results whose statement or proof uses this declaration.
- groupHomology.δproof · cited by 7
- groupHomology.δ_applyproof · cited by 2
- groupHomology.mapShortComplex₁proof · cited by 1
- groupHomology.mapShortComplex₃proof · cited by 1
- groupHomology.map_chainsFunctor_eval_shortExactproof · cited by 1
- groupHomology.mono_δ_of_isZeroproof · cited by 0
- groupHomology.epi_δ_of_isZeroproof · cited by 0
- groupHomology.isIso_δ_of_isZeroproof · cited by 0
- groupHomology.mapShortComplex₁_exactproof · cited by 0
- groupHomology.mapShortComplex₂_exactproof · cited by 0
- groupHomology.mapShortComplex₃_exactproof · cited by 0