OrdinaryXBlockComparison.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.OrdinarySimulation.XResolution.firstBlockComparison line 17
Source documentation
The first actual tensor application is exactly ordinary O tensor Z on the second block.
```
def firstBlockComparison (Z : CochainComplex (ModuleCat.{u} B) ℤ) :
    (tensorFunctor P a l).obj (BlockModule.firstComplex B (B ⊗[k] ChainAlgebra k l) Z) ≅
    BlockModule.secondComplex B (B ⊗[k] ChainAlgebra k l)
      (middleLeftComplex k (B ⊗[k] ChainAlgebra k l) B (BimoduleO P a l) Z) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.tensorFunctor, OAI.LittleFinitistic.BlockModule.firstComplex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.BlockModule.secondComplex, OAI.LittleFinitistic.middleLeftComplex, OAI.LittleFinitistic.OrdinarySimulation.BimoduleO
def OAI.LittleFinitistic.OrdinarySimulation.XResolution.secondBlockComparison line 30
Source documentation
The second actual tensor application selects Q_T and retains first-block support.
```
def secondBlockComparison (Y : CochainComplex (ModuleCat.{u} (B ⊗[k] ChainAlgebra k l)) ℤ) :
    (tensorFunctor P a l).obj (BlockModule.secondComplex B (B ⊗[k] ChainAlgebra k l) Y) ≅
    BlockModule.firstComplex B (B ⊗[k] ChainAlgebra k l)
      (BimoduleComplexTensor.total k B (B ⊗[k] ChainAlgebra k l) (TensorResolution.integerBimoduleComplex k B l) Y
        (TensorResolution.finiteDegrees l) (TensorResolution.finiteDegrees_strictMono l)) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.XResolution.tensorFunctor, OAI.LittleFinitistic.BlockModule.secondComplex, OAI.LittleFinitistic.BlockModule.firstComplex, OAI.LittleFinitistic.BimoduleComplexTensor.total, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleComplex, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees_strictMono
def OAI.LittleFinitistic.OrdinarySimulation.XResolution.squareComparison line 40
Source documentation
The complete actual chain-level square calculation, with the source support and outside action.
```
def squareComparison (b : ℤ) (hb : a+(l:ℤ)=b)
    (hP : ∀ n : ℤ, n < a ∨ b < n → IsZero (P.X n))
    (Z : CochainComplex (ModuleCat.{u} B) ℤ) :
    (tensorFunctor P a l).obj ((tensorFunctor P a l).obj (BlockModule.firstComplex B (B ⊗[k] ChainAlgebra k l) Z)) ≅
    BlockModule.firstComplex B (B ⊗[k] ChainAlgebra k l)
      (BimoduleComplexTensor.total k B B (P⟦b⟧) Z
        (TensorResolution.finiteDegrees l) (TensorResolution.finiteDegrees_strictMono l)) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.tensorFunctor, OAI.LittleFinitistic.BlockModule.firstComplex, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.BimoduleComplexTensor.total, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees_strictMono