Finite generation for the local sphere: transfers and compactness

Source and verification

This article explains family 313 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

Morava localization isolates one chromatic height in stable homotopy theory. It also destroys connectivity: even the localized sphere has homotopy in arbitrarily negative degrees. Family 313 claims that each individual homotopy group nevertheless has a finite algebraic description over the $p$-adic integers. Its proof passes through continuous cohomology, countability on an open deformation stratum, and a compactness argument. (OpenAI, 2026)

🏷️ Preliminaries: localization and finite generation

A spectrum is the stable object representing a generalized cohomology theory. Its group ${\pi }_{j}X$ records maps from the sphere spectrum suspended $j$ times. The Moore spectrum $S/p$ is the cofiber of multiplication by $p$ on the sphere; write $X/p$ for the corresponding cofiber on any spectrum $X$.

At a prime $p$ and positive height $n$, Morava $K$-theory has coefficients ${\mathbb{F}}_p[v_n^{\pm 1}]$, with $|v_n|=2(p^n-1)$. The localization $L_{K(n)}X$ is universal among maps from $X$ to spectra that see only equivalences detected by this theory. Morava $E$-theory is a richer, even periodic theory with

$$\begin{array}{c}(E_n{)}_0=W({\mathbb{F}}_{p^n})[[u_1,\dots ,u_{n-1}]],\\ (E_n{)}_{\ast }=(E_n{)}_0[u^{\pm 1}],|u|=-2.\end{array}$$

Here $W({\mathbb{F}}_{p^n})$ is the unramified extension of ${\mathbb{Z}}_p$ with residue field ${\mathbb{F}}_{p^n}$. The parameters describe deformations of a height-$n$ formal group, a one-dimensional formal power-series group law. Its ordinary automorphism group is the compact $p$-adic group $P_n$; adjoining residue-field automorphisms gives the extended stabilizer ${\mathbb{G}}_n$.

A finitely generated ${\mathbb{Z}}_p$-module is a finite direct sum of copies of ${\mathbb{Z}}_p$ and finite cyclic $p$-groups. This is stronger than knowing its rational dimension or bounding the exponent of its torsion: an infinite product of copies of ${\mathbb{F}}_p$ has exponent $p$ but is not finitely generated.

Manuscript's degreewise finiteness theorem

For every prime $p$, every $n\ge 1$, and every integer $j$, the module ${\pi }_j{L}_{K(n)}{S}_p^{\wedge }$ is finitely generated over ${\mathbb{Z}}_p$. The same holds for ${\pi }_j{L}_{K(n)}F$ whenever $F$ is a finite $p$-local spectrum. No uniform bound on generators or torsion orders is asserted as these parameters vary. (OpenAI, 2026)

The restriction to finite spectra matters. The manuscript does not extend this conclusion to every dualizable or invertible object in the local category. It also does not compute chromatic fracture maps or prove a splitting of them.

🏷️ Continuous coefficients and the compactness principle

Continuous group cohomology is computed by functions $G^a\to M$ and the usual group-cochain differential. Here the topology on $M$ is essential. Compact deformation modules have their parameter-adic topology. For a localized module $M[1/x]$, a cochain must take values continuously in one lattice $x^{-b}M$ for some finite $b$. Thus each cochain has bounded denominators.

The principal coefficient claim is

$$\begin{array}{c}{H}_{\mathrm{cts}}^a(P_n,(E_n{)}_{2t}/p)\\ \text{is finite for }a\ge 0,t\in \mathbb{Z}.\end{array}$$

The proof needs a precisely delimited larger class: periodicity twists of functions on whole finite tuples of division points of the formal group, with specified powered coordinates, followed by finite sums, tensors, summands, and filtrations. It does not claim finiteness for arbitrary semilinear finite free modules. Whole division-point schemes are retained so that passing to a higher-height boundary keeps the coefficients in this class. (OpenAI, 2026)

There is a useful elementary bridge from countability to finiteness. A countable compact Hausdorff group is finite. Indeed, its singleton subsets are closed; Baire’s theorem makes one singleton have interior. Translations make every point open, and a compact discrete group is finite.

For compact coefficients, a resolution with finitely many generators in each degree makes cohomology compact Hausdorff: cycles are closed and boundaries are compact images. The resolution can be infinite in length. No finite cohomological dimension of the full stabilizer is assumed.

🏷️ Downward induction through the height strata

Over a sufficiently large finite field $k$, put

$$\begin{array}{c}{A}_m=k[[u_m,\dots ,u_{n-1}]],\\ A_n=k,x=u_m,\\ B_m=A_m[1/x](m<n).\end{array}$$

At $m=n$, the allowed coefficients are finite-dimensional over a finite field, so their cohomology is finite in every degree. Assume the result on the next boundary stratum $A_{m+1}$.

