BimoduleDerivedPresentation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.LittleFinitistic.BimoduleTotalPresentation.ordinaryProjective line 19
Source documentation
The coefficient presentations have exactly the same right module structure.
```
instance ordinaryProjective : ∀ i, Module.Projective Bᵐᵒᵖ
    (ComplexTensor.rightTerm k B (BimoduleComplexTensor.rightComplex k B B P) (p i)) :=
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex
def OAI.LittleFinitistic.BimoduleTotalPresentation.derivedIso line 25
Source documentation
The already proved chain comparison descends through the actual localization.
```
def derivedIso : BimoduleComplexTensor.derivedTotal k B B P p hp ≅
    BimoduleTotal.derived k B P p hp :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.derivedTotal, OAI.LittleFinitistic.BimoduleTotal.derived
theorem OAI.LittleFinitistic.BimoduleTotalPresentation.derivedIso_comparison line 35
Source documentation
Exact compatibility with the two localization comparison maps.
```
theorem derivedIso_comparison :
    whiskerLeft DerivedCategory.Q (derivedIso k B P p hp).hom ≫
      (BimoduleTotal.derivedComparison k B P p hp).hom =
    (BimoduleComplexTensor.derivedTotalComparison k B B P p hp).hom ≫
      whiskerRight (totalFunctorIso k B P p hp).hom DerivedCategory.Q := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotalPresentation.derivedIso, OAI.LittleFinitistic.BimoduleTotal.derivedComparison, OAI.LittleFinitistic.BimoduleComplexTensor.derivedTotalComparison, OAI.LittleFinitistic.BimoduleTotalPresentation.totalFunctorIso

def OAI.LittleFinitistic.BimoduleTotalPresentation.enumerationIso line 58

Source documentation

Transport only the finite indexing type; every degree and both signed maps are unchanged.

def enumerationIso {l l' : ℕ} (p : Fin l → ℤ) (q : Fin l' → ℤ)
    (hp : StrictMono p) (hq : StrictMono q) (hl : l = l')
    (he : ∀ i, p i = q (Fin.cast hl i)) :
    BimoduleTotal.functor k B P p hp ≅ BimoduleTotal.functor k B P q hq := by
…

Mentions: OAI.LittleFinitistic.BimoduleTotal.functor

def OAI.LittleFinitistic.BimoduleTotalPresentation.nonpositiveTotalFunctorIso line 68
Source documentation
Exact comparison of the ordinary resolution's finite list with the native interval.
```
def nonpositiveTotalFunctorIso (length : ℕ) :
    BimoduleComplexTensor.totalFunctor k B B P
      (OrdinarySimulation.TensorResolution.finiteDegrees length)
      (OrdinarySimulation.TensorResolution.finiteDegrees_strictMono length) ≅
    BimoduleTotal.functor k B P (BimoduleTotal.intervalDegrees (-(length : ℤ)) 0)
      (BimoduleTotal.intervalDegrees_strictMono (-(length : ℤ)) 0) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.totalFunctor, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees_strictMono, OAI.LittleFinitistic.BimoduleTotal.functor, OAI.LittleFinitistic.BimoduleTotal.intervalDegrees, OAI.LittleFinitistic.BimoduleTotal.intervalDegrees_strictMono
def OAI.LittleFinitistic.BimoduleTotalPresentation.boundedDerivedIso line 80
Source documentation
The comparison for exactly the same bounded Q and its chosen interval.
```
def boundedDerivedIso :
    (letI : ∀ i, Module.Projective Bᵐᵒᵖ
        (ComplexTensor.rightTerm k B (BimoduleTotal.right k B P) (data.degrees i)) :=
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.rightTerm, OAI.LittleFinitistic.BimoduleTotal.right