OrdinaryDerivedIterates.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedSquareObject line 19
Source documentation
The actual ordinary square on every native derived object, using essential surjectivity of Q.
```
def derivedSquareObject (Y : DerivedCategory (ModuleCat.{u} B)) :
    (derivedTensor P a l).obj ((derivedTensor P a l).obj
      ((BlockModule.derivedFirst B (B ⊗[k] ChainAlgebra k l)).obj Y)) ≅
    (BlockModule.derivedFirst B (B ⊗[k] ChainAlgebra k l)).obj
      ((shiftedDerivedTensor P b l).obj Y) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedTensor, OAI.LittleFinitistic.BlockModule.derivedFirst, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.shiftedDerivedTensor
def OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedEvenIterate line 32
Source documentation
Every even iterate is the first-block inflation of the corresponding actual P[b] tensor iterate.
```
def derivedEvenIterate (n : ℕ) (Y : DerivedCategory (ModuleCat.{u} B)) :
    ((derivedTensor P a l).obj)^[2*n]
      ((BlockModule.derivedFirst B (B ⊗[k] ChainAlgebra k l)).obj Y) ≅
    (BlockModule.derivedFirst B (B ⊗[k] ChainAlgebra k l)).obj
      (((shiftedDerivedTensor P b l).obj)^[n] Y) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedTensor, OAI.LittleFinitistic.BlockModule.derivedFirst, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.shiftedDerivedTensor