OAI/GroupTheory/PolycyclicRecognition/Finiteness/CompleteCohomologyConnecting.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Connecting maps for the completed coefficient theory

The kernel map of a projective cover and the syzygy dimension equivalence give connecting maps for every short exact coefficient sequence. Naturality holds because different choices of projective lift have the same stable map.

  1. def OAI.PolycyclicRecognition.shiftedCompleteBoundary line 18
  2. theorem OAI.PolycyclicRecognition.shiftedCompleteBoundary_apply line 23
  3. theorem OAI.PolycyclicRecognition.shiftedCompleteBoundary_natural line 29
  4. theorem OAI.PolycyclicRecognition.shiftedCompleteBoundary_comp_f line 38
  5. theorem OAI.PolycyclicRecognition.shiftedCompleteBoundary_g_comp line 46
  6. theorem OAI.PolycyclicRecognition.shiftedCompleteBoundary_zero_of_section line 55
  7. theorem OAI.PolycyclicRecognition.shiftedCompleteBoundary_bijective_of_projective line 65