Arbitrary torsion in a moment-angle manifold over a simplicial $4$ -sphere, for the uniform block group $\mathbb{Z}^k \oplus (\mathbb{Z}/n)^k$

Open

momentAngle_fourSphere_uniformTorsionBlocks

by Gabewhigham · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algebraic-topologyhomologyloop-spacesmoment-angle-complexestorsion

Fix two natural numbers $n\ge 1$ and $k\ge 0$ , and consider the abelian group

G_{n,k}\;=\;\mathbb{Z}^{k}\;\oplus\;\bigl(\mathbb{Z}/n\mathbb{Z}\bigr)^{k}.

The assertion is that there exist a positive integer $m$ and an abstract simplicial complex $L$ on the vertex set $[m]$ whose geometric realization is homeomorphic to the unit sphere $S^4\subset\mathbb{R}^5$ , such that the associated moment-angle manifold

\mathcal{Z}_L=\bigcup_{\sigma\in L}\ \prod_{i=1}^{m} Y_i(\sigma), \qquad Y_i(\sigma)=\begin{cases} D^2, & i\in\sigma,\\ S^1, & i\notin\sigma,\end{cases}

admits injective additive homomorphisms

G_{n,k}\hookrightarrow H_*(\mathcal{Z}_L;\mathbb{Z}) \qquad\text{and}\qquad G_{n,k}\hookrightarrow H_*(\Omega\mathcal{Z}_L;\mathbb{Z}),

where $H_*$ denotes the direct sum of integral singular homology over all nonnegative degrees and $\Omega\mathcal{Z}_L$ is the based loop space at the all-ones point. One and the same $L$ must support both embeddings; the two need not land in the same degree, and no multiplicative structure is claimed.

This is the special case of the source's headline existence theorem in which the finitely generated abelian group is a uniform block group: $k$ free summands together with $k$ cyclic summands of one common modulus $n$ . It is the only shape of group that has to be realized topologically. Indeed, every group of the normal form $\mathbb{Z}^{r}\oplus\bigoplus_{i}\mathbb{Z}/p_i^{e_i}\mathbb{Z}$ embeds additively into $G_{n,k}$ for $n=\prod_i p_i^{e_i}$ and $k=\max(r,\#\{i\})$ , because $\mathbb{Z}/d\mathbb{Z}$ embeds into $\mathbb{Z}/n\mathbb{Z}$ whenever $d\mid n$ ; composing with such an embedding transports both conclusions. So a solver may work with two explicit numerical parameters instead of an abstract group, and the statement is exactly as strong as the general one.

Formalization Note The sphere condition is an actual homeomorphism between the barycentric-coordinate realization of $L$ and the Euclidean unit $4$ -sphere; the moment-angle space and its based loop space are concrete topological spaces; each subgroup claim is an explicit injective additive homomorphism into the direct sum of the integral singular homology groups. The hypothesis $0<n$ excludes the degenerate modulus $n=0$ , for which ZMod 0 is $\mathbb{Z}$ rather than a finite cyclic group.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

Formal statement

open MomentAngle DirectSum

theorem momentAngle_fourSphere_uniformTorsionBlocks (n k : ℕ) (hn : 0 < n) :
    ∃ (m : ℕ) (_hm : 0 < m) (L : AbstractSimplicialComplex (Fin m)),
      IsSimplicialFourSphere L ∧
        AdditivelyEmbeds ((Fin k →₀ ℤ) × (⨁ _ : Fin k, ZMod n))
          (TotalIntegralHomology (Complex L)) ∧
        AdditivelyEmbeds ((Fin k →₀ ℤ) × (⨁ _ : Fin k, ZMod n))
          (TotalIntegralHomology (BasedLoopSpace L)) := by sorry

Source

Yang Han and Keke Li, Moment Angle Manifolds Corresponding to S^4 Whose Homology and Loop Homology May Have Arbitrary Torsion, International Mathematics Research Notices 2026(4), rnag024, Theorem 1.7 on physical p. 3, https://doi.org/10.1093/imrn/rnag024. This is the instance of Theorem 1.7 for the finitely generated abelian group Z^k + (Z/n)^k; it is equivalent to Theorem 1.7, since every finitely generated abelian group embeds additively into such a group.

View graph

Arbitrary torsion in a moment-angle manifold over a simplicial 444-sphere, for the uniform block group Zk⊕(Z/n)k\mathbb{Z}^k \oplus (\mathbb{Z}/n)^kZk⊕(Z/n)k

Arbitrary torsion in a moment-angle manifold over a simplicial $4$ -sphere, for the uniform block group $\mathbb{Z}^k \oplus (\mathbb{Z}/n)^k$