OrdinaryTensorTotalAcyclic.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.ComplexTensor.finiteTotal_acyclic line 19
Source documentation
The actual signed finite tensor total of projective right terms preserves acyclicity. No bound, finiteness, dimension or projectivity condition is imposed on Z.
```
theorem finiteTotal_acyclic [∀ i, Module.Projective Aᵐᵒᵖ (rightTerm k A Q (p i))]
    (hZ : Z.Acyclic) : (finiteTotal k A Q Z p hp).Acyclic :=
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.ComplexTensor.finiteTotal
def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees line 30
Source documentation
Exactly the manuscript's finite interval [-l,0] of Q_T.
```
def finiteDegrees (i : Fin (l+1)) : ℤ := -(l:ℤ) + i.val
```
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees_strictMono line 32
instance OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerTerm_moduleProjective line 38
def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.tensorTotal line 45
Source documentation
Actual signed tensor with the manuscript's Q_T on an arbitrary complex of BC-modules.
```
def tensorTotal (Z : CochainComplex (ModuleCat.{u} (B ⊗[k] ChainAlgebra k l)) ℤ) :
    CochainComplex (ModuleCat.{u} k) ℤ :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.tensorTotal_acyclic line 51
Source documentation
Q_T is K-flat in the acyclic-input characterization, for its actual signed tensor total.
```
theorem tensorTotal_acyclic (Z : CochainComplex (ModuleCat.{u} (B ⊗[k] ChainAlgebra k l)) ℤ)
    (hZ : Z.Acyclic) : (tensorTotal k B l Z).Acyclic :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.tensorTotal