OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleTotalMaps.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleComplexTensor.termInputMap line 15
2. theorem OAI.LittleFinitistic.BimoduleComplexTensor.termInputMap_id line 20
3. theorem OAI.LittleFinitistic.BimoduleComplexTensor.termInputMap_comp line 27
4. def OAI.LittleFinitistic.BimoduleComplexTensor.totalInputMap line 35
5. theorem OAI.LittleFinitistic.BimoduleComplexTensor.forget_totalInputMap line 39

   Source documentation

   The retained-action input map is exactly the prior tensor map after forgetting.

   theorem forget_totalInputMap (n : ℤ) (z : totalTerm k S A Q Z p n) :
       forgetTotalEquiv k S A Q Z' p n (totalInputMap k S A Q f p n z) =
         ((ComplexTensor.finiteTotalMap k A (rightComplex k S A Q) p hp f).f n).hom
           (forgetTotalEquiv k S A Q Z p n z) := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.totalTerm, OAI.LittleFinitistic.BimoduleComplexTensor.forgetTotalEquiv, OAI.LittleFinitistic.BimoduleComplexTensor.totalInputMap, OAI.LittleFinitistic.ComplexTensor.finiteTotalMap, OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex

6. theorem OAI.LittleFinitistic.BimoduleComplexTensor.totalInputMap_comm line 61
7. def OAI.LittleFinitistic.BimoduleComplexTensor.totalMap line 80

   Source documentation

   Actual chain maps of the outside-action tensor total.

   def totalMap : total k S A Q Z p hp ⟶ total k S A Q Z' p hp where
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.total

8. theorem OAI.LittleFinitistic.BimoduleComplexTensor.forgetTotalIso_natural line 95