noncomputable def TorGroup (R : Type u) [CommRing R] (n : ℕ) (M A : ModuleCat R) : ModuleCat R

noncomputable def TorGroup.functor (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor (ModuleCat R) (ModuleCat R))

noncomputable def torRes (R : Type u) [CommRing R] (M : ModuleCat R) : CategoryTheory.ProjectiveResolution M

@[reducible, inline]

noncomputable abbrev tR (R : Type u) [CommRing R] : CategoryTheory.Functor (ModuleCat R) (CategoryTheory.Functor (ModuleCat R) (ModuleCat R))

noncomputable def torChainSC (R : Type u) [CommRing R] (M : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) : CategoryTheory.ShortComplex (ChainComplex (ModuleCat R) ℕ)

noncomputable def torChainSE (R : Type u) [CommRing R] (M : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) : (torChainSC R M S).ShortExact

noncomputable def torIso (R : Type u) [CommRing R] (M A : ModuleCat R) (n : ℕ) : ((CategoryTheory.Tor' (ModuleCat R) n).obj M).obj A ≅ (HomologicalComplex.homologyFunctor (ModuleCat R) (ComplexShape.down ℕ) n).obj ((((tR R).obj A).mapHomologicalComplex (ComplexShape.down ℕ)).obj (torRes R M).complex)

noncomputable def TorGroup.connectingHom (R : Type u) [CommRing R] (M : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) (n : ℕ) : ((CategoryTheory.Tor' (ModuleCat R) (n + 1)).obj M).obj S.X₃ ⟶ ((CategoryTheory.Tor' (ModuleCat R) n).obj M).obj S.X₁