OAI/Algebra/Finitistic/Bimodule/BoundedBimoduleDerived.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LittleFinitistic.BimoduleTotal.BoundedProjective line 13

    Source documentation

    Exactly the bounded-right-projective data needed to compute tensor on every complex.

    structure BoundedProjective (P : BiComplex k B) where
…
  2. abbrev OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.degrees line 22
  3. theorem OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.complete line 24
  4. def OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.derived line 30

    Source documentation

    The native derived tensor endofunctor of this one fixed bounded projective bimodule complex.

    def derived : DerivedCategory (ModuleCat.{u} B) ⥤ DerivedCategory (ModuleCat.{u} B) := by
…
  5. instance OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.additive line 35
  6. def OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.comparison line 40
  7. def OAI.LittleFinitistic.BimoduleTotal.BoundedProjective.singleEvaluation line 47

    Source documentation

    Agreement with the canonical native degree-zero evaluation, including its full B action.

    def singleEvaluation (N : ModuleCat.{u} B) :
    data.derived.obj (DerivedCategory.Q.obj (singleInput B N)) ≅
      DerivedCategory.Q.obj (moduleEvaluation k B P N) := by
…

    Mentions: OAI.LittleFinitistic.BimoduleTotal.singleInput, OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation