OAI/Algebra/Finitistic/Ordinary/OrdinaryCompression.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.underlyingComplex line 15

   Source documentation

   Forgetting to k uses the actual restriction-of-scalars functor on complexes.

   abbrev underlyingComplex (P : CochainComplex (ModuleCat.{u} A) ℤ) :
       CochainComplex (ModuleCat.{u} k) ℤ :=
   …

2. def OAI.LittleFinitistic.OrdinarySimulation.Compression line 21

   Source documentation

   Ordinary finite compression of the actual dg A-module P on [a,a+l]. Take A=B tensor Bᵐᵒᵖ for a genuine dg B-bimodule.

   def Compression (P : CochainComplex (ModuleCat.{u} A) ℤ) (a : ℤ) (l : ℕ) :=
   …

3. instance OAI.LittleFinitistic.OrdinarySimulation.Compression.(instance at line 26) line 26
4. instance OAI.LittleFinitistic.OrdinarySimulation.Compression.(instance at line 28) line 28
5. instance OAI.LittleFinitistic.OrdinarySimulation.Compression.(instance at line 30) line 30
6. instance OAI.LittleFinitistic.OrdinarySimulation.Compression.(instance at line 32) line 32
7. instance OAI.LittleFinitistic.OrdinarySimulation.Compression.(instance at line 34) line 34
8. instance OAI.LittleFinitistic.OrdinarySimulation.Compression.scalarTowerA line 37
9. instance OAI.LittleFinitistic.OrdinarySimulation.Compression.(instance at line 43) line 43
10. def OAI.LittleFinitistic.OrdinarySimulation.Compression.tensorAction line 55

    Source documentation

    The commuting actions give the actual tensor-algebra representation.

    def tensorAction : (A ⊗[k] ChainAlgebra k l) →ₐ[k] Module.End k (Compression P a l) :=
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.Compression

11. theorem OAI.LittleFinitistic.OrdinarySimulation.Compression.tensorAction_tmul line 63
12. instance OAI.LittleFinitistic.OrdinarySimulation.Compression.finiteDimensional line 66