BimoduleBarComparisonIso.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.LittleFinitistic.BimoduleTotal.resolvedTensorAugmentation_isIso line 19
Source documentation
The original augmentation, evaluated on the actual free bar resolution, becomes an isomorphism in the integer derived category.
```
instance resolvedTensorAugmentation_isIso : IsIso
    (whiskerLeft (DerivedBar.barTotalFunctor k B)
      (whiskerLeft (DerivedBar.integerExtension B)
        (whiskerRight res.tensorAugmentation DerivedCategory.Q))) := by
…
```
Mentions: OAI.DerivedBar.barTotalFunctor, OAI.DerivedBar.integerExtension
instance OAI.LittleFinitistic.BimoduleTotal.augmentationComparisonOnChains_isIso line 37
def OAI.LittleFinitistic.BimoduleTotal.nativeBarIso line 45
Source documentation
Natural identification of the native D(B-Mod) tensor by the actual bounded right-projective bimodule resolution and DerivedBar's genuine localized tensor, after chainToIntegerDerived. Both outside module actions are retained.
```
def nativeBarIso :
    DerivedBar.chainToIntegerDerived B ⋙ res.data.derived ≅
      DerivedBar.derivedTensor k B (barModule (X := X)) ⋙ DerivedBar.chainToIntegerDerived B :=
…
```
Mentions: OAI.DerivedBar.chainToIntegerDerived, OAI.DerivedBar.derivedTensor, OAI.LittleFinitistic.BimoduleTotal.barModule
theorem OAI.LittleFinitistic.BimoduleTotal.nativeBarIso_hom line 53
Source documentation
This isomorphism uses precisely the original augmentation-induced map.
```
theorem nativeBarIso_hom : (nativeBarIso res i₀ hi₀).hom = augmentationComparison res i₀ hi₀ := rfl
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.nativeBarIso, OAI.LittleFinitistic.BimoduleTotal.augmentationComparison