OAI/Algebra/Finitistic/Ordinary/OrdinaryOffDiagonalComplex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complexTerm line 15
2. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complexDifferential line 18
3. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complexDifferential_square line 27
4. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complex line 36

   Source documentation

   Actual off-diagonal complex with both actions of the product algebra retained.

   def complex : CochainComplex (ModuleCat.{u} ((L × R) ⊗[k] (L × R)ᵐᵒᵖ)) ℤ :=
   …