OrdinaryDerivedSquareComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedSquareComparison line 21
Source documentation
The actual native derived square comparison on every complex Z, with first-block support. Both tensor functors are the localization lifts of their verified bounded projective models.
```
def derivedSquareComparison (Z : CochainComplex (ModuleCat.{u} B) ℤ) :
    (derivedTensor P a l).obj ((derivedTensor P a l).obj
      ((BlockModule.derivedFirst B (B ⊗[k] ChainAlgebra k l)).obj (DerivedCategory.Q.obj Z))) ≅
    (BlockModule.derivedFirst B (B ⊗[k] ChainAlgebra k l)).obj
      ((shiftedDerivedTensor P b l).obj (DerivedCategory.Q.obj Z)) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedTensor, OAI.LittleFinitistic.BlockModule.derivedFirst, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.shiftedDerivedTensor