OrdinaryTensorTotalQuasiIso.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.ComplexTensor.columnMap_quasiIso line 17
Source documentation
Every shifted projective tensor column preserves arbitrary quasi-isomorphisms.
```
theorem columnMap_quasiIso (p : ℤ) [Module.Projective Aᵐᵒᵖ (rightTerm k A Q p)] [QuasiIso f] :
    QuasiIso (columnMap k A Q f p) := by
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.ComplexTensor.columnMap
theorem OAI.LittleFinitistic.ComplexTensor.finiteTotalMap_quasiIso line 28
Source documentation
The actual signed finite tensor functor preserves quasi-isomorphisms of arbitrary complexes.
```
theorem finiteTotalMap_quasiIso [∀ i, Module.Projective Aᵐᵒᵖ (rightTerm k A Q (p i))] [QuasiIso f] :
    QuasiIso (finiteTotalMap k A Q p hp f) := by
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.ComplexTensor.finiteTotalMap
def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.tensorTotalFunctor line 40
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.tensorTotalFunctor_quasiIso line 46
Source documentation
The actual bounded projective Q_T computes a homotopy-invariant tensor on every input complex.
```
theorem tensorTotalFunctor_quasiIso
    {Z Z' : CochainComplex (ModuleCat.{u} (B ⊗[k] ChainAlgebra k l)) ℤ} (f : Z ⟶ Z') [QuasiIso f] :
    QuasiIso ((tensorTotalFunctor k B l).map f) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.tensorTotalFunctor