First homology of a full subcomplex embeds in moment-angle homology

Open

momentAngle_fullSubcomplex_h1_homology

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

algebraic-topologyhomologymoment-angle-complexestorsion

Let $K$ and $L$ be finite simplicial complexes, with $K$ on $s>0$ vertices. Suppose an injection $e:V(K)\hookrightarrow V(L)$ identifies $K$ with a full subcomplex of $L$ . Then there exists an injective additive homomorphism

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

The moment-angle space uses the disk-circle pair $(D^2,S^1)$ . No sphere, dimension, or neighbourliness hypothesis is imposed on either complex. This is the first-homology summand supplied by the polyhedral-product suspension splitting, expressed in the singular-homology model used by the mission.

Formalization Note The vertex injection is explicit, and fullness is the equivalence of face membership under its induced map on finite vertex sets. All homology groups use integral coefficients.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem momentAngle_fullSubcomplex_h1_homology
    {s m : ℕ} (hs : 0 < s)
    (K : AbstractSimplicialComplex (Fin s))
    (L : AbstractSimplicialComplex (Fin m)) (e : Fin s ↪ Fin m)
    (hfull : ∀ σ : Finset (Fin s), σ ∈ K ↔ σ.map e ∈ L) :
    AdditivelyEmbeds (IntegralHomology 1 (GeometricRealization K))
      (IntegralHomology (s + 2) (Complex L)) := by sorry

Source

First-homology consequence of 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). Apply the summand indexed by the full vertex set of K, of cardinality s. The suspension splitting gives degree s+2 before suspension.

View graph