Every fixed strip $x^{a}M/x^{b}M$ then has finite cohomology. Its successive layers are next-height coefficients with the required conormal twists. The quotient $M[1/x]/M$ is a countable union of finite strips. Bounded-denominator cochains commute with this union, so its cohomology is countable.

The long exact sequence consequently makes both kernel and cokernel of

$$H^i(G,M)⟶H^i(G,M[1/x])$$

countable, where $G=P_n$. It remains to prove countability on the open stratum. Once that is known, $H^i(G,M)$ is both countable and compact Hausdorff, hence finite. This is why a countability theorem can close a finiteness induction.

Finite covers $B_U$ of $B_m$ mark the connected formal group and the étale Tate module, the compatible system of torsion points in the étale quotient. Crucially, the desired countability is at every sufficiently deep fixed finite marking level $U$. A result only on the completed infinite tower would not suffice for descent.

🏷️ Transfers, Laurent residues, and a finite intersection

The marked cover is an idempotent summand $B_U=e{A}^{\prime }[1/x]$ of a whole finite free model. The idempotent need not extend across $x=0$, so boundary estimates use $A^{\prime }$ before applying $e$.

The source constructs a normalized Cartier transfer $S$, an additive equivariant operator that divides Frobenius powers. For a fixed power $h_0$ of $p$, it has a pole estimate

$$S(x^{-D}{A}^{\prime })\subset x^{-\lceil D/h_0\rceil -c}{A}^{\prime }$$

with one constant $c$. Thus a sufficiently large lattice $\mathcal{P}=x^{-D_0}{A}^{\prime }$ is preserved by $S$, and repeated transfers eventually carry each bounded-pole family into it. Define

$$\begin{array}{c}{M}_U^i=H^i(G,\mathcal{P}),\\ X_U^i=H^i(G,B_U).\end{array}$$

The compact group $M_U^i$ admits a finite stable image

$$I_U^i=\bigcap _{a\ge 0}{S}^a{M}_U^i.$$

The underlying geometric input identifies the completed marked tower with independent tuples in a cohomology space on the Fargues–Fontaine curve, a curve organizing $p$-adic representations by vector bundles. A support calculation gives finite homology for a Laurent-series module. Its positive-order subspace is acyclic: a Baire argument makes the boundary subgroup open, while Frobenius contracts any cycle into that subgroup and acts invertibly on the relevant module. The residue quotient then identifies with a direct limit under the dual transfer. Compact duality yields finiteness of the stable image. These geometric and analytic constructions are substantial inputs, not consequences of compactness alone. (OpenAI, 2026)

Even here one must distinguish two objects. Duality first gives a finite inverse limit under $S$. Its projection surjects onto $I_U^i$ because nested compact sets supply compatible preimages. Equality with the inverse limit is not assumed in advance.

More importantly, a finite intersection of transfer images does not by itself bound all of $X_U^i$. A separate stabilization argument controls what can disappear between successive images. The source works modulo countable spaces while retaining the entire tail of fixed marking levels. It obtains, uniformly on a sufficiently deep tail, countability of

$$S^N{X}_U^i/S^{N+1}{X}_U^i.$$

The compact comparison identifies the actual intersection

$$F_U^i=\bigcap _{a\ge 0}\mathrm{im}(S^a{M}_U^i\to X_U^i)$$

with the finite image of $I_U^i$. It does not replace an algebraic image by its closure.

🏷️ One boundary operator for every high transfer

For $m>1$, the translation directions have distribution algebra $k[[D_1,\dots ,D_d]]$, where $d=(m-1)(n-m)$. Its Koszul resolution records the relations among these directions. If uncountable cohomology persisted on arbitrarily deep marking levels, choose the largest degree $b$ where it persists. The top Koszul operation gives a map from degree $b-d$ onto degree $b$, modulo a countable cokernel.

The key estimate retains one fixed finite extension diagram and one common marking subgroup for all high transfers. Write $\mathcal{B}$ for its cochain boundary operator. Its pole loss is bounded by one constant, independent of the transfer exponent.

Fix the root index $s$ and write $h_s=s^{m-1}$. The representative $w$ is a degree-$(b-d)$ cocycle with coefficients in $B_U^{1/h_s}$, the algebra obtained by adjoining the indicated Frobenius roots. For the allowed powers $q=q_0^a\ge s$, first include $w$ into the larger root coefficient algebra $B_U^{1/h}$, where $h=q^{m-1}$, and then take its $h$th power. This gives an ordinary $B_U$-valued cocycle. Up to a nonzero scalar, the operation is

$$\begin{array}{c}{e}_s[w]=c_{q,U}^{-1}{S}^a[\mathcal{B}(w^h)],\\ h=q^{m-1}.\end{array}$$

