OAI/Algebra/Finitistic/Localization/SourceOddDoubleEvaluation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.SourceImageEvaluation.compose_square line 9
2. def OAI.LittleFinitistic.SourceImageEvaluation.shiftIso line 23

   Source documentation

   The additive extension respects the native formal shift.

   def shiftIso (n : ℤ) :
       OddDouble.formalShiftFunctor (C := SourceVerdier.Q E.relations) n ⋙ completed (Y := Y) E ≅
   …

   Mentions: OAI.LittleFinitistic.OddDouble.formalShiftFunctor, OAI.LittleFinitistic.SourceVerdier.Q, OAI.LittleFinitistic.SourceImageEvaluation.completed

3. def OAI.LittleFinitistic.SourceImageEvaluation.shiftedImageIso line 28
4. theorem OAI.LittleFinitistic.SourceImageEvaluation.shifted_corner_square line 34
5. def OAI.LittleFinitistic.SourceImageEvaluation.oddDoubleImageIso line 51
6. theorem OAI.LittleFinitistic.SourceImageEvaluation.oddDouble_corner_square line 57
7. theorem OAI.LittleFinitistic.SourceImageEvaluation.oddDouble_selecting_square line 69