First homology of $|K|$ embeds in $H_{s+2}(\\mathcal Z_K)$

Open

momentAngle_h1_selfComplex_topSummand

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

algebraic-topologyhomologymoment-angle-complexes

Let $K$ be a finite abstract simplicial complex on $s>0$ vertices. Then there is an injective additive homomorphism

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

where $|K|$ is the barycentric-coordinate geometric realization and $\mathcal Z_K$ the disk-circle moment-angle complex on the same vertex set.

This is the summand of the polyhedral-product suspension splitting indexed by the full vertex set: the splitting expresses $\Sigma\mathcal Z_K$ as a wedge over subsets $\sigma$ of the vertex set of the suspensions $\Sigma^{|\sigma|+1}|K_\sigma|$ , and taking $\sigma$ to be all $s$ vertices, so that $K_\sigma=K$ , contributes $H_1(|K|)$ to $H_{1+s+1}(\mathcal Z_K)$ .

No hypotheses beyond $s>0$ are imposed on $K$ . 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 $\mathcal Z_K$ as a retract of $\mathcal Z_L$ .

Formalization Note All homology is integral singular homology, and the conclusion is an explicit injective additive homomorphism in the stated degrees.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem momentAngle_h1_selfComplex_topSummand
    {s : ℕ} (hs : 0 < s) (K : AbstractSimplicialComplex (Fin s)) :
    AdditivelyEmbeds (IntegralHomology 1 (GeometricRealization K))
      (IntegralHomology (s + 2) (Complex K)) := by sorry

Source

Bahri-Bendersky-Cohen-Gitler, The polyhedral product functor, Advances in Mathematics 225 (2010), Theorem 2.21; stated explicitly as Proposition 2.5 in Lewis Stanton, arXiv:2407.10781v2 (https://arxiv.org/html/2407.10781v2#S2.SS2). Take the summand indexed by the full vertex set, of cardinality s; the suspension splitting gives degree s+2 before suspension.

View graph

First homology of ∣K∣|K|∣K∣ embeds in Hs+2(mathcalZK)H_{s+2}(\\mathcal Z_K)Hs+2​(mathcalZK​)

First homology of $|K|$ embeds in $H_{s+2}(\\mathcal Z_K)$