Uniform torsion blocks in a neighbourly two-complex inside a simplicial $4$ -sphere

Open

momentAngle_exists_neighborly_twoComplex_subcomplex_blocks

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

algebraic-topologyhomologymoment-angle-complexestorsion

For integers $n \ge 1$ and $k \ge 0$ put

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

The assertion is that there are finite simplicial complexes $K$ on $s > 3$ vertices and $L$ on $m > 0$ vertices and a vertex injection $e$ identifying $K$ with a subcomplex of $L$ , such that $|L|$ is homeomorphic to $S^4$ , every face of $K$ has at most three vertices, every pair of vertices of $K$ spans an edge of $K$ , and

G_{n,k} \hookrightarrow H_1(|K|;\mathbb Z).

Only the subcomplex relation is required here — a face of $L$ all of whose vertices come from $K$ need not be a face of $K$ . Fullness is a separate, purely piecewise-linear step, obtained afterwards by subdividing the ambient sphere away from $K$ .

A route to the statement is the one used in the source: perform zero-framed surgery on the split union of $k$ copies of the torus link $T(2,2n)$ and $k$ unknots, obtaining a closed three-manifold $M$ with $H_1(M;\mathbb Z) \cong \mathbb Z^k \oplus (\mathbb Z/n\mathbb Z)^{2k}$ , which contains $G_{n,k}$ ; both halves of the partitioned link are unlinks, hence slice, so $M$ embeds smoothly in $S^4$ . Give $M$ a two-neighbourly triangulation and extend the triangulation to the ambient sphere; the two-skeleton of that triangulation of $M$ has the same first homology as $M$ , has dimension two, and has a complete one-skeleton.

Formalization Note The bound on face cardinality expresses the dimension bound, homology is integral singular homology of the barycentric-coordinate realization, and the displayed inclusion means an injective additive homomorphism.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle DirectSum

Formal statement

theorem momentAngle_exists_neighborly_twoComplex_subcomplex_blocks
    (n k : ℕ) (hn : 0 < n) :
    ∃ (s : ℕ) (_hs : 3 < s) (m : ℕ) (_hm : 0 < m)
      (K : AbstractSimplicialComplex (Fin s))
      (L : AbstractSimplicialComplex (Fin m)) (e : Fin s ↪ Fin m),
      IsSimplicialFourSphere L ∧
      (∀ σ : Finset (Fin s), σ ∈ K → σ.map e ∈ L) ∧
      (∀ σ ∈ K, σ.card ≤ 3) ∧
      (∀ i j : Fin s, ({i, j} : Finset (Fin s)) ∈ K) ∧
      AdditivelyEmbeds ((Fin k →₀ ℤ) × (⨁ _ : Fin k, ZMod n))
        (IntegralHomology 1 (GeometricRealization K)) := by sorry

Source

Yang Han and Keke Li, Moment Angle Manifolds Corresponding to S^4 Whose Homology and Loop Homology May Have Arbitrary Torsion, IMRN 2026(4), rnag024, proof of Theorem 1.7; the ingredients are Ryan Budney and Benjamin A. Burton, Embeddings of 3-manifolds in S^4, arXiv:0810.2346v6, Construction 2.8, p. 12; K. S. Sarkaria, On neighbourly triangulations, Trans. AMS 277 (1983), Neighbourliness Theorem for 3-Manifolds, p. 213; M. A. Armstrong, Extending triangulations, Proc. AMS 18 (1967), pp. 701-704. This is the subcomplex form of the mission's geometric lemma momentAngle_exists_full_neighborly_twoComplex_blocks, with the fullness step separated off.

View graph

Uniform torsion blocks in a neighbourly two-complex inside a simplicial 444-sphere

Uniform torsion blocks in a neighbourly two-complex inside a simplicial $4$ -sphere