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.
Under the ultrafilter lemma, abelian groups are amenable
Statement
Assume the ultrafilter lemma. Every abelian group is amenable.
Facts & Assumptions
Given: An abelian group and the ultrafilter lemma.
A finitely generated abelian group is isomorphic to with finite (The fundamental theorem of finitely generated abelian groups from PID modules).
Under the ultrafilter lemma, the Folner condition is equivalent to amenability (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).
Proof
Suppose first that is finitely generated. By [L1], write with finite. Let be finite and let . If , then is finite and satisfies for every , so the Folner condition is immediate. Assume now that . Transport across the isomorphism, and let be the maximum of the -norms of the -components of the transported elements. For , put . Then every translate by an element of changes only the -thick boundary layers of the box, so uniformly in , while . For large this gives for every . Thus finitely generated abelian groups satisfy the Folner condition.
By [L2], every finitely generated abelian group is therefore amenable.
Now let be arbitrary. Given a finite subset and , the subgroup is finitely generated and abelian, so step 2.1 makes it amenable. Applying [L2] inside yields a finite nonempty set with for every . The same set witnesses the Folner condition in . Since and were arbitrary, [L2] shows that every abelian group is amenable.
Depends on
Used by
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. Löh, Geometric Group Theory: An Introduction (2015 course version) (standard reference, not scraped)
- Cornelia Drutu and Michael Kapovich, Lectures on Geometric Group Theory (standard reference, not scraped)