OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleResolutionProjective.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleRight_projective line 14

   Source documentation

   The actual genuine bimodule resolution is right-projective in every integer degree.

   instance integerBimoduleRight_projective (n : ℤ) :
       Module.Projective (B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ
         (ComplexTensor.rightTerm k (B ⊗[k] ChainAlgebra k l)
           (BimoduleComplexTensor.rightComplex k B (B ⊗[k] ChainAlgebra k l) (integerBimoduleComplex k B l)) n) := by
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleComplex

2. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimodule_lower line 24
3. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimodule_upper line 30