OAI/Algebra/Finitistic/Ordinary/OrdinaryMiddleTensorFunctors.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.middleLeftFunctor line 14

   Source documentation

   Tensor by the fixed middle bimodule, retaining its actual left action.

   def middleLeftFunctor : ModuleCat.{u} B ⥤ ModuleCat.{u} A where
   …

2. instance OAI.LittleFinitistic.middleLeftFunctor_additive line 32
3. def OAI.LittleFinitistic.middleRightFunctor line 42

   Source documentation

   Tensor a right module by the middle bimodule, retaining its actual right action.

   def middleRightFunctor : ModuleCat.{u} Aᵐᵒᵖ ⥤ ModuleCat.{u} Bᵐᵒᵖ where
   …

4. instance OAI.LittleFinitistic.middleRightFunctor_additive line 60
5. def OAI.LittleFinitistic.middleRightComplex line 71

   Source documentation

   The genuine right tensor complex, with its right B-action.

   def middleRightComplex (Q : CochainComplex (ModuleCat.{u} Aᵐᵒᵖ) ℤ) :
       CochainComplex (ModuleCat.{u} Bᵐᵒᵖ) ℤ :=
   …

6. def OAI.LittleFinitistic.middleLeftComplex line 76

   Source documentation

   The genuine left tensor complex, with its left A-action.

   def middleLeftComplex (Z : CochainComplex (ModuleCat.{u} B) ℤ) :
       CochainComplex (ModuleCat.{u} A) ℤ :=
   …