Coarse Spaces and the Švarc-Milnor Lemma

Stream: mathlib4

[Saif Ghobash]

Hello all,

I've been working on a geometric group theory library for Lean using a coarse spaces approach. You can find the repository here. The first milestone is complete: the Švarc-Milnor Lemma (~6,900 lines total and documented).

Coarse space recap

A coarse space is a collection of "controlled" entourages (subsets of X × X) that capture the notion of "bounded distance" without reference to a metric. One can think of an entourage as points with uniformly bounded distance (this analogy is explicit in the Metric/Basic.lean file where we define the basic controlled entourages as follows: E is controlled iff ∃ r : ℝ≥0, ∀ x y, (x, y) ∈ E → edist x y ≤ r). The axioms come in two flavors:
Metric axioms lifted to sets:

• The diagonal is controlled (points are close to themselves)

• Controlled sets are symmetric and closed under composition
  Bornology-like axioms:

• Subsets and finite unions of controlled sets are controlled

I created a general Entourage API for this, since Mathlib's existing SetRel infrastructure is better suited to uniform spaces as opposed to coarse spaces.

Two functions f g : α → X are close (notation f =ᶜ g) if the set {(f a, g a) | a : α} is controlled—i.e., they're uniformly within bounded distance of each other. A controlled map (standard terminology: bornologous) sends controlled sets to controlled sets (the analogue of being coarsely Lipschitz). A coarsely proper map has the property that preimages of coarsely bounded sets are coarsely bounded. A coarse map is both controlled and coarsely proper. A coarse equivalence is a pair of coarse maps that are mutually inverse up to closeness—this is the coarse analogue of quasi-isometry, but without explicit constants.

The formalization of coarse spaces is based on J. Roe, Lectures on Coarse Geometry, University Lecture Series 31, AMS, 2003

The coarse space approach

After a lot of experimenting, I settled on coarse spaces as the foundation rather than the traditional route via word metrics and quasi-isometries. A few advantages:

1. Canonical instance on groups. Different generating sets yield different (but quasi-isometric) word metrics, so one cannot place a single MetricSpace instance on a group. The coarse approach allows a single canonical CoarseSpace instance independent of generating set.

2. Avoiding the word metric. One goal of GGT is showing that under suitable geometric conditions, the word problem is decidable and distance becomes computable. If we construct a generic word metric it would need to be non computable to work over all groups. Furthermore, many groups already come with natural metrics that may or may not coincide with some word metric—forcing Švarc-Milnor through a word metric construction felt architecturally unclean.

3. Avoiding geodesics/length spaces. I don't know what use cases Mathlib needs these for or what the best architecture would be for future directions, so I avoided formalizing them.

Library structure

The library mirrors Mathlib's topology hierarchy (ignoring Entourage, QuasiIsometry, and ApproximateMidpoints files which ought to be moved elsewhere since they don't involve coarse spaces directly):

CoarseSpace/
├── Entourage/
│   └── Basic.lean            # Entourage API: composition (○), inverse, symmetrization
├── Defs.lean                 # CoarseSpace, IsControlled, Coarse, Controlled, CoarselyProper
├── Basic.lean                # Core lemmas and API
├── Order.lean                # Complete lattice of coarse structures, generateFrom
├── Constructions.lean        # Products, subspaces, induced/coinduced structures
├── Connected.lean            # Coarsely connected spaces
├── Finiteness.lean           # Finitely generated coarse spaces (FG)
├── CoarseEquiv/
│   ├── Defs.lean             # CoarseEquiv (≃ᶜ): refl, symm, trans
│   ├── Lemmas.lean           # Transferring coarse properties across coarse equivs
│   └── TransferInstance.lean # Transfer coarse structures across equivalences
├── QuasiIsometry.lean        # QuasiIsometryWith, QuasiIsometry, QuasiIsometryEquiv (≃qi)
├── ApproximateMidpoints.lean # HasCoarseMidpoints
├── CoarseSMul.lean           # Coarse group actions, coarse Švarc-Milnor (G ≃ᶜ X)
├── Group/
│   ├── Basic.lean            # Left-multiplication coarse structure on groups
│   ├── LeftInvariant.lean    # Left-invariant metrics ↔ coarse structures
│   └── SvarcMilnor.lean      # Full Švarc-Milnor theorem (G ≃qi X)
└── Metric/
    ├── Basic.lean            # Metric spaces as coarse spaces
    └── TransferQI.lean       # Coarse equivalence ↔ quasi-isometry bridge

