OAI/Algebra/Finitistic/Bimodule/BimoduleInputNaturality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.BimoduleTotal.input_tensor_square line 13

   Source documentation

   The canonical maps in the two tensor variables commute, preserving the full outside action.

   theorem input_tensor_square {M M' : ModuleCat.{u} (Enveloping k B)}
       {N N' : ModuleCat.{u} B} (f : M ⟶ M') (g : N ⟶ N') :
       (inputFunctor k B M).map g ≫
         (BimoduleBalancedTensor.functor k B (BalancedTensor.ScalarLeftModule k B N')).map f =
       (BimoduleBalancedTensor.functor k B (BalancedTensor.ScalarLeftModule k B N)).map f ≫
         (inputFunctor k B M').map g := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.inputFunctor, OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BalancedTensor.ScalarLeftModule

2. theorem OAI.LittleFinitistic.BimoduleTotal.termMap_decompose line 32