Mathlib Map

Theorems · Definition · group theory

Rep.torIso

{k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        {B : Rep.{u, u, u} k G} →
          (P : CategoryTheory.ProjectiveResolution B) →
            (n : ℕ) →
              ((Rep.Tor k G n).obj A).obj B ≅
                HomologicalComplex.homology (HomologicalComplex.coinvariantsTensorObj A P.complex) n

Tor can be computed using a projective resolution.

Defined in
Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Cited by
0 results in Mathlib
Foundations
Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

groupHomologyIsoTor · cited by 1groupHomologyIsoTorgroupHomologyIso · cited by 0groupHomologyIsoCategoryTheory.Functor.obj · cited by 19642Functor.objCommRing · cited by 17173CommRingCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorGroup · cited by 6238GroupCategoryTheory.Iso · cited by 3963CategoryTheory.IsoModuleCat · cited by 1429ModuleCatRep · cited by 843RepComplexShape.down · cited by 605ComplexShape.downHomologicalComplex.homology · cited by 209HomologicalComplex.homolo…HomologicalComplex.sc · cited by 205HomologicalComplex.scCategoryTheory.ProjectiveResolution · cited by 92CategoryTheory.Projective…CategoryTheory.ProjectiveResolution.complex · cited by 82ProjectiveResolution.comp…Rep.coinvariantsTensor · cited by 13Rep.coinvariantsTensorCategoryTheory.ProjectiveResolution.isoLeftDerivedObj · cited by 8ProjectiveResolution.isoL…HomologicalComplex.coinvariantsTensorObj · cited by 3HomologicalComplex.coinva…Rep.torIsoCITED BYCITES

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.