The parallel with Mathlib.Topology:

• Defs / Basic — core definitions and API (cf. Topology.Basic)
• Order — (cf. Topology.Order)
• Constructions — products, subspaces, induced/coinduced (cf. Topology.Constructions)
• Connected — (cf. Topology.Connected)

Bridging coarse and metric worlds

While I didn't formalize the word metric, I did formalize quasi-isometries so one can pass back and forth between coarse equivalences and classical quasi-isometries (see Metric/TransferQI.lean):

• Quasi-isometry → Coarse equivalence: Always possible.
• Coarse equivalence → Quasi-isometry: Requires a purely metric condition: both spaces must have coarse midpoints.
  Coarse midpoints. A metric space has coarse midpoints if there exists a constant ε ≥ 0 such that for every pair of points x, y, there is a point m with

dist x m ≤ dist x y / 2 + ε
dist m y ≤ dist x y / 2 + ε

This is a coarse version of the approximate midpoint property in length spaces.

Statement of Švarc-Milnor

The proof proceeds in two stages:
1. Coarse Švarc-Milnor (see CoarseSMul.lean): If G acts on a coarse space X such that the action is uniformly controlled, coarse, and cocompact, then the orbit map is a coarse equivalence G ≃ᶜ X. This requires no metric assumptions, it's pure coarse geometry and based on the paper: N. Brodskiy, J. Dydak, A. Mitra, "Coarse structures and group actions" ( found here).
2. Classical Švarc-Milnor (see Group/SvarcMilnor.lean): The classical statement drops out as a corollary via the coarse-to-QI bridge. We add metric hypotheses to both sides:

• G has a PseudoMetricSpace structure with left-invariant metric (IsIsometricSMul G G)
• G is a ProperSpace with DiscreteTopology
• Both G and X satisfy HasCoarseMidpoints

Any word metric automatically satisfies these assumptions, so this formulation generalizes the classical statement.

Under these hypotheses, if G acts properly discontinuously, cocompactly, and by isometries on a proper metric space X, then the orbit map is a quasi-isometry equivalence G ≃qi X.

---

Is there interest in having coarse geometry infrastructure in Mathlib as the way to do GGT?

[Junyan Xu]

Not an expert myself but let me tag @Laurent Bartholdi, @Rémi Bottinelli, @Jim Fowler and @Georgi Kocharyan from previous work / discussions #new members > svarc-milnor @ 💬 and #new members > Word metric on group -- a new attempt @ 💬.

[Jireh Loreaux]

I would love to see coarse geometry in Mathlib, and reading your description above (without yet looking at the code), I think your approach makes sense. I would be happy to review PRs on this topic. I think @Anatole Dedecker might also be interested here.

[Saif Ghobash]

@Jireh Loreaux Wonderful! yes the coarse approach makes a lot of sense architecturally, and the nice thing is that growth, amenability etc can be phrased coarsely too. Other things like hyperbolic groups can just be phrased as the coarse structure on G is coarsely equivalent to a hyperbolic metric space and one can work "metrically" in that way, so not much needs to be added to the coarse space side. That way we're not just recreating the metric space library for coarse spaces.

