BimoduleFiniteRowsAcyclic.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.BimoduleTotal.closed_horizontal line 19
Source documentation
A closed total element whose higher coordinates vanish is closed in the next row.
```
theorem closed_horizontal (n a : ℤ) (x : TotalTerm k B P p Z n)
    (hx : ((total k B P p hp Z).d n (n+1)).hom x = 0)
    (hhigh : coefficient k B P Z p n (a+1) x = 0) :
    horizontalBetween k B P Z n (n+1) a (a+1) rfl rfl
      (coefficient k B P Z p n a x) = 0 := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.TotalTerm, OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.coefficient, OAI.LittleFinitistic.BimoduleTotal.horizontalBetween
theorem OAI.LittleFinitistic.BimoduleTotal.total_exact_of_rows line 38
Source documentation
Row-by-row elimination gives an actual preimage for every closed finite-total element.
```
theorem total_exact_of_rows (lo hi n : ℤ) (hlo : ∀ i, lo ≤ p i) (hhi : ∀ i, p i ≤ hi) :
    Function.Exact ((total k B P p hp Z).d (n-1) n).hom
      ((total k B P p hp Z).d n (n+1)).hom := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.total
theorem OAI.LittleFinitistic.BimoduleTotal.total_acyclic_of_rows line 101
Source documentation
A bounded acyclic bimodule complex tensors to an acyclic finite total with any complex of projective left modules. The full outside B-action is retained.
```
theorem total_acyclic_of_rows (lo hi : ℤ) (hlo : ∀ i, lo ≤ p i) (hhi : ∀ i, p i ≤ hi) :
    (total k B P p hp Z).Acyclic := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.total