TotalBarResolution.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.barTotalSection line 21
Source documentation
Unit insertion is an actual additive chain section of the total augmentation.
```
def barTotalSection : Q ⟶ P where
…
```
def OAI.DerivedBar.barTotalHomotopy line 29
Source documentation
The explicit additive contraction, with its degree condition.
```
def barTotalHomotopy : Homotopy (𝟙 P) (π ≫ barTotalSection k A Z) where
…
```
Mentions: OAI.DerivedBar.barTotalSection
def OAI.DerivedBar.barTotalAdditiveEquiv line 48
Source documentation
The total augmentation is a homotopy equivalence after forgetting the A-action. The inverse and homotopy are explicit unit insertions, not A-linear splittings.
```
def barTotalAdditiveEquiv : HomotopyEquiv P Q where
…
```
instance OAI.DerivedBar.barTotalAugmentation_quasiIso line 59
Source documentation
The actual D-linear total-bar augmentation is a quasi-isomorphism for every nonnegative chain input; neither projectivity nor flatness of the input is assumed.
```
instance barTotalAugmentation_quasiIso : QuasiIso (barTotalAugmentation k A Z) := by
…
```
Mentions: OAI.DerivedBar.barTotalAugmentation
def OAI.DerivedBar.barTotalCochain line 65
Source documentation
The source's bounded-above cochain model is obtained by the literal n ↦ -n extension.
```
def barTotalCochain : CochainComplex (ModuleCat.{u} A) ℤ :=
…
```
instance OAI.DerivedBar.barTotalCochain_isKProjective line 69
Source documentation
The proved projective total terms make the cochain extension K-projective.
```
instance barTotalCochain_isKProjective : (barTotalCochain k A Z).IsKProjective := by
…
```
Mentions: OAI.DerivedBar.barTotalCochain