As for PR's I'm glad you'd be willing to review, I tried to keep the code structure clean, readable, modular, and fitting mathlibs existing patterns to make it easier for review (along with following PR guidelines). There's just a few tweaks I am going to make tomorrow (some variables are implicit where it makes more sense to be explicit, so nothing major). As for actually submitting a PR, should it be staged? (Note: I've never submitted a PR, so not sure about how best to do so.)

Grouping as follows?

1. Quasi Isometries, approximate midpoint file as purely metric files, Entourage API since its standalone
2. Defs, Basic, Constructions, Order, Finiteness, Connected as the foundation for coarse spaces
3. CoarseEquiv files
4. Metric files for metric coarse structure and CoarseEquiv-QI bridge
5. CoarseSMul: Coarse Švarc-Milnor Lemma
6. Group files: Coarse structure on groups and classic Švarc-Milnor Lemma

[Jireh Loreaux]

Yes, you should definitely split it into small chunks. Especially for the early PRs, I want you to keep them as small as is reasonably possible (say <200 lines). You may find that despite your efforts to keep things up to Mathlib standards, there may still be lots of changes required to get it into Mathlib.

[Anatole Dedecker]

Thanks for tagging me Jireh, I am definitely interested. I am not working with coarse spaces directly but some of my colleagues do and I’ve long considered it might be a good formalization target. I’ll read this thread more carefully soon.

[Saif Ghobash]

@Jireh Loreaux Alright, I'll try to refactor into smaller chunks for the early PRs, I am opening to making changes, that's fine with me. Also for <200 lines are we counting documentation?

[Jireh Loreaux]

Yes, counting documentation. Sometimes we merge larger PRs, but I would never recommend that for a first-time contribution.

[Saif Ghobash]

Okay, thanks for letting me know, Ill get started working on the refactor for the PR tomorrow hopefully, will keep this thread updated.

[Anatole Dedecker]

I had a quick look at the code, this looks quite good! A few remarks that I would like to make:

1. I would have hoped to emphasize that coarse structures are to bornologies what uniform structures are to topologies. (EDIT: This turns out not to be so true, see below). In particular:

• Instead of your IsCoarselyBounded, CoarselyBoundedSpace and CoarselyProper definitions, I would expect an instance of CoarseSpace --> Bornology and the a use of bornological definitions
• Analogously to how our docs#Bornology is defined in terms of its filter at infinity, you could define a coarse structure on X as a filter on X × X corresponding to pairs of points which go further and further away from each other. The axioms then become that this filter is invariant under swapping coordinates, that eventually the two coordinates are different, and that if x and z go far away from each other, then either x and y or y and z do. While I'm not sure this should be taken as a definition (but I would at least consider it), I think some part of the API may be nice to see from this point of view.

2. I'm skeptical of your Entourage abbreviation, and I think Mathlib avoids this kind of "duplication for the sake of terminology". One thing I will say is, I think docs#SetRel.image and docs#SetRel.preimage should be called "left/right thickenings" instead, and we should have "left/right balls" for general SetRels.
3. There is currently an issue in your code because you have instances of CoarseSpace for both groups and metric spaces. However they have no reason to coincide (definitionally, or even propositionally) whenever you have a group with a distance, which is quite common. I would suggest removing the "Group --> CoarseSpace" instance in favor of a Prop-valued IsLeftCoarseGroup typeclss or something like this.
4. Related to the above, there is a question regarding forgetful inheritance (see docs#LibraryNote.forgetful_inheritance). I think CoarseSpace should extend Bornology in the same way UniformSpace extends TopologicalSpace. Should MetricSpace extend CoarseSpace instead of Bornology? Or should there be no MetricSpace --> CoarseSpace instance but an IsMetricCoarseSpace?

Sorry if this is a bit too much, I've been abstractly thinking about this for a while. For now I have to go but I'm happy to elaborate on anything tomorrow.

[Yaël Dillies]

Re point 2: see #33077

[Saif Ghobash]

@Anatole Dedecker Thanks for looking at the code! I actually did go for a bornology on X times X approach initially, it was a pain to work with (since you'd have a bornology on X times X and that itself induces a bornology on X via the coarsely bounded notions which then induces a bornology on the product via the existing instance in Mathlib, so you're juggling different bornologies).

Secondly it severely limits the class of coarse spaces one can actually talk about, indeed the standard definition is almost a bornology, and in fact induces a bornology on X precisely when X is coarsely connected. While I understand the appeal of working via filters which are arguably more Mathlib centric, I don't really know how (and if) it should be taken as the approach for coarse spaces.

I understand the skepticism on the entourage abbreviation, I'm open to changing it to work with set rels. I used the entourage version since I wanted to define entourage products as the standard product instance on entourages which is in fact already defined in the uniformity file via entourageProd, so it is mainly cosmetic. But again, I dont mind refactoring in favor of set rels.

I have instances for groups and metric spaces, and you're right there is no reason for them to coincide (they do in fact coincide for proper left invariant metrics that generate the discrete topology which is proved in the file Group/LeftInvariant.lean). I see your point however in that generically for groups with distances you'd get two different coarse structure instances, so it makes sense to have something like IsLeftCoarseGroup, IsMetricCoarseSpace.

I appreciate your comments :)

[Aaron Liu]

Saif Ghobash said:

Anatole Dedecker Thanks for looking at the code! I actually did go for a bornology on X times X approach initially, it was a pain to work with (since you'd have a bornology on X times X and that itself induces a bornology on X via the coarsely bounded notions which then induces a bornology on the product via the existing instance in Mathlib, so you're juggling different bornologies).

oh no don't implement is as a bornology on X times X

[Aaron Liu]

get a filter on X times X (the filter of cocontrolled sets) and have stuff in terms of that

[Anatole Dedecker]

Yes sorry, I was just in the process of realizing that coarse spaces do not actually induce a bornology on their own in general, I am too used to "nice" coarse spaces. Sorry for this, it is too late for me to think properly.

[Anatole Dedecker]

Bornology on X times X was not what I was suggesting, and indeed I would assume it to be very painful.

[Anatole Dedecker]

But I had not anticipated the fact that coarse => bornology was not automatic, I feel a bit stupid (I've told that "coarse/bornology is just like uniform/topology" story a few times, turns out I should have checked the axioms)...

[Saif Ghobash]

haha don't worry, I dont blame you for going that route, it definitely feels like it ought to be the case at least intuitively

[Saif Ghobash]

@Aaron Liu interesting, I'll see if I can work out the details via the filter axioms, and see if it makes life any easier

[Anatole Dedecker]

For anyone wondering, the issue is clear on the case of a coarse space with only subsets of the diagonal being controlled. Then any singleton is coarsely bounded but no two-element set is.

[Yaël Dillies]

I designed docs#SetRel to be used for entourages, so I don't see the point of the abbrev

[Anatole Dedecker]

Maybe we should call the usual notion of coarse spaces an ECoarseSpace and coarsely-connected ones CoarseSpaces? By analogy with EMetricSpace/MetricSpace? Just throwing the idea in case people like it.

[Saif Ghobash]

fair point, I don't think it would be too difficult to swap it out for SetRels

[Anatole Dedecker]

(Note that EMetricSpaces do not induce bornologies for the exact same reason: if two bounded sets are infinitely far from each other, their union is not bounded)

[Anatole Dedecker]

With that said, I have to go to bed.

[Saif Ghobash]

Coarse spaces: rewritten library + Švarc–Milnor lemma

I've rewritten my coarse geometry library from the ground up. The main changes:

• Everything is now built on a SetRel API, with the coarse space axioms stated filter-theoretically via a cocontrolled filter, directly mirroring Mathlib's uniformity.

• The Švarc–Milnor lemma is proved in a general coarse setting (~70 lines of code), then specialized to metric spaces. The key abstraction is uniformly controlled actions (generalizing isometric actions): rather than requiring a specific coarse structure on the group, we only ask that whatever structure it carries admits a uniformly controlled action on itself.

• The whole library is ~1,000 lines with module docs throughout (each file at most 200 lines). Quasi-isometries, monogenicity of coarse structures, connectedness, and approximate / coarse midpoints are saved for a later PR.

File structure:

ForMathlib/
  Data/Rel.lean
  Topology/MetricSpace/IsometricSMul.lean
CoarseSpace/
  Defs.lean
  Basic.lean
  CoarseEquiv/Defs.lean
  Algebra/UniformlyControlledSMul.lean
  Metric/Basic.lean
  Metric/SvarcMilnor.lean

I've also written a companion document walking through the design decisions and some proofs, intended to help reviewers: here

[Repo here] (https://github.com/koly777/GeometricGroupTheoryLean)

Feedback on the API design, naming, and overall approach is very welcome. Happy to split into PRs if reviewers have a preferred order.