SubgroupResolution.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Restricting integral resolutions to subgroups

Restriction is exact and preserves projectives. Truncating at a projective syzygy before restriction gives the cohomological-dimension bound for every subgroup, without a finite-generation hypothesis.

def OAI.PolycyclicRecognition.subgroupResolution line 22
Source documentation
Restrict an actual integral resolution, retaining its augmentation.
```
def subgroupResolution (P : ProjectiveResolution (trivialIntegral G)) :
    ProjectiveResolution (trivialIntegral H) :=
…
```
Mentions: OAI.PolycyclicRecognition.trivialIntegral
theorem OAI.PolycyclicRecognition.subgroup_cohomologicalDimension_le line 27
Source documentation
Integral cohomological dimension cannot increase on passing to a subgroup.
```
theorem subgroup_cohomologicalDimension_le (d : ℕ)
    [HasProjectiveDimensionLE (trivialIntegral G) d] :
    HasProjectiveDimensionLE (trivialIntegral H) d := by
…
```
Mentions: OAI.PolycyclicRecognition.trivialIntegral
theorem OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension.subgroup line 36