Finite simplicial complexes, minimal non-faces, flagness, stellar subdivision
DefinitionHirsch_simplicial_complex_flagAbstract finite simplicial complexes on a vertex type , given by a Finset of faces closed under subsets and containing . A minimal non-face of is a subset of 's own vertex support () that is not a face of but every proper subset of which is; a complex is flag if every minimal non-face has exactly two vertices. The stellar subdivision of at a face with a new vertex (not used by any face of ) removes the open star of and cones the link of , joined with the proper faces of , from .
These are the objects of Adiprasito–Benedetti's Hirsch theorem for flag normal complexes, and of the campaign's own results bounding minimal non-face counts under stellar refinement (stellar_injects_minimal_nonfaces, flag_refinement_vertex_lower_bound).
Formalization Note The restriction in IsMinimalNonface is load-bearing: without it, any vertex unused by trivially yields a content-free minimal non-face , which would make the stellar-subdivision injection theorem false as stated (an unused vertex introduced as the new stellar center would give a singleton non-face of with no image among 's non-faces). The restriction matches how vertexCard already measures "vertices actually used by " and does not otherwise change stellar, IsFlag, or vertexCard.
import Mathlib
/-!
# Finite simplicial complexes, minimal non-faces, flagness, stellar subdivision
Abstract finite simplicial complexes on a vertex type `V`, given by their set of faces
(closed under subsets). A **minimal non-face** is a non-face all of whose proper subsets
are faces; a complex is **flag** if every minimal non-face has exactly two vertices.
The **stellar subdivision** at a face `σ` with a new vertex `a` removes the star of `σ`
and cones the link of `σ` joined with the boundary of `σ` from `a`.
These are the objects of Adiprasito--Benedetti's Hirsch theorem for flag normal
complexes (*The Hirsch conjecture holds for normal flag complexes*, Math. Oper. Res.
39 (2014)), and of the campaign's negative result that polynomially many stellar
subdivisions cannot make the boundary of the cyclic polytope `C(4m, 2m)` flag.
-/
namespace Hirsch
/-- A finite abstract simplicial complex on `V`: a set of faces closed under subsets and
containing the empty face. -/
structure SComplex (V : Type*) [DecidableEq V] where
faces : Finset (Finset V)
empty_mem : ∅ ∈ faces
down_closed : ∀ σ ∈ faces, ∀ τ ⊆ σ, τ ∈ faces
namespace SComplex
variable {V : Type*} [DecidableEq V] [Fintype V]
/-- A minimal non-face: a subset of `K`'s own vertex support that is not a face,
but every proper subset of which is a face. Restricting `M` to `K.faces.biUnion id`
(the vertices actually used by some face of `K`) rules out vacuous "non-faces" built
from vertices unrelated to `K`, e.g. a vertex `a` with `∀ F ∈ K.faces, a ∉ F` would
otherwise make `{a}` a content-free minimal non-face. -/
def IsMinimalNonface (K : SComplex V) (M : Finset V) : Prop :=
M ⊆ K.faces.biUnion id ∧ M ∉ K.faces ∧ ∀ τ ⊂ M, τ ∈ K.faces
/-- Flag complexes: every minimal non-face is an edge. -/
def IsFlag (K : SComplex V) : Prop :=
∀ M, K.IsMinimalNonface M → M.card = 2
/-- The stellar subdivision of `K` at the face `σ` using the new vertex `a ∉ σ`
(`a` is required not to be a vertex of any face of `K`). Faces are: faces not containing
`σ`, and sets `insert a (τ ∪ ρ)` with `τ ⊂ σ` proper, `ρ ∈ link σ` (i.e. `ρ ∪ σ ∈ K`,
`ρ ∩ σ = ∅`). -/
def stellar (K : SComplex V) (σ : Finset V) (a : V) : Finset (Finset V) :=
(K.faces.filter (fun F => ¬ σ ⊆ F)) ∪
((K.faces.filter (fun ρ => Disjoint ρ σ ∧ ρ ∪ σ ∈ K.faces)).biUnion
(fun ρ => (σ.powerset.filter (fun τ => τ ⊂ σ)).image (fun τ => insert a (τ ∪ ρ))))
/-- Number of vertices actually used by a complex. -/
def vertexCard (K : SComplex V) : ℕ := (K.faces.biUnion id).card
end SComplex
end Hirsch