OAI/Algebra/Finitistic/Bimodule/BimoduleShiftedPresentation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotalPresentation.shiftedDerivedIso line 24

   Source documentation

   The ordinary shifted-derived API agrees with any native model of the identical shifted complex on [-length,0]. No shift-left tensor theorem is reproved or assumed.

   def shiftedDerivedIso (hlo : data.lower = -(length : ℤ)) (hhi : data.upper = 0) :
       OrdinarySimulation.shiftedDerivedTensor P b length ≅ data.derived :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.shiftedDerivedTensor

2. def OAI.LittleFinitistic.BimoduleTotalPresentation.shiftedPowerIso line 29

   Source documentation

   The same comparison on every actual shifted-derived iterate.

   def shiftedPowerIso (hlo : data.lower = -(length : ℤ)) (hhi : data.upper = 0)
       (r : ℕ) (Y : DerivedCategory (ModuleCat.{u} B)) :
       ((OrdinarySimulation.shiftedDerivedTensor P b length).obj^[r]) Y ≅
         (data.derived.obj^[r]) Y :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.shiftedDerivedTensor