OAI/Algebra/Finitistic/Localization/SourceShiftLinear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.SourceVerdier.shiftLinearK line 11

   Source documentation

   Scalar action commutes with shifts on bounded projective homotopy complexes.

   instance shiftLinearK (n : ℤ) : (shiftFunctor (K P) n).Linear k := by
   …

   Mentions: OAI.LittleFinitistic.SourceVerdier.K

2. instance OAI.LittleFinitistic.SourceVerdier.shiftLinearQ line 22

   Source documentation

   Scalar action commutes with shifts on the actual source Verdier quotient.

   instance shiftLinearQ (n : ℤ) : (shiftFunctor (Q P) n).Linear k := by
   …

   Mentions: OAI.LittleFinitistic.SourceVerdier.Q