ControlledGroupCohomology.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Controlled cochains compute group-ring cohomology

Coefficient extraction identifies the whole controlled complex with the Hom complex of the standard projective resolution, including its differential.

theorem OAI.PolycyclicRecognition.homogeneousGroupRingLinear_coboundary line 18
theorem OAI.PolycyclicRecognition.homogeneousRepresentationCochain_coboundary line 27
def OAI.PolycyclicRecognition.controlledStandardCochainIso line 38
Source documentation
The controlled complex is the actual standard-resolution cochain complex.
```
def controlledStandardCochainIso :
    controlledCochainComplex R G ≅
      (Rep.standardComplex R G).linearYonedaObj R (Rep.leftRegular R G) :=
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochainComplex
def OAI.PolycyclicRecognition.controlledGroupCohomologyIso line 54
Source documentation
Controlled scalar homogeneous cohomology is group-ring cohomology.
```
def controlledGroupCohomologyIso (n : ℕ) :
    (controlledCochainComplex R G).homology n ≅
      groupCohomology (Rep.leftRegular R G) n :=
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochainComplex