OAI/Algebra/Finitistic/Ordinary/OrdinaryOffDiagonalComplexMaps.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complexTermMap line 13
2. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complex_d line 21
3. def OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complexMap line 27

   Source documentation

   An actual map of off-diagonal complexes retaining both product-ring actions.

   def complexMap (f : O ⟶ O') (g : T ⟶ T') : complex k L R O T ⟶ complex k L R O' T' where
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complex