OrdinarySimulationComparison.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.OrdinarySimulation.differential_transport line 14
def OAI.LittleFinitistic.OrdinarySimulation.restrictedShiftIso line 21
Source documentation
Align the finite resolution's degree n with the source's degree a+n.
```
def restrictedShiftIso : P.restriction (ComplexShape.embeddingUpIntGE a) ≅
    (unsignedShift P (a+(l:ℤ))).restriction (TensorResolution.degreeEmbedding l) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.unsignedShift, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.degreeEmbedding
theorem OAI.LittleFinitistic.OrdinarySimulation.unsignedSupport line 35
Source documentation
The lower support condition of the manuscript supplies strict support after reindexing.
```
theorem unsignedSupport (hP : ∀ n : ℤ, n < a → IsZero (P.X n)) :
    (unsignedShift P (a+(l:ℤ))).IsStrictlySupported (TensorResolution.degreeEmbedding l) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.unsignedShift, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.degreeEmbedding
def OAI.LittleFinitistic.OrdinarySimulation.computedTensorComplex line 50
Source documentation
The computed BC-balanced tensor complex in degrees -l,...,0 with both B-actions.
```
def computedTensorComplex : CochainComplex (ModuleCat.{u} (Enveloping k B)) ℤ :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.Enveloping
def OAI.LittleFinitistic.OrdinarySimulation.computedTensorIso line 54
Source documentation
Full bimodule chain comparison, including all zero terms and the genuine integer shift sign.
```
def computedTensorIso
    (hLower : ∀ n : ℤ, n < a → IsZero (P.X n))
    (hUpper : ∀ n : ℕ, l < n → IsZero (P.X (a+(n:ℤ)))) :
    computedTensorComplex P a l ≅ P⟦a+(l:ℤ)⟧ := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.computedTensorComplex
def OAI.LittleFinitistic.OrdinarySimulation.sourceShiftComparison line 65
Source documentation
Exact source indexing: b=a+l, with only the manuscript's support hypothesis.
```
def sourceShiftComparison (b : ℤ) (hb : a+(l:ℤ)=b)
    (hP : ∀ n : ℤ, n < a ∨ b < n → IsZero (P.X n)) :
    computedTensorComplex P a l ≅ P⟦b⟧ := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.computedTensorComplex