OAI/Algebra/Finitistic/Bimodule/BimoduleScalarEvaluation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleTotal.CanonicalInput line 11
2. def OAI.LittleFinitistic.BimoduleTotal.toNativeScalar line 15
3. def OAI.LittleFinitistic.BimoduleTotal.fromNativeScalar line 26
4. def OAI.LittleFinitistic.BimoduleTotal.scalarTensorIso line 38

   Source documentation

   Canonical restriction and the native compatible k action give the same B-valued tensor.

   def scalarTensorIso :
       (BimoduleBalancedTensor.functor k B (CanonicalInput k B N)).obj M ≅
         (BimoduleBalancedTensor.functor k B N).obj M where
   …

   Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BimoduleTotal.CanonicalInput

5. theorem OAI.LittleFinitistic.BimoduleTotal.scalarTensor_natural line 65
6. def OAI.LittleFinitistic.BimoduleTotal.scalarEvaluationIso line 79

   Source documentation

   Exact comparison to native module evaluation with its original compatible scalar structure.

   def scalarEvaluationIso (P : BiComplex k B) :
       moduleEvaluation k B P (ModuleCat.of B N) ≅
         ((BimoduleBalancedTensor.functor k B N).mapHomologicalComplex (.up ℤ)).obj P :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation, OAI.LittleFinitistic.BimoduleBalancedTensor.functor