we-solve (beta)

Math-1808 · mathematics · Group theory

Questions in Geometric Group Theory — Q 8.7

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Fix a prime $p$. The Prüfer group is the direct limit \[ C_{p^\infty}=\bigcup_{j\geq1}C_{p^j}, \] where the inclusion sends a generator of order $p^j$ to the $p$th power of a generator of order $p^{j+1}$. Equivalently, it is the multiplicative group of all complex roots of unity of $p$-power order, regarded as a discrete group.

A group $G$ is of type $\mathrm{FP}_n$ over $\mathbb Z$ if the trivial module $\mathbb Z$ has a projective $\mathbb ZG$-resolution whose terms in degrees $0,\ldots,n$ are finitely generated. Type $\mathrm{FP}_\infty$ requires this in every degree. Type $F_n$ means that $G$ has a classifying CW complex $K(G,1)$ with finite $n$-skeleton; its universal cover is contractible.

Can $C_{p^\infty}$ embed in a group of type $\mathrm{FP}_\infty$? Can it embed in a group of type $\mathrm{FP}_3$? Ask these for each prime $p$, allowing the target to depend on $p$.

The source also asks whether, for every integer $n\geq2$, every group of type $F_n$ embeds in some group of type $F_{n+1}$. All embeddings are injective abstract group homomorphisms. The ambient groups need not share the original group's dimension or torsion properties. Homological finiteness $\mathrm{FP}_n$ and geometric finiteness $F_n$ are explicitly different conditions; neither is silently substituted for the other in these three questions.

Short English statement

Can Prüfer groups embed in stronger homological finiteness classes, and can every $F_n$ group embed in an $F_{n+1}$ group?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-1808-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-1808

The universal group of type $F_\infty$ contains every finitely presented group, so it supplies the $F_{n+1}$ overgroup for each input of type $F_n$ with $n\ge2$. For a prime $p$, the Prüfer group has the recursive presentation $\langle c_1,c_2,\ldots\mid c_1^p=1,\ c_{i+1}^p=c_i\ (i\ge1)\rangle$. The source gives an HNN construction embedding a countably generated recursively presented group into a finitely generated recursively presented group. Applying that construction here and then Higman embedding places the Prüfer group in a finitely presented group, hence in the universal $F_\infty$ overgroup. Such an overgroup is of type $\mathrm{FP}_\infty$ and therefore $\mathrm{FP}_3$. These consequences cover every clause on this page. The simple-overgroup result has a decidability restriction and is not needed for these deductions.

Questions in Geometric Group Theory — Q 8.7

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: One group of type $F_\infty$ is claimed to contain every finitely presented group, with finitely generated subgroups exactly the recursively presented ones; A group with finitely many generators and a decidable identity-word test is claimed to embed into a nontrivial simple group of type $F_\infty$. Together they provide the following support within the scopes described below.

Mathematical statement of the claimed result

Result 1.
The claimed group $H$ has type $F_\infty$, meaning a classifying space with finite skeleton in every dimension, and satisfies \[ \forall G\text{ finitely presented},\qquad\exists\iota:G\hookrightarrow H. \] The corollary characterizes the finitely generated subgroups embeddable in this same $H$: \[ G\text{ finitely generated}:\qquad G\hookrightarrow H \quad\Longleftrightarrow\quad G\text{ recursively presented}. \] This does not assert embedding of every countable group.
Result 2.
Consider a group $G$ generated by finitely many elements, with an algorithm deciding its word problem. The assertion supplies a nontrivial simple group $H$ of type $F_\infty$ and an embedding \[ \iota:G\hookrightarrow H. \] Type $F_\infty$ requires finite skeleta of a classifying space in all dimensions. The decidability condition on $G$ is part of this theorem.
Consequences for the two embedding clauses.
If $n\ge2$, type $F_n$ implies finite presentation, so the claimed universal overgroup has type $F_{n+1}$. For each prime $p$, the presentation $C_{p^\infty}=\langle c_1,c_2,\ldots\mid c_1^p=1,\ c_{i+1}^p=c_i\ (i\ge1)\rangle$ is countable and recursive. The source's HNN construction compresses it to a finitely generated recursive presentation. Higman's theorem then gives a finitely presented overgroup, which the claimed universal theorem embeds into an $F_\infty$ group. In particular, the Prüfer group acquires an overgroup of type $\mathrm{FP}_\infty$, and thus of type $\mathrm{FP}_3$. These are deductions from the selected source claim and its stated embedding construction.

Outline of the argument

A universal finite presentation is inserted into faithful finite diagram envelopes using two systems of idempotents. An ascending-torus construction supplies uniform fillings with finitely many simplex types in each dimension, establishing the claimed higher finiteness of the universal envelope.

Encoded finite diagrams carry faithful actions with controlled stabilizers. A homological device for ascending tori provides fillings in every dimension, and stabilizers of finite type in a highly transitive action assemble the simple overgroup while retaining higher finiteness.

Formal verification

For family 250, the documented entries cover Boone--Higman equivalence, simple $F_\infty$ overgroups for decidable word problems, and one universal $F_\infty$ group. The converse characterization of all its recursively presented subgroups is extra manuscript scope. The listed Comparator files are BooneHigman.lean, SimpleOvergroups.lean, UniversalFInfinity.lean. Named declarations include OAI.UniversalFInfinity.universal_group_of_type_FInfinity. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →