CohomologicalFiniteness.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The finiteness and duality properties used in recognition

These are concrete properties of the trivial integral representation and its projective resolutions. A finite classifying space supplies a finite resolution of this kind, but no predicate for an unspecified classifying space is used. The cohomology condition includes the possibly nontrivial orientation action: only the underlying integral module in top degree is required to be ℤ.

abbrev OAI.PolycyclicRecognition.trivialIntegral line 26
Source documentation
The trivial integral representation used to compute integral finiteness.
```
abbrev trivialIntegral : Rep ℤ G := Rep.trivial ℤ G ℤ
```
def OAI.PolycyclicRecognition.IntegralRepresentationFinite line 29
Source documentation
Finite generation refers to the group-ring action of the representation.
```
def IntegralRepresentationFinite (A : Rep ℤ G) : Prop :=
…
```
def OAI.PolycyclicRecognition.TypeFP line 34
Source documentation
Type FP_n(ℤ): a projective resolution finite over ℤ[G] through degree n.
```
def TypeFP (n : ℕ) : Prop :=
…
```
def OAI.PolycyclicRecognition.TypeFPInfinity line 39
Source documentation
Type FP_∞(ℤ) means type FP_n(ℤ) in every finite degree.
```
def TypeFPInfinity : Prop := ∀ n, TypeFP G n
```
Mentions: OAI.PolycyclicRecognition.TypeFP
def OAI.PolycyclicRecognition.HasFiniteProjectiveResolution line 42
Source documentation
A finite projective resolution, with all terms finite over the group ring.
```
def HasFiniteProjectiveResolution : Prop :=
…
```
def OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension line 49
Source documentation
Finite integral cohomological dimension is finite projective dimension of the trivial integral representation.
```
def HasFiniteIntegralCohomologicalDimension : Prop :=
…
```
def OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup line 53
Source documentation
Integral Poincaré duality in dimension n, allowing an orientation twist.
```
def IsIntegralPoincareDualityGroup (n : ℕ) : Prop :=
…
```
theorem OAI.PolycyclicRecognition.HasFiniteProjectiveResolution.typeFPInfinity line 58
theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.typeFPInfinity line 63
theorem OAI.PolycyclicRecognition.HasFiniteProjectiveResolution.finiteCohomologicalDimension line 69
Source documentation
The bounded resolution in the definition really implies finite cohomological dimension: every higher Ext cocycle has zero source.
```
theorem HasFiniteProjectiveResolution.finiteCohomologicalDimension
    (h : HasFiniteProjectiveResolution G) :
    HasFiniteIntegralCohomologicalDimension G := by
…
```
Mentions: OAI.PolycyclicRecognition.HasFiniteProjectiveResolution, OAI.PolycyclicRecognition.HasFiniteIntegralCohomologicalDimension
theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.finiteCohomologicalDimension line 81