Face numbers of simplicial spheres

StructureFinite simplicial sphere#✓fully proved

For a natural number \(d\), a finite simplicial \((d-1)\)-sphere is a geometric simplicial complex \(K\) in the Euclidean space \(\mathbb{R}^d\) with finitely many faces whose underlying space is homeomorphic to the unit sphere \(S^{d-1} = \{x \in \mathbb{R}^d : \|x\| = 1\}\).

structure FiniteSimplicialSphere (d : ℕ) where
  K : Geometry.SimplicialComplex ℝ (EuclideanSpace ℝ (Fin d))
  finite_faces : K.faces.Finite
  sphere_homeomorph :
    Nonempty (K.space ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin d)) 1)

Used by 9

Used byColour group of a 2-coloured sphere triangulation · Proper colourings of the triangles of a sphere triangulation · Kourovka Problem 17.35 (statement) · Triangles of a sphere triangulation · Dehn–Sommerville equations · Extended face numbers · Face numbers of a simplicial sphere · The h-vector of a simplicial sphere · Upper bound theorem for simplicial spheres

DefinitionFace numbers of a simplicial sphere#✓fully proved

For a finite simplicial \((d-1)\)-sphere \(X\) and a natural number \(k\), \(f_k(X)\) is the number of \(k\)-dimensional faces of \(X\), that is, of faces with exactly \(k+1\) vertices.

noncomputable def faceCount {d : ℕ} (X : FiniteSimplicialSphere d) (k : ℕ) : ℕ :=
  {s : Finset (EuclideanSpace ℝ (Fin d)) | s ∈ X.K.faces ∧ s.card = k + 1}.ncard

Uses 1 · Used by 2

Statement usesFinite simplicial sphere

Used byExtended face numbers · Upper bound theorem for simplicial spheres

DefinitionExtended face numbers#✓fully proved

For a finite simplicial \((d-1)\)-sphere \(X\) and a natural number \(i\), the \(i\)-th extended face number of \(X\) is \(1\) if \(i = 0\), and is the number \(f_{i-1}(X)\) of \((i-1)\)-dimensional faces of \(X\) if \(i \ge 1\). Thus it equals \(f_{i-1}(X)\) under the convention \(f_{-1}(X) = 1\).

noncomputable def extendedFaceCount {d : ℕ} (X : FiniteSimplicialSphere d) (i : ℕ) : ℕ :=
  if i = 0 then 1 else faceCount X (i - 1)

Uses 2 · Used by 1

Statement usesFinite simplicial sphere · Face numbers of a simplicial sphere

Used byThe h-vector of a simplicial sphere

DefinitionThe h-vector of a simplicial sphere#✓fully proved

For a finite simplicial \((d-1)\)-sphere \(X\) and a natural number \(j\),

\[h_j(X) = \sum_{i=0}^{j} (-1)^{j-i} \binom{d-i}{j-i} f_{i-1}(X),\]

where \(f_{i-1}(X)\) is the number of \((i-1)\)-dimensional faces of \(X\) for \(i \ge 1\), \(f_{-1}(X) = 1\), and \(d - i\) is read as \(0\) when \(i > d\).

noncomputable def hVector {d : ℕ} (X : FiniteSimplicialSphere d) (j : ℕ) : ℤ :=
  ∑ i ∈ Finset.range (j + 1),
    (-1 : ℤ) ^ (j - i) * (Nat.choose (d - i) (j - i) : ℤ) *
      (extendedFaceCount X i : ℤ)

Uses 2 · Used by 1

Statement usesFinite simplicial sphere · Extended face numbers

Used byDehn–Sommerville equations

TheoremDehn–Sommerville equations#●ready to prove

Let \(X\) be a finite simplicial \((d-1)\)-sphere, that is, a finite geometric simplicial complex in \(\mathbb{R}^d\) whose underlying space is homeomorphic to the unit sphere of \(\mathbb{R}^d\). Then for every natural number \(j \le d\), the h-vector of \(X\) satisfies \(h_j = h_{d-j}\). Here \(h_j = \sum_{i=0}^{j} (-1)^{j-i} \binom{d-i}{j-i} f_{i-1}\), where \(f_{-1} = 1\) and \(f_k\) is the number of \(k\)-dimensional faces of \(X\).

public theorem_wanted dehn_sommerville
    {d j : ℕ} (X : FiniteSimplicialSphere d) (hj : j ≤ d) :
    hVector X j = hVector X (d - j)

Sources

• M. Dehn (1905); D. M. Y. Sommerville (1927); see Stanley, Combinatorics and Commutative Algebra. Knill, Some fundamental theorems in mathematics, §142. Problem dehn_sommerville of the lean-eval benchmark.

Uses 2

Statement usesFinite simplicial sphere · The h-vector of a simplicial sphere

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.