OrdinaryGenuineBimoduleComparison.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.OrdinarySimulation.genuineTensorFunctor line 14
def OAI.LittleFinitistic.OrdinarySimulation.genuineFiniteTermIso line 17
def OAI.LittleFinitistic.OrdinarySimulation.genuineFiniteComplexIso line 31
Source documentation
The actual finite bimodule tensor agrees with the existing full computation, preserving both B-actions.
```
def genuineFiniteComplexIso :
    ((genuineTensorFunctor P a l).mapHomologicalComplex (.up ℕ)).obj
      (TensorResolution.bimoduleComplex k B l) ≅ FullTensorTerm.complex P a l :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.genuineTensorFunctor, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleComplex, OAI.LittleFinitistic.OrdinarySimulation.FullTensorTerm.complex
def OAI.LittleFinitistic.OrdinarySimulation.genuineComputedTensor line 58
Source documentation
The actual all-integer tensor of genuine Q_T with O, retaining both outside B-actions.
```
def genuineComputedTensor : CochainComplex (ModuleCat.{u} (Enveloping k B)) ℤ :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.Enveloping
def OAI.LittleFinitistic.OrdinarySimulation.genuineComputedTensorIso line 63
Source documentation
Agreement with the preserved full signed-comparison input in every integer degree.
```
def genuineComputedTensorIso : genuineComputedTensor P a l ≅ computedTensorComplex P a l :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.genuineComputedTensor, OAI.LittleFinitistic.OrdinarySimulation.computedTensorComplex
def OAI.LittleFinitistic.OrdinarySimulation.genuineSourceShiftComparison line 70
Source documentation
The actual ordinary tensor Q_T tensor O is isomorphic to P[b] as B-bimodule complexes. Only the manuscript support and indexing hypotheses are used.
```
def genuineSourceShiftComparison (b : ℤ) (hb : a+(l:ℤ)=b)
    (hP : ∀ n : ℤ, n < a ∨ b < n → IsZero (P.X n)) :
    genuineComputedTensor P a l ≅ P⟦b⟧ :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.genuineComputedTensor