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

Open

momentAngle_exists_full_neighborly_twoComplex_blocks

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

algebraic-topologyhomologymoment-angle-complexestorsion

For integers $n\ge1$ and $k\ge0$ , put

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

There exist finite simplicial complexes $K$ on $s>3$ vertices and $L$ on $m>0$ vertices, and an injection $e:V(K)\hookrightarrow V(L)$ , such that $|L|$ is homeomorphic to $S^4$ , $K$ has dimension at most two and contains every edge between its vertices, and $e$ identifies $K$ with the full subcomplex of $L$ on $e(V(K))$ . Moreover,

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

Here fullness means that a set of vertices is a face of $K$ if and only if its image is a face of $L$ . This isolates the geometric realization problem from calculations involving moment-angle spaces and their loop spaces. It is a derived geometric lemma from the cited embedding and triangulation results, rather than a verbatim restatement of any one of them.

Formalization Note Face cardinality at most three expresses the dimension bound. The homology is integral singular homology of the existing 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_full_neighborly_twoComplex_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

Geometric consequence of Ryan Budney and Benjamin A. Burton, Embeddings of 3-manifolds in S^4, arXiv:0810.2346v6, Construction 2.8, p. 12 (https://arxiv.org/pdf/0810.2346v6); K. S. Sarkaria, On neighbourly triangulations, Trans. AMS 277 (1983), Neighbourliness Theorem for 3-Manifolds, p. 213 (https://www.kssarkaria.org/docs/On%20Neighbourly%20Triangulations.pdf); M. A. Armstrong, Extending triangulations, Proc. AMS 18 (1967), Theorem, pp. 701-702, doi:10.1090/S0002-9939-1967-0221513-2 (accessible thesis version: https://wrap.warwick.ac.uk/id/eprint/74313/1/WRAP_Thesis_Armstrong_1966.pdf, fourth paper, pp. 1-2). The additional step is relative stellar subdivision outside the two-skeleton. See the parent reduction explanation for the explicit surgery and homology argument.

View graph

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

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