Theorem 1.7 — Arbitrary torsion in moment-angle and loop-space homology

Open

momentAngle_arbitrary_torsion

by ShouqiaoWang · Aug 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algebraic-topologyhomologyloop-spacesmoment-angle-complexestorsion

Let $G$ be a finitely generated abelian group. Prove that there exist a natural number $m$ and an abstract simplicial complex $L$ on Fin m whose geometric realization is homeomorphic to the unit sphere $S^4\subset\mathbb R^5$ , such that the same moment-angle space $\mathcal Z_L$ admits injective additive homomorphisms

G\hookrightarrow H_*(\mathcal Z_L;\mathbb Z) \quad\text{and}\quad G\hookrightarrow H_*(\Omega\mathcal Z_L;\mathbb Z).

Here $\mathcal Z_L$ is the union, over faces $\sigma$ of $L$ , of coordinate products having a disk $D^2$ in the coordinates of $\sigma$ and a circle $S^1$ elsewhere. The loop space is based at the all-ones point, and $H_*$ denotes the direct sum of integral singular homology over all nonnegative degrees.

The same simplicial $4$ -sphere must witness both embeddings. The claim concerns additive subgroups; the embeddings need not occupy the same homological degree or preserve a graded ring structure.

Formalization Note The sphere condition is an actual homeomorphism, the moment-angle and loop spaces are concrete topological spaces, and the two subgroup claims are explicit injective additive homomorphisms.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

Formal statement

open MomentAngle

theorem momentAngle_arbitrary_torsion
    (G : Type) [AddCommGroup G] [Module.Finite ℤ G] :
    ∃ (m : ℕ) (_hm : 0 < m) (L : AbstractSimplicialComplex (Fin m)),
      IsSimplicialFourSphere L ∧
        AdditivelyEmbeds G (TotalIntegralHomology (Complex L)) ∧
        AdditivelyEmbeds G (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

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

For every type $G$ carrying an abelian-group structure whose canonical $\mathbb Z$ -module is finitely generated, there exist a natural number $m$ with $m>0$ and an abstract simplicial complex $L$ on $\operatorname{Fin}(m)$ such that: the subtype of nonnegative real coordinate functions on $\operatorname{Fin}(m)$ having total sum $1$ and support a face of $L$ is homeomorphic to the unit sphere in $\mathbb R^5$ ; there is an injective addition-and-zero-preserving map from $G$ into the direct sum over all nonnegative degrees of the integral singular-homology groups of the subtype of functions $z:\operatorname{Fin}(m)\to\mathbb C$ for which some empty-or- $L$ -face $\sigma$ contains every coordinate allowed to have modulus at most $1$ , while every coordinate outside $\sigma$ has modulus exactly $1$ ; and there is also an injective addition-and-zero-preserving map from $G$ into the analogous total integral singular homology of the space of parametrized continuous loops in that same subtype based at the all-ones point. The same $m$ and $L$ serve both embeddings, but the two injective maps need not be related. The embeddings may use multiple homological degrees and need not split. The statement does not itself assert that the moment-angle subtype is a manifold.

Human review

Endorsed by Shuze Chen · Aug 27, 2026
Endorsed by ShouqiaoWang · Aug 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph