OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleDerivedTensor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LittleFinitistic.BimoduleComplexTensor.total_inverts line 19
  2. def OAI.LittleFinitistic.BimoduleComplexTensor.derivedTotal line 27

    Source documentation

    Localization of the actual tensor total, retaining the outside action.

    def derivedTotal : DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} S) :=
…
  3. def OAI.LittleFinitistic.BimoduleComplexTensor.derivedTotalComparison line 31
  4. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.derivedBimoduleTensor line 43

    Source documentation

    The actual Q_T tensor lift with the source's left B-action retained.

    def derivedBimoduleTensor : DerivedCategory (ModuleCat.{u} (B ⊗[k] ChainAlgebra k l)) ⥤
    DerivedCategory (ModuleCat.{u} B) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

  5. def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.derivedBimoduleTensorComparison line 48