OAI/Algebra/Finitistic/Ordinary/OrdinaryOffDiagonalSingle.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.singles line 13
2. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.singles_isZero line 17
3. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.singleTermIso line 21
4. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.singleIso line 32

   Source documentation

   The off-diagonal direct sum of two ordinary modules is their ordinary bimodule in degree zero.

   def singleIso : singles k L R O T ≅
       (HomologicalComplex.single _ (.up ℤ) 0).obj (object k L R O T) :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.singles, OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.object