OAI/GroupTheory/PolycyclicRecognition/Finiteness/FiniteProjectivePresentations.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite projective covers of finitely generated representations

  1. structure OAI.PolycyclicRecognition.FiniteIntegralProjectivePresentation line 14
  2. theorem OAI.PolycyclicRecognition.finiteIntegralFreeCover_exists line 18
  3. theorem OAI.PolycyclicRecognition.finiteIntegralProjectivePresentation_exists line 51
  4. def OAI.PolycyclicRecognition.chosenIntegralPresentation line 64

    Source documentation

    A projective presentation chosen with finite source whenever the target is finitely generated. The finiteness proof stays inside the chosen object.

    def chosenIntegralPresentation (A : Rep.{0} ℤ G) : ProjectivePresentation A := by
…
  5. theorem OAI.PolycyclicRecognition.chosenIntegralPresentation_finite line 70