OAI/Algebra/Finitistic/Bimodule/BimoduleDerivedShift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.BimoduleTotal.derived_commShift line 18

   Source documentation

   The proved total-complex shift structure descends through the native derived localization.

   instance derived_commShift : (derived k B P p hp).CommShift ℤ := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.derived

2. instance OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.commShift line 32
3. def OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.shiftComparison line 39

   Source documentation

   Full left B-valued derived tensor commutes with every integer shift.

   def shiftComparison (s : ℤ) : shiftFunctor _ s ⋙ data.derived ≅ data.derived ⋙ shiftFunctor _ s :=
   …