OAI/GroupTheory/PolycyclicRecognition/Finiteness/CompleteVanishingExactFunctor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional resolutions after an exact coefficient functor

Only the images of countable free covers must have vanishing completion. The terminal projective is handled by its actual retract of a free cover.

  1. instance OAI.PolycyclicRecognition.normalizedFreeRepresentation_countable line 18
  2. instance OAI.PolycyclicRecognition.normalizedSyzygy_countable line 23
  3. theorem OAI.PolycyclicRecognition.shiftedCompleteCohomology_subsingleton_of_retract line 28
  4. theorem OAI.PolycyclicRecognition.exactFunctor_complete_vanishing_of_finite_dimension line 47

    Source documentation

    A finite projective-dimensional coefficient can be used without choosing finitely generated projectives, provided its countable free covers vanish.

    theorem exactFunctor_complete_vanishing_of_finite_dimension [Countable Q]
    (hfree : ∀ (B : Rep.{0} ℤ Q) [Countable B] (p : ℕ),
      Subsingleton (ShiftedCompletedCohomology p (F.obj (normalizedFreeRepresentation B))))
    (A : Rep.{0} ℤ Q) [Countable A] (d : ℕ)
    (hd : HasProjectiveDimensionLE A d) (p : ℕ) :
    Subsingleton (ShiftedCompletedCohomology p (F.obj A)) := by
…

    Mentions: OAI.PolycyclicRecognition.ShiftedCompletedCohomology, OAI.PolycyclicRecognition.normalizedFreeRepresentation