OAI/GroupTheory/PolycyclicRecognition/Finiteness/StableResolutionIdentity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The stable identity of a resolution syzygy

Maps factoring through projective representations form the image of a chosen projective cover. The identity is zero in that quotient precisely when the representation is projective. Applied to a resolution syzygy this detects finite integral cohomological dimension, without assuming any stable vanishing theorem.

  1. def OAI.PolycyclicRecognition.projectiveCoverMap line 21
  2. instance OAI.PolycyclicRecognition.projectiveCoverMap_epi line 24
  3. def OAI.PolycyclicRecognition.projectiveCoverPostcomp line 27
  4. def OAI.PolycyclicRecognition.projectiveFactorSubmodule line 33
  5. abbrev OAI.PolycyclicRecognition.StableRepresentationHom line 36
  6. def OAI.PolycyclicRecognition.stableRepresentationClass line 39
  7. theorem OAI.PolycyclicRecognition.stableRepresentationClass_eq_zero_iff_projective_factor line 43
  8. theorem OAI.PolycyclicRecognition.stableRepresentationIdentity_eq_zero_iff line 60
  9. theorem OAI.PolycyclicRecognition.stableRepresentationClass_eq_iff_projective_factor line 70
  10. theorem OAI.PolycyclicRecognition.resolution_dimension_of_opcycles_dimension line 77
  11. theorem OAI.PolycyclicRecognition.stableResolutionIdentity_eq_zero_iff_dimension line 93