BimoduleSingleDifferential.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.single_horizontal line 15
Source documentation
On the unique nonzero summands, the total differential becomes the original native tensor differential.
```
theorem single_horizontal (n m : ℤ) (h : n+1=m) :
    ModuleCat.ofHom (horizontalBetween k B P (singleInput B N) n m n m h h) ≫
      (singleTermIso k B P N m m rfl).hom =
    (singleTermIso k B P N n n rfl).hom ≫ (moduleEvaluation k B P N).d n m := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.horizontalBetween, OAI.LittleFinitistic.BimoduleTotal.singleInput, OAI.LittleFinitistic.BimoduleTotal.singleTermIso, OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation
theorem OAI.LittleFinitistic.BimoduleTotal.single_total_d line 43
theorem OAI.LittleFinitistic.BimoduleTotal.evaluationAtIndex_comm line 65
Source documentation
The degreewise comparison intertwines the full native differential at every pair of included consecutive degrees.
```
theorem evaluationAtIndex_comm (i j : Fin l) (h : p i+1=p j) :
    (evaluationAtIndex k B P N p hp i).hom ≫ (moduleEvaluation k B P N).d (p i) (p j) =
      (total k B P p hp (singleInput B N)).d (p i) (p j) ≫
        (evaluationAtIndex k B P N p hp j).hom := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.evaluationAtIndex, OAI.LittleFinitistic.BimoduleTotal.moduleEvaluation, OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.singleInput