BimoduleAugmentedResolution.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.BimoduleTotal.bimoduleStalk line 12
structure OAI.LittleFinitistic.BimoduleTotal.AugmentedProjective line 17
Source documentation
Actual bounded right-projective resolution data, including the bimodule augmentation and its quasi-isomorphism; no tensor comparison is assumed.
```
structure AugmentedProjective (P : BiComplex k B) (X : ModuleCat.{u} (Enveloping k B)) where
…
```
def OAI.LittleFinitistic.BimoduleTotal.AugmentedProjective.tensorAugmentation line 27
Source documentation
The augmentation induces the concrete finite-total transformation.
```
def tensorAugmentation : functor k B P res.data.degrees
    (intervalDegrees_strictMono res.data.lower res.data.upper) ⟶
    functor k B (bimoduleStalk k B X) res.data.degrees
      (intervalDegrees_strictMono res.data.lower res.data.upper) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.functor, OAI.LittleFinitistic.BimoduleTotal.intervalDegrees_strictMono, OAI.LittleFinitistic.BimoduleTotal.bimoduleStalk
theorem OAI.LittleFinitistic.BimoduleTotal.AugmentedProjective.projectiveRow_quasiIso line 36
Source documentation
Each horizontal augmentation row is a B-linear quasi-isomorphism on a projective left-module input, including every term of the total bar.
```
theorem projectiveRow_quasiIso (N : ModuleCat.{u} B) [Projective N] :
    QuasiIso (((BimoduleBalancedTensor.functor k B
      (BalancedTensor.ScalarLeftModule k B N)).mapHomologicalComplex (.up ℤ)).map
        res.augmentation) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BalancedTensor.ScalarLeftModule
theorem OAI.LittleFinitistic.BimoduleTotal.AugmentedProjective.barRow_quasiIso line 47
Source documentation
In particular the actual resolution supplied by DerivedBar has all the projective rows needed for the remaining finite-total quasi-isomorphism proof.
```
theorem barRow_quasiIso (Z : ChainComplex (ModuleCat.{u} B) ℕ) (n : ℕ) :
    QuasiIso (((BimoduleBalancedTensor.functor k B
      (BalancedTensor.ScalarLeftModule k B ((DerivedBar.barTotal k B Z).X n))).mapHomologicalComplex
        (.up ℤ)).map res.augmentation) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.functor, OAI.LittleFinitistic.BalancedTensor.ScalarLeftModule, OAI.DerivedBar.barTotal