Modulo a countable quotient, source classes admit representatives of strictly positive $x$-order. Powering makes this order tend to infinity. It eventually absorbs the fixed loss of $\mathcal{B}$, so the bracketed cocycle lies in $\mathcal{P}$. Hence the same output class belongs to every sufficiently late compact transfer image and therefore to their finite intersection. The threshold may depend on $w$; uniformity over all cocycles is unnecessary.

The operation consequently has countable image and countable cokernel, contradicting the chosen uncountable target. When $m=1$, a split Frobenius–Cartier identity replaces this positive-dimensional Koszul argument. This supplies the required open-stratum countability.

Finally, finite marking descent uses the torsor’s Amitsur complex. A trace-one element provides a continuous contraction on the underlying coefficient complex; it need not be $G$-equivariant. The resulting double complex has finite total-degree diagonals. It preserves countability even when the finite covering group’s order is divisible by $p$, without averaging by that order. (OpenAI, 2026)

🏷️ From finite coefficients to integral homotopy

Passing from $P_n$ to ${\mathbb{G}}_n$ preserves degreewise coefficient finiteness by the finite-group extension spectral sequence. The Moore-spectrum descent spectral sequence is

$$\begin{array}{c}{H}_{\mathrm{cts}}^s({\mathbb{G}}_n,{\pi }_t(E_n/p))\\ ⟹{\pi }_{t-s}{L}_{K(n)}(S/p).\end{array}$$

Its second-page entries are finite. An imported descendability theorem supplies a horizontal vanishing line on a finite page: for some $R,N$, every $E_R^{s,t}$ with $s>N$ is zero. This is a later-page assertion, compatible with the stabilizer having $p$-torsion. Strong convergence leaves a finite filtration in each stem, so the abutment is finite. No additive extensions need to be computed for that conclusion.

Positive-height locality makes $X=L_{K(n)}S$ derived $p$-complete. The obstruction to $X\simeq {\mathrm{holim}}_{a}X/p^a$ is the mapping spectrum from $S[1/p]$, which vanishes because $S[1/p]$ is $K(n)$-acyclic.

Finiteness of every ${\pi }_j(X/p)$ implies finiteness of every ${\pi }_j(X/p^a)$ by cofiber sequences. An inverse system of finite groups has the Mittag–Leffler property even if its transition maps are not surjective. The adjacent Milnor ${\lim }^1$ vanishes, giving

$$M={\pi }_{j}X\cong \underset{a}{\underleftarrow{\lim }}{\pi }_j(X/p^a).$$

Thus $M$ is a compact pro-$p$ ${\mathbb{Z}}_p$-module. The cofiber exact sequence gives

$$\begin{array}{rl}0⟶M/pM& ⟶{\pi }_j(X/p)\\ & ⟶{\pi }_{j-1}X[p]⟶0.\end{array}$$

In particular $M/pM$ is finite. Choose finitely many lifts $a_i$ of generators of that quotient. Successively expanding a residual element modulo $p$ gives $p$-adic coefficients for an expression ${\sum }_i{c}_i{a}_i$. The remainder after $L$ expansions belongs to $p^{L}M$ and tends to zero uniformly: every fixed finite quotient of $M$ is annihilated by a power of $p$. This proves actual surjectivity ${\mathbb{Z}}_p^r\to M$, not merely density of its image. It is the compact Nakayama step, valid without connectivity.

🏷️ A height-one calculation and the scope of the result

At height one and odd $p$, the stabilizer is ${\mathbb{Z}}_p^{\times }$. First take invariants under its subgroup of order $p-1$; only weights $t$ divisible by $p-1$ remain. The residual group is generated topologically by $1+p$, and its cohomology is computed by the two-term operator $(1+p{)}^t-1$.

At weight zero this operator is zero, giving ${\mathbb{Z}}_p$ in degrees $0$ and $-1$. At any nonzero weight $t\in (p-1)\mathbb{Z}$, its valuation is $1+{\nu }_p(t)$, giving

$${\pi }_{2t-1}{L}_{K(1)}{S}_p^{\wedge }\cong \mathbb{Z}/p^{1+{\nu }_p(t)}.$$

All remaining groups vanish. This example includes negative weights and resolves the additive groups, rather than only an associated graded object.

At general height, an imported rational calculation determines the free ranks: they are the graded dimensions of an exterior algebra with generator degrees $-1,-3,\dots ,-(2n-1)$. The finiteness theorem supplies finite torsion groups in each degree, but does not determine their orders or multiplicities. The selected-source review here follows the coefficient-to-homotopy argument and the fixed-transfer mechanism; it does not independently reconstruct the complete tower geometry, Laurent analysis, or external descent theorems.

🏷️ Related posts

