FiniteDimensionCohomology.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Cohomology above the integral dimension bound

The bound applies to every coefficient representation. In particular the periodic cohomology of a nontrivial finite cyclic group rules out finite integral cohomological dimension.

theorem OAI.PolycyclicRecognition.groupCohomology_isZero_above_dimension line 22
theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.dimension_le line 38
Source documentation
A nonzero dualizing module cannot occur above the cohomological dimension.
```
theorem IsIntegralPoincareDualityGroup.dimension_le [Group G] {n d : ℕ}
    (hG : IsIntegralPoincareDualityGroup G n)
    [HasProjectiveDimensionLE (trivialIntegral G) d] : n ≤ d := by
…
```
Mentions: OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup, OAI.PolycyclicRecognition.trivialIntegral
theorem OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension.bounds_duality_subgroups line 50
Source documentation
One finite dimension bound controls every duality subgroup.
```
theorem HasFiniteIntegralCohomologicalDimension.bounds_duality_subgroups [Group G]
    (hG : HasFiniteIntegralCohomologicalDimension G) :
    ∃ d : ℕ, ∀ (H : Subgroup G) (n : ℕ), IsIntegralPoincareDualityGroup H n → n ≤ d := by
…
```
Mentions: OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension, OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup
theorem OAI.PolycyclicRecognition.finiteCyclic_even_cohomology_not_isZero line 65
Source documentation
The class of one in positive even integral cohomology is nonzero whenever there is more than one group element.
```
theorem finiteCyclic_even_cohomology_not_isZero (hG : 1 < Fintype.card G)
    (i : ℕ) [NeZero i] (hi : Even i) :
    ¬ IsZero (groupCohomology (trivialIntegral G) i) := by
…
```
Mentions: OAI.PolycyclicRecognition.trivialIntegral