BimoduleLeftNaturality.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.leftTotalMap_naturality line 15
Source documentation
Naturality of the actual bimodule-induced tensor map on arbitrary complexes.
```
theorem leftTotalMap_naturality (f : P ⟶ P') (g : Z ⟶ Z') :
    totalMap k B P p hp g ≫ leftTotalMap f Z' p hp =
      leftTotalMap f Z p hp ≫ totalMap k B P' p hp g := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.totalMap, OAI.LittleFinitistic.BimoduleTotal.leftTotalMap
def OAI.LittleFinitistic.BimoduleTotal.leftTensorNat line 45
Source documentation
An augmentation of bimodule complexes induces this concrete natural transformation.
```
def leftTensorNat (f : P ⟶ P') : functor k B P p hp ⟶ functor k B P' p hp where
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.functor
theorem OAI.LittleFinitistic.BimoduleTotal.leftTotalMap_id line 49
theorem OAI.LittleFinitistic.BimoduleTotal.leftTotalMap_comp line 60
def OAI.LittleFinitistic.BimoduleTotal.leftTensorFunctor line 77
Source documentation
The finite signed total is functorial in the genuine bimodule complex too.
```
def leftTensorFunctor : BiComplex k B ⥤
    (CochainComplex (ModuleCat.{u} B) ℤ ⥤ CochainComplex (ModuleCat.{u} B) ℤ) where
…
```