OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorBimoduleResolution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleTerm line 13
2. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleDifferential line 15
3. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleDifferential_square line 18
4. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleComplex line 25

   Source documentation

   The actual finite resolution retains the left B-action as a genuine tensor-algebra complex.

   def bimoduleComplex : CochainComplex (ModuleCat.{u} (B ⊗[k] (B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ)) ℕ :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

5. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleComplex line 31

   Source documentation

   The genuine bimodule resolution in exactly the source interval [-l,0].

   def integerBimoduleComplex : CochainComplex (ModuleCat.{u} (B ⊗[k] (B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ)) ℤ :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

6. abbrev OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimodule line 34
7. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimoduleTerm line 39
8. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimoduleComplex line 55

   Source documentation

   Forgetting the retained left action recovers the verified ordinary finite resolution.

   def forgetBimoduleComplex :
       ((forgetBimodule k B l).mapHomologicalComplex (.up ℕ)).obj (bimoduleComplex k B l) ≅ complex k B l :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimodule, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleComplex, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.complex

9. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetIntegerBimoduleComplex line 72

   Source documentation

   Every integer term and differential agrees after forgetting the left action.

   def forgetIntegerBimoduleComplex :
       ((forgetBimodule k B l).mapHomologicalComplex (.up ℤ)).obj (integerBimoduleComplex k B l) ≅
         integerComplex k B l :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimodule, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleComplex, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerComplex