OAI/Algebra/Finitistic/Localization/NativeSingleEvaluation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.nativeSingleEvaluation line 15

   Source documentation

   Native degree-zero module embedding, with the module's original compatible scalar action.

   def nativeSingleEvaluation (N : Type u) [AddCommGroup N] [Module k N] [Module B N]
       [IsScalarTower k B N] :
       data.derived.obj ((DerivedCategory.singleFunctor (ModuleCat.{u} B) 0).obj (ModuleCat.of B N)) ≅
         DerivedCategory.Q.obj (((BimoduleBalancedTensor.functor k B N).mapHomologicalComplex (.up ℤ)).obj P) :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor