OAI/Algebra/Finitistic/Ordinary/OrdinaryShiftDerivedTensor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.OrdinarySimulation.shifted_right_projective line 15
2. def OAI.LittleFinitistic.OrdinarySimulation.shiftedDerivedTensor line 22

   Source documentation

   The native derived tensor functor computed by the source's actual bounded P[b].

   def shiftedDerivedTensor : DerivedCategory (ModuleCat.{u} B) ⥤ DerivedCategory (ModuleCat.{u} B) :=
   …

3. def OAI.LittleFinitistic.OrdinarySimulation.shiftedDerivedTensorComparison line 26
4. theorem OAI.LittleFinitistic.OrdinarySimulation.shifted_support line 34