BimoduleBarResolution.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.BimoduleTotal.integerTotalFunctor line 16
def OAI.LittleFinitistic.BimoduleTotal.barInputAugmentation line 20
Source documentation
The original bar augmentation, followed by the fixed finite bimodule total.
```
def barInputAugmentation : DerivedBar.barTotalFunctor k B ⋙ integerTotalFunctor data ⟶
    integerTotalFunctor data :=
…
```
Mentions: OAI.DerivedBar.barTotalFunctor, OAI.LittleFinitistic.BimoduleTotal.integerTotalFunctor
instance OAI.LittleFinitistic.BimoduleTotal.barInputAugmentation_isIso line 25
Source documentation
The left leg of the actual comparison zigzag is invertible for every chain input.
```
instance barInputAugmentation_isIso : IsIso (barInputAugmentation data) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.barInputAugmentation
def OAI.LittleFinitistic.BimoduleTotal.nativeBarResolutionIso line 42
Source documentation
The native derived tensor of the integer extension is computed on its genuine projective bar resolution, with no hypothesis on the input's terms.
```
def nativeBarResolutionIso : DerivedBar.integerQ B ⋙ data.derived ≅
    DerivedBar.barTotalFunctor k B ⋙ integerTotalFunctor data :=
…
```
Mentions: OAI.DerivedBar.integerQ, OAI.DerivedBar.barTotalFunctor, OAI.LittleFinitistic.BimoduleTotal.integerTotalFunctor
def OAI.LittleFinitistic.BimoduleTotal.nativeChainBarResolutionIso line 49
Source documentation
The same comparison written using the native chain-localization inclusion.
```
def nativeChainBarResolutionIso :
    DerivedBar.chainQ B ⋙ (DerivedBar.chainToIntegerDerived B ⋙ data.derived) ≅
      DerivedBar.barTotalFunctor k B ⋙ integerTotalFunctor data :=
…
```
Mentions: OAI.DerivedBar.chainQ, OAI.DerivedBar.chainToIntegerDerived, OAI.DerivedBar.barTotalFunctor, OAI.LittleFinitistic.BimoduleTotal.integerTotalFunctor