Theorems · Theorem · group theory
Rep.isZero_Tor_succ_of_projective
∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (X Y : Rep.{u, u, u} k G) [CategoryTheory.Projective Y] (n : ℕ),
CategoryTheory.Limits.IsZero (((Rep.Tor k G (n + 1)).obj X).obj Y)The higher Tor groups for X and Y are zero if Y is projective.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Functorstatement · cited by 16,252
- Groupstatement and proof · cited by 6,238
- ModuleCatstatement · cited by 1,429
- Repstatement and proof · cited by 843
- CategoryTheory.Limits.IsZerostatement · cited by 306
- CategoryTheory.Projectivestatement and proof · cited by 78
- Rep.coinvariantsTensorproof · cited by 13
- Rep.Torstatement · cited by 3
- CategoryTheory.Functor.isZero_leftDerived_obj_projective_succproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- isZero_groupHomology_succ_of_subsingletonproof · cited by 0