BicomplexFilteredHomology.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The finite column filtration on actual total homology

A cycle with zero leading row class can be changed by an actual total boundary so that its support lies in fewer columns. This is the elementary filtration step used for finiteness, without identifying a nilpotent group's homology with the exterior algebra of its abelianization.

def OAI.PolycyclicRecognition.boundedTotalCycles line 22
Source documentation
Actual total cycles supported in columns strictly below p.
```
def boundedTotalCycles (n p : ℕ) :
    Submodule R ((K.total (ComplexShape.down ℕ)).cycles n) :=
…
```
theorem OAI.PolycyclicRecognition.mem_boundedTotalCycles line 28
theorem OAI.PolycyclicRecognition.boundedTotalCycles_support line 34
def OAI.PolycyclicRecognition.filteredTotalHomology line 40
Source documentation
The induced filtration on the homology of the given total complex.
```
def filteredTotalHomology (n p : ℕ) :
    Submodule R ((K.total (ComplexShape.down ℕ)).homology n) :=
…
```
theorem OAI.PolycyclicRecognition.totalCycles_isDiagonalCycle line 45
def OAI.PolycyclicRecognition.boundedTotalLeadingCycles line 53
Source documentation
The leading component as a map to the cycles in its row.
```
def boundedTotalLeadingCycles (n p j : ℕ) (h : p + j = n) :
    ModuleCat.of R (boundedTotalCycles K n (p + 1)) ⟶ (K.X p).cycles j := by
…
```
Mentions: OAI.PolycyclicRecognition.boundedTotalCycles
theorem OAI.PolycyclicRecognition.boundedTotalLeadingCycles_apply line 71
def OAI.PolycyclicRecognition.boundedTotalLeadingHomology line 88
Source documentation
The leading row's homology class.
```
def boundedTotalLeadingHomology (n p j : ℕ) (h : p + j = n) :
    boundedTotalCycles K n (p + 1) →ₗ[R] (K.X p).homology j :=
…
```
Mentions: OAI.PolycyclicRecognition.boundedTotalCycles
theorem OAI.PolycyclicRecognition.zero_leading_class_lowers_filtration line 92