OAI/Algebra/Finitistic/Bimodule/BimoduleTotalTerms.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleTotal.right line 14
2. abbrev OAI.LittleFinitistic.BimoduleTotal.Term line 17
3. theorem OAI.LittleFinitistic.BimoduleTotal.bimap_smul line 25

   Source documentation

   Balanced tensor maps retain the original outside left B action.

   theorem bimap_smul (f : P.X p ⟶ P.X p') (g : Z.X q ⟶ Z'.X q')
       (b : B) (x : Term k B P Z p q) :
       @BalancedTensor.bimap k B
         (ComplexTensor.rightTerm k B (right k B P) p)
         (ComplexTensor.rightTerm k B (right k B P) p')
         (ComplexTensor.leftTerm k B Z q) (ComplexTensor.leftTerm k B Z' q') _ _ _
         _ _ _ (BalancedTensor.scalarLeftTower k Bᵐᵒᵖ ((right k B P).X p))
         _ _ _ (BalancedTensor.scalarLeftTower k Bᵐᵒᵖ ((right k B P).X p'))
         _ _ _ (BalancedTensor.scalarLeftTower k B (Z.X q))
         _ _ _ (BalancedTensor.scalarLeftTower k B (Z'.X q'))
         ((forgetRight k B).map f).hom g.hom (b • x) =
       b • (show Term k B P Z' p' q' from @BalancedTensor.bimap k B
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.BalancedTensor.bimap, OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.BimoduleTotal.right, OAI.LittleFinitistic.ComplexTensor.leftTerm, OAI.LittleFinitistic.BalancedTensor.scalarLeftTower

4. theorem OAI.LittleFinitistic.BimoduleTotal.horizontal_smul line 68
5. theorem OAI.LittleFinitistic.BimoduleTotal.column_d_smul line 75
6. theorem OAI.LittleFinitistic.BimoduleTotal.inputMap_smul line 91