BimoduleAugmentationQuasiIso.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.shortExact_quasiIso_g line 16
Source documentation
An acyclic kernel in an actual short exact sequence makes the quotient map an isomorphism on homology.
```
theorem shortExact_quasiIso_g (S : ShortComplex (CochainComplex (ModuleCat.{u} B) ℤ))
    (hS : S.ShortExact) (hK : S.X₁.Acyclic) : QuasiIso S.g := by
…
```
theorem OAI.LittleFinitistic.BimoduleTotal.augmentation_epi line 33
Source documentation
The actual bimodule augmentation is an epimorphism of complexes.
```
theorem augmentation_epi : Epi res.augmentation := by
…
```
theorem OAI.LittleFinitistic.BimoduleTotal.augmentation_total_quasiIso line 44
Source documentation
Tensoring the actual bounded resolution augmentation with a complex of projective left modules gives a quasi-isomorphism of B-module complexes.
```
theorem augmentation_total_quasiIso (Z : CochainComplex (ModuleCat.{u} B) ℤ)
    [∀ q, Projective (Z.X q)] :
    QuasiIso (leftTotalMap res.augmentation Z res.data.degrees
      (intervalDegrees_strictMono res.data.lower res.data.upper)) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.leftTotalMap, OAI.LittleFinitistic.BimoduleTotal.intervalDegrees_strictMono