First homology of a neighbourly $2$ -complex $|K|$ embeds in $H_{s+1}(\\Omega\\mathcal Z_K)$

Open

momentAngle_neighborlyTwoComplex_h1_selfLoopHomology

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

algebraic-topologyhomologyloop-spacesmoment-angle-complexes

Let $K$ be a finite abstract simplicial complex on $s>3$ vertices, of dimension at most two (every face has at most three vertices), whose one-skeleton is the complete graph on its vertices. Then there is an injective additive homomorphism

H_1(|K|;\mathbb Z)\hookrightarrow H_{s+1}(\Omega\mathcal Z_K;\mathbb Z),

where $\Omega\mathcal Z_K$ is the based loop space of the disk-circle moment-angle complex of $K$ at the all-ones point.

The mechanism is the desuspended loop space decomposition available for two-dimensional complexes together with the James construction: under the neighbourliness hypothesis the relevant wedge summand of $\Sigma\mathcal Z_K$ indexed by the full vertex set contributes $\Sigma^{s+1}|K|$ , and looping the corresponding suspension gives a copy of $H_1(|K|)$ in degree $s+1$ of the loop homology.

The statement is the special case $L=K$ of the corresponding statement for a full subcomplex of an ambient complex; the general case follows from it because a full subcomplex realizes $\Omega\mathcal Z_K$ as a retract of $\Omega\mathcal Z_L$ .

Formalization Note Face cardinality at most three expresses the dimension bound, all homology is integral singular homology, and the conclusion is an explicit injective additive homomorphism.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem momentAngle_neighborlyTwoComplex_h1_selfLoopHomology
    {s : ℕ} (hs : 3 < s) (K : AbstractSimplicialComplex (Fin s))
    (hdim : ∀ σ ∈ K, σ.card ≤ 3)
    (hneighborly : ∀ i j : Fin s, ({i, j} : Finset (Fin s)) ∈ K) :
    AdditivelyEmbeds (IntegralHomology 1 (GeometricRealization K))
      (IntegralHomology (s + 1) (BasedLoopSpace K)) := by sorry

Source

Derived from Lewis Stanton, Loop space decompositions of moment-angle complexes associated to two dimensional simplicial complexes, arXiv:2407.10781v2, Lemma 6.1 (https://arxiv.org/html/2407.10781v2#S6), citing the Iriye-Kishimoto neighbourliness criterion; I. M. James, Reduced Product Spaces, Annals of Mathematics 62 (1955), Sections 3-5.

View graph

First homology of a neighbourly 222-complex ∣K∣|K|∣K∣ embeds in Hs+1(OmegamathcalZK)H_{s+1}(\\Omega\\mathcal Z_K)Hs+1​(OmegamathcalZK​)

First homology of a neighbourly $2$ -complex $|K|$ embeds in $H_{s+1}(\\Omega\\mathcal Z_K)$