BimoduleBoundedPresentation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.LittleFinitistic.BimoduleTotalPresentation.projectiveDegrees line 12
def OAI.LittleFinitistic.BimoduleTotalPresentation.boundedNonpositiveTotalIso line 22
Source documentation
Any native bounded model with these endpoints uses exactly the ordinary finite degree list.
```
def boundedNonpositiveTotalIso (hlo : data.lower = -(length : ℤ)) (hhi : data.upper = 0) :
    BimoduleComplexTensor.totalFunctor k B B P p hp ≅
      BimoduleTotal.functor k B P data.degrees
        (BimoduleTotal.intervalDegrees_strictMono data.lower data.upper) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.totalFunctor, OAI.LittleFinitistic.BimoduleTotal.functor, OAI.LittleFinitistic.BimoduleTotal.intervalDegrees_strictMono
def OAI.LittleFinitistic.BimoduleTotalPresentation.boundedNonpositiveDerivedIso line 35
Source documentation
Generic bridge for a shifted P as well as Q_X. No augmentation or target module is needed to compare two presentations of the very same bounded complex.
```
def boundedNonpositiveDerivedIso (hlo : data.lower = -(length : ℤ)) (hhi : data.upper = 0) :
    BimoduleComplexTensor.derivedTotal k B B P p hp ≅ data.derived :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.derivedTotal

theorem OAI.LittleFinitistic.BimoduleTotalPresentation.boundedNonpositiveDerivedIso_comparison line 45

Source documentation

Exact localization compatibility for the generic bounded model.

theorem boundedNonpositiveDerivedIso_comparison (hlo : data.lower = -(length : ℤ)) (hhi : data.upper = 0) :
    whiskerLeft DerivedCategory.Q (boundedNonpositiveDerivedIso k B P data length hlo hhi).hom ≫
      data.comparison.hom =
    (BimoduleComplexTensor.derivedTotalComparison k B B P p hp).hom ≫
      whiskerRight (boundedNonpositiveTotalIso k B P data length hlo hhi).hom DerivedCategory.Q := by
…

Mentions: OAI.LittleFinitistic.BimoduleTotalPresentation.boundedNonpositiveDerivedIso, OAI.LittleFinitistic.BimoduleComplexTensor.derivedTotalComparison, OAI.LittleFinitistic.BimoduleTotalPresentation.boundedNonpositiveTotalIso

def OAI.LittleFinitistic.BimoduleTotalPresentation.powerObjIso line 63

Source documentation

A natural endofunctor comparison identifies every actual object-function iterate.

def powerObjIso {C : Type*} [Category C] {F G : C ⥤ C} (e : F ≅ G) :
    (r : ℕ) → (Y : C) → (F.obj^[r]) Y ≅ (G.obj^[r]) Y
  | 0, Y => Iso.refl Y
  | r+1, Y => by
    rw [Function.iterate_succ_apply', Function.iterate_succ_apply']
    exact e.app _ ≪≫ G.mapIso (powerObjIso e r Y)

/-- Direct iterate transport for any same-complex bounded model on [-length,0]. -/

def OAI.LittleFinitistic.BimoduleTotalPresentation.boundedNonpositivePowerIso line 71

Source documentation

Direct iterate transport for any same-complex bounded model on [-length,0].

def boundedNonpositivePowerIso (hlo : data.lower = -(length : ℤ)) (hhi : data.upper = 0)
    (r : ℕ) (Y : DerivedCategory (ModuleCat.{u} B)) :
    ((BimoduleComplexTensor.derivedTotal k B B P p hp).obj^[r]) Y ≅
      (data.derived.obj^[r]) Y :=
…

Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.derivedTotal