OAI/GroupTheory/PolycyclicRecognition/Finiteness/ProjectiveResolutionSyzygies.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Projectivity of the top syzygy

Successive quotient terms of a projective resolution fit into short exact sequences. Finite projective dimension therefore makes the corresponding top quotient projective; it remains finitely generated when the old term is.

  1. def OAI.PolycyclicRecognition.resolutionOpcyclesSequence line 17
  2. theorem OAI.PolycyclicRecognition.resolutionOpcyclesSequence_shortExact line 22
  3. def OAI.PolycyclicRecognition.resolutionOpcyclesZeroIso line 59
  4. theorem OAI.PolycyclicRecognition.resolutionOpcycles_projectiveDimension line 63
  5. theorem OAI.PolycyclicRecognition.resolutionOpcycles_projective line 79
  6. theorem OAI.PolycyclicRecognition.resolutionOpcycles_finite line 85