Tor

📁 Source: Mathlib/CategoryTheory/Monoidal/Tor.lean

Statistics

Metric	Count
Definitions Tor, Tor', Tor	3
Theorems Tor'_map_app, Tor'_obj_map, Tor'_obj_obj, Tor_map, Tor_obj, isZero_Tor'_succ_of_projective, isZero_Tor_succ_of_projective	7
Total	10

CategoryTheory

Definitions

Name	Category	Theorems
Tor 📖	CompOp	3 math math: Tor_obj, isZero_Tor_succ_of_projective, Tor_map
Tor' 📖	CompOp	4 math math: Tor'_obj_obj, isZero_Tor'_succ_of_projective, Tor'_obj_map, Tor'_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Tor'_map_app 📖	mathematical	—	NatTrans.app Functor.obj Functor Functor.category Functor.leftDerived MonoidalCategory.tensoringRight NatTrans.leftDerived Functor.map Tor'	—	Abelian.hasZeroObject
Tor'_obj_map 📖	mathematical	—	Functor.map Functor.obj Functor Functor.category Tor' NatTrans.app Functor.leftDerived MonoidalCategory.tensoringRight NatTrans.leftDerived	—	Abelian.hasZeroObject
Tor'_obj_obj 📖	mathematical	—	Functor.obj Functor Functor.category Tor' Functor.leftDerived MonoidalCategory.tensoringRight	—	Abelian.hasZeroObject
Tor_map 📖	mathematical	—	Functor.map Functor Functor.category Tor NatTrans.leftDerived Functor.obj MonoidalCategory.tensoringLeft	—	Abelian.hasZeroObject
Tor_obj 📖	mathematical	—	Functor.obj Functor Functor.category Tor Functor.leftDerived MonoidalCategory.tensoringLeft	—	Abelian.hasZeroObject
isZero_Tor'_succ_of_projective 📖	mathematical	—	Limits.IsZero Functor.obj Functor Functor.category Tor'	—	Abelian.hasZeroObject Functor.isZero_leftDerived_obj_projective_succ
isZero_Tor_succ_of_projective 📖	mathematical	—	Limits.IsZero Functor.obj Functor Functor.category Tor	—	Abelian.hasZeroObject Functor.isZero_leftDerived_obj_projective_succ

Rep

Definitions

Name	Category	Theorems
Tor 📖	CompOp	3 math math: Tor_map, isZero_Tor_succ_of_projective, Tor_obj

---

← Back to Index