OAI/GroupTheory/PolycyclicRecognition/Finiteness/BicomplexSecondPageCycles.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Leading classes are cycles on the second page

The cycle equation in the adjacent column makes the leading row-homology class a horizontal cycle. All maps below use actual homology objects.

  1. abbrev OAI.PolycyclicRecognition.rowHomologyComplex line 18
  2. theorem OAI.PolycyclicRecognition.boundedTotalLeadingHomology_isCycle line 22
  3. def OAI.PolycyclicRecognition.boundedTotalSecondPageCycles line 63

    Source documentation

    Leading total cycles mapped into the cycles of the first-page complex.

    def boundedTotalSecondPageCycles (n p j : ℕ) (h : p + j = n) :
    ModuleCat.of R (boundedTotalCycles K n (p + 1)) ⟶
      (rowHomologyComplex K j).cycles p := by
…

    Mentions: OAI.PolycyclicRecognition.boundedTotalCycles, OAI.PolycyclicRecognition.rowHomologyComplex

  4. theorem OAI.PolycyclicRecognition.boundedTotalSecondPageCycles_apply line 77
  5. def OAI.PolycyclicRecognition.boundedTotalSecondPageClass line 88