OAI/Algebra/Finitistic/Ordinary/OrdinaryXDerivedTensor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.LittleFinitistic.OrdinarySimulation.XResolution.rightTerm_projective line 13
  2. abbrev OAI.LittleFinitistic.OrdinarySimulation.XResolution.tensorFunctor line 19

    Source documentation

    Tensor with the actual right-projective Q_X on arbitrary input complexes of D-modules.

    abbrev tensorFunctor := BimoduleComplexTensor.totalFunctor k (AlgebraD k l B) (AlgebraD k l B)
…

    Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.totalFunctor, OAI.LittleFinitistic.OrdinarySimulation.AlgebraD

  3. theorem OAI.LittleFinitistic.OrdinarySimulation.XResolution.tensorFunctor_quasiIso line 22
  4. def OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedTensor line 30

    Source documentation

    The derived endofunctor obtained from the actual bounded resolution of X.

    def derivedTensor : DerivedCategory (ModuleCat.{u} (AlgebraD k l B)) ⥤
    DerivedCategory (ModuleCat.{u} (AlgebraD k l B)) :=
…

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.AlgebraD

  5. def OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedTensorComparison line 35