CoarseEquivalence.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Coarse equivalences of discrete groups

Finite subsets are the bounded sets in a word metric on a finitely generated group. Controlling all finite sets of differences is the metric-free form of being bornologous. For finitely generated groups, a coarse equivalence in this sense is a quasi-isometry. It also matches the coarse-equivalence formulation of Li's finiteness and duality theorems.

def OAI.PolycyclicRecognition.GroupBornologous line 24
Source documentation
Uniform control of bounded differences, for the discrete group coarse structure.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:39 (same declaration text).
```
def GroupBornologous (f : G → H) : Prop :=
…
```
theorem OAI.PolycyclicRecognition.groupBornologous_hom line 28
theorem OAI.PolycyclicRecognition.GroupBornologous.comp line 33
structure OAI.PolycyclicRecognition.GroupCoarseEquivalence line 43
Source documentation
Coarse inverse maps with uniformly bounded errors, measured by finite sets of group differences.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:44 (same declaration text).
```
structure GroupCoarseEquivalence (G H : Type*) [Group G] [Group H] where
…
```
theorem OAI.PolycyclicRecognition.GroupCoarseEquivalence.finite_fiber line 55
Source documentation
Coarse inverses force finite fibers; this is the properness condition in the discrete-group definition of a coarse map.
```
theorem finite_fiber (e : GroupCoarseEquivalence G H) (y : H) :
    (e.toFun ⁻¹' {y}).Finite := by
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence
def OAI.PolycyclicRecognition.GroupCoarseEquivalence.symm line 64
theorem OAI.PolycyclicRecognition.GroupCoarseEquivalence.composite_error line 73
def OAI.PolycyclicRecognition.GroupCoarseEquivalence.trans line 86
theorem OAI.PolycyclicRecognition.finite_rightCosetRepresentatives line 99
theorem OAI.PolycyclicRecognition.groupBornologous_subgroupCoordinate line 107
def OAI.PolycyclicRecognition.finiteIndexCoarseEquivalence line 127
Source documentation
Finite-index subgroups are coarsely equivalent to their ambient groups. The coordinate map uses a finite right-coset transversal.
```
noncomputable def finiteIndexCoarseEquivalence (K : Subgroup G) [K.FiniteIndex] :
    GroupCoarseEquivalence K G where
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence