OrdinaryBimoduleAugmentationQuasiIso.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forget_bimoduleAugmentation line 12
Source documentation
The genuine augmentation becomes exactly the already verified right-module augmentation.
```
theorem forget_bimoduleAugmentation :
    (forgetBimoduleComplex k B l).hom ≫ augmentationMap k B l =
      ((forgetBimodule k B l).mapHomologicalComplex (.up ℕ)).map (bimoduleAugmentationMap k B l) ≫
        (forgetAugmentationTargetIso k B l).hom := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimoduleComplex, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentationMap, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetBimodule, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleAugmentationMap, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.forgetAugmentationTargetIso
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleAugmentationMap_quasiIso line 60
Source documentation
Actual augmentation quasi-isomorphism with its outside left B-action retained.
```
theorem bimoduleAugmentationMap_quasiIso : QuasiIso (bimoduleAugmentationMap k B l) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleAugmentationMap
def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleAugmentation line 72
Source documentation
The source's augmentation in degrees [-l,0], as a genuine bimodule map.
```
def integerBimoduleAugmentation : integerBimoduleComplex k B l ⟶
    (HomologicalComplex.single _ (.up ℤ) 0).obj (bimoduleTerminalObject k B l) :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleComplex, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.bimoduleTerminalObject
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleAugmentation_quasiIso line 78