BimoduleDerivedFunctor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.inverts line 16
Source documentation
Every quasi-isomorphism becomes invertible after applying the actual B-valued total.
```
theorem inverts : (HomologicalComplex.quasiIso (ModuleCat.{u} B) (.up ℤ)).IsInvertedBy
    (functor k B P p hp ⋙ DerivedCategory.Q) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.functor
def OAI.LittleFinitistic.BimoduleTotal.derived line 24
Source documentation
The actual fixed bimodule tensor total descends to the native derived category of B-modules.
```
def derived : DerivedCategory (ModuleCat.{u} B) ⥤ DerivedCategory (ModuleCat.{u} B) :=
…
```
def OAI.LittleFinitistic.BimoduleTotal.derivedComparison line 29
Source documentation
This derived endofunctor is computed by the signed tensor total on every input complex.
```
def derivedComparison : DerivedCategory.Q ⋙ derived k B P p hp ≅
    functor k B P p hp ⋙ DerivedCategory.Q :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.derived, OAI.LittleFinitistic.BimoduleTotal.functor
instance OAI.LittleFinitistic.BimoduleTotal.derived_additive line 34