OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleCoefficients.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleCoefficients line 11

   Source documentation

   A genuine tensor-algebra module with both scalar restrictions recorded together.

   def BimoduleCoefficients (k S A : Type u) [Field k] [Ring S] [Ring A] [Algebra k S] [Algebra k A]
       (M : ModuleCat.{u} (S ⊗[k] Aᵐᵒᵖ)) := M
   …

2. instance OAI.LittleFinitistic.BimoduleCoefficients.(instance at line 16) line 16
3. instance OAI.LittleFinitistic.BimoduleCoefficients.(instance at line 17) line 17
4. instance OAI.LittleFinitistic.BimoduleCoefficients.(instance at line 18) line 18
5. instance OAI.LittleFinitistic.BimoduleCoefficients.(instance at line 19) line 19
6. instance OAI.LittleFinitistic.BimoduleCoefficients.(instance at line 21) line 21
7. instance OAI.LittleFinitistic.BimoduleCoefficients.towerLeft line 23
8. instance OAI.LittleFinitistic.BimoduleCoefficients.towerRight line 29
9. instance OAI.LittleFinitistic.BimoduleCoefficients.commute line 35
10. def OAI.LittleFinitistic.BimoduleCoefficients.map line 43
11. theorem OAI.LittleFinitistic.BimoduleCoefficients.map_left line 47