OAI/Algebra/Finitistic/Bimodule/BimoduleTensorFunctor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.BimoduleBalancedTensor.algebraMap_smul line 15
2. instance OAI.LittleFinitistic.BimoduleBalancedTensor.scalarTower line 35
3. def OAI.LittleFinitistic.BimoduleBalancedTensor.map line 40

   Source documentation

   A genuine bimodule map induces a map preserving the full left B action after tensoring.

   def map (f : M ⟶ M') : Tensor k B M N →ₗ[B] Tensor k B M' N where
   …

   Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.Tensor

4. def OAI.LittleFinitistic.BimoduleBalancedTensor.functor line 61

   Source documentation

   The actual balanced tensor functor from bimodules to left modules.

   def functor : ModuleCat.{u} (Enveloping k B) ⥤ ModuleCat.{u} B where
   …

5. instance OAI.LittleFinitistic.BimoduleBalancedTensor.additive line 85