OrdinaryBimoduleTensorTotal.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.BimoduleComplexTensor.totalTerm line 14
def OAI.LittleFinitistic.BimoduleComplexTensor.forgetTotalEquiv line 16
def OAI.LittleFinitistic.BimoduleComplexTensor.entry line 21
Source documentation
The horizontal arrow map retains its left action and exact degree transport.
```
def entry (n : ℤ) (i j : Fin l) : term k S A Q Z (p i) (n + -(p i)) →ₗ[S]
    term k S A Q Z (p j) ((n+1) + -(p j)) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.term
def OAI.LittleFinitistic.BimoduleComplexTensor.differential line 27
Source documentation
The actual signed differential, now linear for the outside algebra.
```
def differential (n : ℤ) : totalTerm k S A Q Z p n →ₗ[S] totalTerm k S A Q Z p (n+1) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.totalTerm
theorem OAI.LittleFinitistic.BimoduleComplexTensor.forget_entry line 33
theorem OAI.LittleFinitistic.BimoduleComplexTensor.forget_differential line 44
Source documentation
Forgetting the outside action gives exactly the previously verified signed differential.
```
theorem forget_differential (n : ℤ) (z : totalTerm k S A Q Z p n) :
    forgetTotalEquiv k S A Q Z p (n+1) (differential k S A Q Z p n z) =
      (FiniteColumnComplex.totalDifferential (ComplexTensor.columns k A (rightComplex k S A Q) Z p)
        (ComplexTensor.tensorHorizontal k A (rightComplex k S A Q) Z p hp)).d n
        (forgetTotalEquiv k S A Q Z p n z) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.totalTerm, OAI.LittleFinitistic.BimoduleComplexTensor.forgetTotalEquiv, OAI.LittleFinitistic.BimoduleComplexTensor.differential, OAI.LittleFinitistic.FiniteColumnComplex.totalDifferential, OAI.LittleFinitistic.ComplexTensor.columns, OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex, OAI.LittleFinitistic.ComplexTensor.tensorHorizontal
theorem OAI.LittleFinitistic.BimoduleComplexTensor.differential_square line 74
def OAI.LittleFinitistic.BimoduleComplexTensor.total line 87
Source documentation
Actual signed finite tensor total in modules over the outside algebra.
```
def total : CochainComplex (ModuleCat.{u} S) ℤ :=
…
```