BimoduleStalkTotal.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.stalkTerm_isZero line 16
Source documentation
Every off-zero column of the stalk bimodule total is actually zero.
```
theorem stalkTerm_isZero (Z : CochainComplex (ModuleCat.{u} B) ℤ) (n : ℤ)
    (i : Fin l) (hi : i ≠ i₀) :
    IsZero (ModuleCat.of B (Term k B (bimoduleStalk k B X) Z (p i) (n + -(p i)))) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.BimoduleTotal.bimoduleStalk
def OAI.LittleFinitistic.BimoduleTotal.stalkTotalColumnIso line 24
Source documentation
Projecting onto its sole nonzero column is a genuine B-linear chain isomorphism.
```
def stalkTotalColumnIso (Z : CochainComplex (ModuleCat.{u} B) ℤ) :
    total k B (bimoduleStalk k B X) p hp Z ≅
      (columnFunctor k B (bimoduleStalk k B X) (p i₀)).obj Z :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.bimoduleStalk, OAI.LittleFinitistic.BimoduleTotal.columnFunctor
def OAI.LittleFinitistic.BimoduleTotal.stalkTotalColumnNatIso line 50
Source documentation
The stalk-total comparison is natural in the entire input complex.
```
def stalkTotalColumnNatIso : functor k B (bimoduleStalk k B X) p hp ≅
    columnFunctor k B (bimoduleStalk k B X) (p i₀) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.functor, OAI.LittleFinitistic.BimoduleTotal.bimoduleStalk, OAI.LittleFinitistic.BimoduleTotal.columnFunctor
def OAI.LittleFinitistic.BimoduleTotal.inputBimoduleIso line 70
Source documentation
An actual bimodule isomorphism induces a natural isomorphism of input tensor functors.
```
def inputBimoduleIso {M M' : ModuleCat.{u} (Enveloping k B)} (e : M ≅ M') :
    inputFunctor k B M ≅ inputFunctor k B M' :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.inputFunctor
def OAI.LittleFinitistic.BimoduleTotal.stalkTotalIso line 78
Source documentation
Finite total with the stalk bimodule is the ordinary tensor functor on all integer complexes. The only indexing condition is that degree zero is included.
```
def stalkTotalIso : functor k B (bimoduleStalk k B X) p hp ≅
    (inputFunctor k B X).mapHomologicalComplex (.up ℤ) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.functor, OAI.LittleFinitistic.BimoduleTotal.bimoduleStalk, OAI.LittleFinitistic.BimoduleTotal.inputFunctor