BimoduleExactRows.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.tensorAcross_right_id line 14
Source documentation
The cross-variable tensor map with an identity input is the original bimodule map.
```
theorem tensorAcross_right_id {M M' : ModuleCat.{u} (Enveloping k B)}
    (f : M ⟶ M') (N : ModuleCat.{u} B) :
    tensorAcross f (𝟙 N) = BimoduleBalancedTensor.map k B (BalancedTensor.ScalarLeftModule k B N) f := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.tensorAcross, OAI.LittleFinitistic.BimoduleBalancedTensor.map, OAI.LittleFinitistic.BalancedTensor.ScalarLeftModule
theorem OAI.LittleFinitistic.BimoduleTotal.row_exact line 31
Source documentation
Every row of an acyclic bimodule complex tensored with a projective input term is exact.
```
theorem row_exact (a q : ℤ) :
    Function.Exact (tensorAcross (P.d (a-1) a) (𝟙 (Z.X q)))
      (tensorAcross (P.d a (a+1)) (𝟙 (Z.X q))) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.tensorAcross
theorem OAI.LittleFinitistic.BimoduleTotal.horizontal_exact line 46
Source documentation
The row exactness statement with precisely the transports occurring in the signed total.
```
theorem horizontal_exact (n a : ℤ) :
    Function.Exact
      (horizontalBetween k B P Z (n-1) n (a-1) a (by omega) (by omega))
      (horizontalBetween k B P Z n (n+1) a (a+1) rfl rfl) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.horizontalBetween