OrdinaryTensorDerivedFunctor.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.ComplexTensor.finiteTotal_inverts line 18
Source documentation
The proved actual total functor sends every quasi-isomorphism to an isomorphism after localization.
```
theorem finiteTotal_inverts : (HomologicalComplex.quasiIso (ModuleCat.{u} A) (.up ℤ)).IsInvertedBy
    (finiteTotalFunctor k A Q p hp ⋙ DerivedCategory.Q) := by
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.finiteTotalFunctor
def OAI.LittleFinitistic.ComplexTensor.derivedFiniteTotal line 26
Source documentation
Localization of the actual signed total tensor functor, justified by the proved preservation theorem.
```
def derivedFiniteTotal : DerivedCategory (ModuleCat.{u} A) ⥤ DerivedCategory (ModuleCat.{u} k) :=
…
```
def OAI.LittleFinitistic.ComplexTensor.derivedFiniteTotalComparison line 31
Source documentation
The explicit natural comparison with the actual chain-level total on every input complex.
```
def derivedFiniteTotalComparison :
    DerivedCategory.Q ⋙ derivedFiniteTotal k A Q p hp ≅ finiteTotalFunctor k A Q p hp ⋙ DerivedCategory.Q :=
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.derivedFiniteTotal, OAI.LittleFinitistic.ComplexTensor.finiteTotalFunctor