OAI/Algebra/Finitistic/Bimodule/BimoduleInputFunctor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleTotal.InputTensor line 12
2. def OAI.LittleFinitistic.BimoduleTotal.inputModuleMap line 15
3. def OAI.LittleFinitistic.BimoduleTotal.inputFunctor line 28

   Source documentation

   Tensor by one genuine bimodule, varying the left-module input and retaining the outside action.

   def inputFunctor : ModuleCat.{u} B ⥤ ModuleCat.{u} B where
   …

4. instance OAI.LittleFinitistic.BimoduleTotal.inputFunctor_additive line 52
5. abbrev OAI.LittleFinitistic.BimoduleTotal.columnFunctor line 64
6. instance OAI.LittleFinitistic.BimoduleTotal.columnFunctor_additive line 68