OAI/GroupTheory/PolycyclicRecognition/Algebra/CountableUnionDimension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integral dimension bounds for countable increasing unions

  1. theorem OAI.PolycyclicRecognition.projectiveDimension_of_cohomology_vanishing line 17
  2. theorem OAI.PolycyclicRecognition.cohomologicalDimension_le_of_exhaustion line 39

    Source documentation

    Countable unions cost at most one additional integral dimension.

    theorem cohomologicalDimension_le_of_exhaustion (S : ℕ → Subgroup G)
    (hS : Monotone S) (hcover : ∀ g, ∃ n, g ∈ S n) (d : ℕ)
    (hd : ∀ n, HasProjectiveDimensionLE (trivialIntegral (S n)) d) :
    HasProjectiveDimensionLE (trivialIntegral G) (d + 1) := by
…

    Mentions: OAI.PolycyclicRecognition.trivialIntegral

  3. theorem OAI.PolycyclicRecognition.exists_fg_subgroup_exhaustion line 54
  4. theorem OAI.PolycyclicRecognition.cohomologicalDimension_le_of_fg_subgroups line 71