• Chromatic support and stabilizer orbits treats tensor-ideal classification; its dualizable-object setting is broader than the finite-spectrum finiteness assertion here.
• Smith–Toda complexes explains finite spectra that isolate chromatic layers; here finite spectra inherit degreewise finiteness after localization.

🏷️ Key steps and proof outlines

Recovering an actual intersection requires control of disappearing classes

Let $M$ be the compact cohomology group at one fixed marking level, $X$ its localized counterpart, $f:M\to X$ the comparison map, and $S$ the transfer. The source needs

$$\bigcap _{a}f(S^{a}M)=f\left(\bigcap _a{S}^{a}M\right).$$

This equality is not formal: representatives of a fixed localized class might vary with $a$, and an algebraic image need not be closed. The proof establishes enough finiteness before invoking compactness.

Fix $N\ge 1$ for which $S^{N}X/S^{N+1}X$ is countable, and put $A=S^{N}M$. The earlier comparison estimates make both the relevant comparison kernel and cokernel countable. They imply that $A/SA$ is countable. Since $SA$ is a compact image, it is closed; thus $A/SA$ is compact Hausdorff and consequently finite by Baire’s theorem.

The compact-operator lemma now gives finite generation of $A/I$ over the power-series ring in $S$, where $I={\bigcap }_a{S}^{a}M$, and finiteness of the locally $S$-nilpotent subgroup of $A$. To place $\ker (f{|}_A)$ inside that subgroup, take a representative cocycle that becomes a boundary after localization. Its primitive has some finite pole bound. Repeated transfer reduces that bound until the primitive lies in the preserved compact lattice. Applying the chain-map identity then shows that a sufficiently high power of $S$ kills the original class in $M$.

The required power may depend on the primitive. This is enough: the entire locally nilpotent subgroup is already finite. Hence $\ker (f{|}_A)$ is finite and closed. For a localized class $\xi$ in every transfer image, consider

$$E_a=\{v\in S^{a}A:f(v)=\xi \}.$$

These are nonempty nested finite closed sets in the compact space $A$. Their intersection supplies one representative in $I$ mapping to $\xi$. This proves the equality of actual intersections without assigning a Hausdorff topology to $X$ or replacing any image by its closure. (OpenAI, 2026)

A later-page vanishing line gives a finite filtration

After the coefficient theorem, each entry of the Moore-spectrum descent spectral sequence is finite. There can nevertheless be infinitely many entries along a fixed stem, so entrywise finiteness alone does not prove finite homotopy.

The imported descent theorem supplies a page $R$ and filtration bound $N$ with $E_R^{s,t}=0$ for $s>N$. On a fixed stem $j$, only the entries with $0\le s\le N$ and $t=j+s$ remain. Strong convergence supplies an exhaustive separated filtration on the abutment. Above $N$ its successive quotients vanish, so its tail is constant; separatedness forces that constant tail to be zero. The abutment is therefore a finite extension of finitely many finite groups.

This is compatible with nonzero group cohomology in arbitrarily high degrees on the second page. It uses a vanishing line after differentials have acted, rather than assuming finite cohomological dimension for the full stabilizer.

Compact Nakayama produces generators, not merely a dense subgroup

Derived completeness identifies

$$M={\pi }_{j}X\cong \underset{a}{\underleftarrow{\lim }}{\pi }_j(X/p^a).$$

The groups on the right are finite $p$-groups. The adjacent derived inverse limit vanishes because decreasing images in each finite target stabilize; surjectivity of every transition map is unnecessary.

The cofiber sequence shows $M/pM$ is finite. Choose lifts $a_1,\dots ,a_d$ of generators of that quotient. For any $z\in M$, recursively write

$$z_{\ell }=\sum _{i=1}^d{b}_{i,\ell }{a}_i+p{z}_{\ell +1},0\le b_{i,\ell }<p,z_0=z.$$

After $L$ steps the coefficients are finite base-$p$ sums and the remainder is $p^L{z}_L$. In every fixed finite target of the inverse limit, one power of $p$ kills the entire target. Thus the remainder tends to zero regardless of how $z_L$ varies. Passing to the convergent coefficients

$$c_i=\sum _{\ell \ge 0}{p}^{\ell }{b}_{i,\ell }\in {\mathbb{Z}}_p$$

gives the exact equality $z={\sum }_i{c}_i{a}_i$. Hence ${\mathbb{Z}}_p^d\to M$ is surjective. The conclusion is finite generation as a module, not just topological density. This proof works degree by degree, including negative degrees, and makes no connectivity assumption on the localized spectrum.

🏷️ Manuscripts and verification scope

• Finite generation for the K(n)-local sphere — pinned manuscript and companion source.

No family scope page was present at lean/docs/313.md in the pinned snapshot. This does not establish that all related formalization code is absent. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. Finite generation for the K(n)-local sphere.