A neighbourly two-complex in a four-sphere with the surgery presentation

Open

MomentAngleSurgery.exists_neighborly_twoComplex_cokernel

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algebraic-topologymoment-angle-complexessurgerytriangulation

Let $n\geq1$ and $k\geq0$ be integers. Set $A_k=(\mathbb Z^k)^3$ and $\Lambda_{n,k}(a,b,c)=(0,nc,nb)$ . There exist a finite simplicial complex $K$ on $s>3$ vertices, a finite simplicial complex $L$ on $m>0$ vertices, and a vertex injection 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 spans a face, and

H_1(|K|;\mathbb Z)\cong A_k/\operatorname{im}(\Lambda_{n,k}).

This is the geometric realization step for the explicit zero-surgery presentation. The subcomplex need not be full. The homology is actual integral singular homology of the barycentric-coordinate realization, and the displayed identification is an additive group isomorphism. Its algebraic cokernel computation is a separate theorem.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces
import Definitions.Def_MomentAngle_surgery_blocks

open MomentAngle MomentAngleSurgery

Formal statement

theorem MomentAngleSurgery.exists_neighborly_twoComplex_cokernel
    (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) ∧
      Nonempty (Cokernel n k ≃+ IntegralHomology 1 (GeometricRealization K)) := by sorry

Source

Geometric combination of Budney–Burton, arXiv:0810.2346v6, Construction 2.8, printed p. 12 (zero-surgery on a union of two slice sublinks embeds in S4), https://arxiv.org/pdf/0810.2346v6 ; Sarkaria, On neighbourly triangulations, Trans. AMS 277 (1983), Neighbourliness Theorem for 3-Manifolds, printed p. 213 (connected closed 3-manifolds have neighbourly triangulations with arbitrarily many sufficiently large numbers of vertices), https://www.kssarkaria.org/docs/On%20Neighbourly%20Triangulations.pdf ; Armstrong, Extending triangulations, Proc. AMS 18 (1967), pp. 701-704, DOI 10.1090/S0002-9939-1967-0221513-2 (relative PL triangulation). Use the split union of k copies of T(2,2n) and k unknots, all framings zero; each half is an unlink. The presentation matrix is Lambda(n,k); see Calegari, Chapter 6: Floer Theories, Section 1.1.4, Lemma 1.5, p. 4, https://math.uchicago.edu/~dannyc/courses/heegaard_2020/floer_theory_notes.pdf . Passing to the two-skeleton preserves first homology. This is the presentation-group form of the geometric step used for Han–Li, IMRN 2026(4), rnag024, Theorem 1.7; it is a derived combination of these ingredients.

View graph