First homology of a full neighbourly two-complex embeds in loop homology

Open

momentAngle_fullNeighborlyTwoComplex_h1_loopHomology

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

algebraic-topologyhomologymoment-angle-complexestorsion

Let $K$ be a finite simplicial complex on $s>3$ vertices, of dimension at most two, whose one-skeleton is the complete graph. Let $L$ be a finite simplicial complex, and suppose a vertex injection identifies $K$ with a full subcomplex of $L$ . Then there exists an injective additive homomorphism

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

The loop space is based at the all-ones point of the disk-circle moment-angle space. This is a homological consequence of the desuspended polyhedral-product splitting and the James construction, together with the retraction associated to a full subcomplex. The dimension and complete-graph hypotheses apply to $K$ ; no such restrictions are imposed on $L$ .

Formalization Note All homology is integral singular homology. The conclusion is an additive embedding in the specified degree; it makes no ring-embedding assertion.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem momentAngle_fullNeighborlyTwoComplex_h1_loopHomology
    {s m : ℕ} (hs : 3 < s)
    (K : AbstractSimplicialComplex (Fin s))
    (L : AbstractSimplicialComplex (Fin m)) (e : Fin s ↪ Fin m)
    (hfull : ∀ σ : Finset (Fin s), σ ∈ K ↔ σ.map e ∈ L)
    (hdim : ∀ σ ∈ K, σ.card ≤ 3)
    (hneighborly : ∀ i j : Fin s, ({i, j} : Finset (Fin s)) ∈ K) :
    AdditivelyEmbeds (IntegralHomology 1 (GeometricRealization K))
      (IntegralHomology (s + 1) (BasedLoopSpace L)) := 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, especially Theorem (4.1) and the canonical-map theorems (https://webhomes.maths.ed.ac.uk/~v1ranick/papers/jamesred.pdf). The full-subcomplex coordinate inclusion has a pointed retraction. For the same mechanism, see Stanton-Vylegzhanin, arXiv:2506.15573v2, proof of Proposition 4.16 (https://arxiv.org/html/2506.15573v2#S4.SS5).

View graph