OAI/Algebra/Finitistic/Ordinary/OrdinarySingleTensorTotal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.SingleBimoduleTensor.entry_selected_zero line 17
2. theorem OAI.LittleFinitistic.SingleBimoduleTensor.differential_selected line 28
3. theorem OAI.LittleFinitistic.SingleBimoduleTensor.termEquivAt_vertical line 36
4. theorem OAI.LittleFinitistic.SingleBimoduleTensor.totalTermEquiv_differential line 51
5. def OAI.LittleFinitistic.SingleBimoduleTensor.shiftedTotalIso line 61

   Source documentation

   A genuine ordinary bimodule in degree zero has exactly its ordinary tensor complex as total.

   def shiftedTotalIso : total k S A (complex k S A N) Z p hp ≅ (middleLeftComplex k S A N Z)⟦-(p i₀)⟧ :=
   …

   Mentions: OAI.LittleFinitistic.SingleBimoduleTensor.complex, OAI.LittleFinitistic.middleLeftComplex

6. def OAI.LittleFinitistic.SingleBimoduleTensor.totalIso line 76

   Source documentation

   Removing the proved zero shift identifies the ordinary tensor complex exactly.

   def totalIso : total k S A (complex k S A N) Z p hp ≅ middleLeftComplex k S A N Z :=
   …

   Mentions: OAI.LittleFinitistic.SingleBimoduleTensor.complex, OAI.LittleFinitistic.middleLeftComplex