OrdinarySourceResolutionModels.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees_range line 15
def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.resolutionModel line 29
Source documentation
The actual Q_T augmentation with all source resolution obligations proved.
```
def resolutionModel (k B : Type u) [Field k] [Ring B] [Algebra k B] (l : ℕ) :
    BoundedBimoduleResolution k B (B ⊗[k] ChainAlgebra k l) (bimoduleTerminalObject k B l) where
…
```
Mentions: OAI.LittleFinitistic.BoundedBimoduleResolution, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleTerminalObject
def OAI.LittleFinitistic.OrdinarySimulation.XResolution.resolutionModel line 49
Source documentation
The actual Q_X resolution with no assumed augmentation, projectivity, or support theorem.
```
def XResolution.resolutionModel :
    BoundedBimoduleResolution k (AlgebraD k l B) (AlgebraD k l B) (XResolution.ordinaryXObject P a l) where
…
```
Mentions: OAI.LittleFinitistic.BoundedBimoduleResolution, OAI.LittleFinitistic.OrdinarySimulation.AlgebraD, OAI.LittleFinitistic.OrdinarySimulation.XResolution.ordinaryXObject
def OAI.LittleFinitistic.OrdinarySimulation.shiftedResolutionModel line 64
Source documentation
The actual P[b] itself is a finite right-projective tensor model with exactly the source support.
```
def shiftedResolutionModel (b : ℤ) (hb : a+(l:ℤ)=b)
    (hP : ∀ n : ℤ, n < a ∨ b < n → IsZero (P.X n)) : FiniteProjectiveBimoduleComplex k B B where
…
```
Mentions: OAI.LittleFinitistic.FiniteProjectiveBimoduleComplex