Moment-angle complexes and total integral homology

IsFaceOrEmpty. For any natural number $m$, any abstract simplicial complex $L$ on the vertex type $\operatorname{Fin}(m)$, and any finite set $\sigma$ of those vertices, IsFaceOrEmpty L σ means exactly that either $\sigma$ is empty or $\sigma$ is a face recorded by $L$. No nonemptiness of $\sigma$ is otherwise required.

GeometricRealization. For any natural number $m$ and abstract simplicial complex $L$ on $\operatorname{Fin}(m)$, the geometric realization is the subtype of functions $x:\operatorname{Fin}(m)\to\mathbb R$ such that every $x_i\ge 0$, the finite sum of all coordinates is $1$, and the finite set of indices at which $x_i\ne0$ belongs to $L$. Thus the support is required to be an actual recorded face, not merely empty-or-a-face. When $m=0$, no such $x$ exists because the empty sum is $0$, not $1$.

FourSphere. FourSphere is the metric sphere of radius $1$ centered at the zero vector in the Euclidean space $\mathbb R^5$; its elements are exactly the vectors in that space whose distance from zero is $1$.

IsSimplicialFourSphere. For any natural number $m$ and abstract simplicial complex $L$ on $\operatorname{Fin}(m)$, IsSimplicialFourSphere L means that there exists a homeomorphism between the above geometric-realization subtype and the unit sphere in $\mathbb R^5$. It does not separately assert a combinatorial dimension, purity, a manifold structure, or any particular triangulation property beyond the existence of that homeomorphism.

IsInMomentAngle. For any natural number $m$, abstract simplicial complex $L$ on $\operatorname{Fin}(m)$, and function $z:\operatorname{Fin}(m)\to\mathbb C$, IsInMomentAngle L z means that there exists a finite set $\sigma$ of vertices such that $\sigma$ is empty or is a face of $L$, and, for every vertex $i$, one has $|z_i|\le1$ if $i\in\sigma$ and $|z_i|=1$ if $i\notin\sigma$. The witnessing face is not required to be unique; coordinates on its boundary may also have modulus $1$. When $m=0$, the empty $\sigma$ witnesses the condition for the unique empty function, since the coordinate condition is vacuous.

Complex. For any natural number $m$ and abstract simplicial complex $L$ on $\operatorname{Fin}(m)$, Complex L is the subtype of functions $z:\operatorname{Fin}(m)\to\mathbb C$ satisfying the preceding existential face-and-modulus condition. This declaration itself asserts no manifold property.

basepoint. For every such $L$, basepoint L is the element of Complex L whose every coordinate is $1$. Its membership is witnessed by the empty finite set: every coordinate is outside that set and has modulus $1$. This also defines a point when $m=0$.

BasedLoopSpace. For every such $L$, BasedLoopSpace L is the type of parametrized continuous paths in Complex L whose initial and terminal points are both the all-ones basepoint. It is the path/loop space itself, not a set of homotopy classes.

IntegralHomology. For every natural degree $q$ and topological type $X$, IntegralHomology q X is the underlying type of Mathlib’s degree-$q$ singular-homology object of $X$ with coefficients in the rank-one integer module $\mathbb Z$. Only nonnegative degrees are represented because $q$ ranges over $\mathbb N$.

TotalIntegralHomology. For every topological type $X$, TotalIntegralHomology X is the direct sum, indexed by all $q\in\mathbb N$, of the preceding integral singular-homology groups. Its elements therefore have only finitely many nonzero degree components.

AdditivelyEmbeds. For types $G$ and $H$ equipped only with addition and zero, AdditivelyEmbeds G H means that there exists an injective map $f:G\to H$ preserving addition and zero. It asserts neither surjectivity nor a splitting, and when $H$ is graded it imposes no requirement that the image lie in or preserve any one degree.