OAI/Algebra/Finitistic/Ordinary/OrdinaryRetainedRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.RetainedBimodule.object line 14
2. def OAI.LittleFinitistic.RetainedBimodule.rightEquiv line 17

   Source documentation

   Recover the exact original right action after packaging the ordinary bimodule.

   def rightEquiv : BimoduleCoefficients k S A (object k S A M) ≃ₗ[Aᵐᵒᵖ] M where
   …

   Mentions: OAI.LittleFinitistic.BimoduleCoefficients, OAI.LittleFinitistic.RetainedBimodule.object

3. theorem OAI.LittleFinitistic.RetainedBimodule.rightEquiv_left line 30
4. def OAI.LittleFinitistic.RetainedBimodule.scalarEquiv line 39

   Source documentation

   Recover the exact original scalar module after retaining both actions.

   def scalarEquiv : (ModuleCat.restrictScalars (algebraMap k (S ⊗[k] Aᵐᵒᵖ))).obj
       (object k S A M) ≃ₗ[k] M where
   …

   Mentions: OAI.LittleFinitistic.RetainedBimodule.object