OAI/Algebra/Finitistic/Ordinary/OrdinaryFirstBlockTotal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.BlockTensor.firstTotalEquiv line 17
2. theorem OAI.LittleFinitistic.OrdinarySimulation.BlockTensor.firstTotalEquiv_apply line 24
3. theorem OAI.LittleFinitistic.OrdinarySimulation.BlockTensor.first_entry line 29
4. theorem OAI.LittleFinitistic.OrdinarySimulation.BlockTensor.first_vertical line 52
5. theorem OAI.LittleFinitistic.OrdinarySimulation.BlockTensor.first_differential line 60
6. def OAI.LittleFinitistic.OrdinarySimulation.BlockTensor.firstTotalIso line 89

   Source documentation

   Actual tensor with the off-diagonal complex on a first-block input is the second-block O-total.

   def firstTotalIso :
       total k (L × R) (L × R) (OffDiagonal.complex k L R O T) (BlockModule.firstComplex L R Z) p hp ≅
         BlockModule.secondComplex L R (total k R L O Z p hp) :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complex, OAI.LittleFinitistic.BlockModule.firstComplex, OAI.LittleFinitistic.BlockModule.secondComplex