OrdinaryBimoduleTotalFunctor.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BimoduleComplexTensor.totalFunctor line 16
Source documentation
The actual tensor total is a functor retaining its outside action on every complex.
```
def totalFunctor : CochainComplex (ModuleCat.{u} A) ℤ ⥤ CochainComplex (ModuleCat.{u} S) ℤ where
…
```
def OAI.LittleFinitistic.BimoduleComplexTensor.forgetTotalFunctorIso line 42
Source documentation
The forgetful chain comparison is natural in all input complexes.
```
def forgetTotalFunctorIso :
    totalFunctor k S A Q p hp ⋙ (ModuleCat.restrictScalars (algebraMap k S)).mapHomologicalComplex (.up ℤ) ≅
    ComplexTensor.finiteTotalFunctor k A (rightComplex k S A Q) p hp :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.totalFunctor, OAI.LittleFinitistic.ComplexTensor.finiteTotalFunctor, OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex
theorem OAI.LittleFinitistic.BimoduleComplexTensor.totalFunctor_quasiIso line 50
Source documentation
The genuine outside-action tensor preserves arbitrary quasi-isomorphisms when its right terms are projective. There are no restrictions on either input complex.
```
theorem totalFunctor_quasiIso
    [∀ i, Module.Projective Aᵐᵒᵖ (ComplexTensor.rightTerm k A (rightComplex k S A Q) (p i))]
    {Z Z' : CochainComplex (ModuleCat.{u} A) ℤ} (f : Z ⟶ Z') [QuasiIso f] :
    QuasiIso ((totalFunctor k S A Q p hp).map f) := by
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex, OAI.LittleFinitistic.BimoduleComplexTensor.totalFunctor, OAI.LittleFinitistic.BimoduleComplexTensor.map