CoarseGroupRingCohomology.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Coarse invariance of group-ring cohomology

The maps need not be homomorphisms. Their finite coarse errors provide the controlled prism homotopies, and hence inverse maps on group-ring cohomology.

def OAI.PolycyclicRecognition.GroupCoarseEquivalence.refl line 17
theorem OAI.PolycyclicRecognition.controlledCochainMap_refl line 25
def OAI.PolycyclicRecognition.controlledCochainHomotopyEquiv line 32
Source documentation
The coarse inverse produces inverse controlled cochain maps up to homotopy.
```
def controlledCochainHomotopyEquiv (e : GroupCoarseEquivalence G H) :
    HomotopyEquiv (controlledCochainComplex R G) (controlledCochainComplex R H) where
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochainComplex
def OAI.PolycyclicRecognition.controlledCohomologyIso line 46
Source documentation
Coarse-equivalent groups have isomorphic controlled scalar cohomology.
```
def controlledCohomologyIso (e : GroupCoarseEquivalence G H) (n : ℕ) :
    (controlledCochainComplex R G).homology n ≅ (controlledCochainComplex R H).homology n where
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochainComplex
def OAI.PolycyclicRecognition.coarseGroupRingCohomologyIso line 61
Source documentation
The group-ring case of coarse cohomology invariance, with the actual left regular representations and standard group cohomology.
```
def coarseGroupRingCohomologyIso (e : GroupCoarseEquivalence G H) (n : ℕ) :
    groupCohomology (Rep.leftRegular R G) n ≅ groupCohomology (Rep.leftRegular R H) n :=
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence