How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Finiteness is a geometric property of finitely generated groups
Statement
Finiteness is a geometric property of finitely generated groups.
Facts & Assumptions
Given: The hypotheses of the Statement.
A quasi-isometry invariant is a map on finitely generated groups constant on quasi-isometry classes, and a property is geometric when its indicator is such an invariant (Quasi-isometry invariants and geometric properties of finitely generated groups).
A finitely generated group is finite if and only if it is quasi-isometric to a one-point space (A finitely generated group is finite if and only if it is quasi-isometric to a point).
A finitely generated group is quasi-isometric to a metric space when its word metric for some, equivalently every, finite generating set is (The quasi-isometry type of a finitely generated group).
Being quasi-isometric is a reflexive, symmetric and transitive relation on metric spaces (Being quasi-isometric is reflexive, symmetric and transitive).
Proof
Two quasi-isometric finitely generated groups are simultaneously quasi-isometric to a point, by transitivity of the relation.
Being quasi-isometric to a point characterises finiteness, so the indicator of finiteness is a quasi-isometry invariant and finiteness is a geometric property.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- C. Loh, Geometric Group Theory: An Introduction (2015 course version), 264 pp. (standard reference, not scraped)
- C. Drutu and M. Kapovich, Geometric Group Theory (with an appendix by B. Nica), 837 pp. (standard reference, not scraped)