Stellar subdivision at a face

Starring a complex K at one of its faces σ, with a fresh vertex v, replaces the closed star of σ by the cone with apex v on the boundary of that closed star. It is the combinatorial model of the geometric move in which a new vertex placed in the interior of σ cones off the boundary of the closed star; suitably realized, the source and the target of that move are PL-homeomorphic, but nothing of the kind is asserted here, since the construction below supplies no placement of v (see the paragraph on realizations).

This file builds that move for PreAbstractSimplicialComplex, Mathlib's downward-closed collections of nonempty finite faces. The precomplex type is the right home: a starring changes which vertices are used, since σ itself stops being a face while v becomes one.

The definition is the usual explicit description of the faces, split by whether the new vertex occurs. A face is either

• a face τ of K with v ∉ τ that does not contain σ; when v is fresh, these are the faces of the deletion deletion K σ; or
• insert v ρ, where ρ does not contain σ and ρ ∪ σ is a face of K — that is, v joined with a face of the boundary ∂σ ∗ link K σ of the closed star.

Phrasing the second clause through ρ ∪ σ ∈ K rather than through an explicit join keeps the whole construction on the original vertex type, so starrings can be iterated. The face collection is downward closed with no hypothesis at all on σ or v. For a genuine stellar move, the intended hypotheses are that σ is a face and that v is fresh, meaning {v} is not a face of K (equivalently, by notMem_of_singleton_notMem, that v occurs in no face); individual theorems state only the assumptions they need.

Stellar subdivision is the combinatorial substitute for a general subdivision that layer 11 of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md) needs before combinatorial spheres and balls can be defined: those are complexes that are PL-homeomorphic, after subdivision, to the boundary of the standard simplex, respectively to the standard simplex, and the barycentric subdivision alone (Subdivision.Basic) is too rigid to serve, since it cannot be applied at a single face. The equivalence relation generated by the move is Subdivision.Stellar.Equivalence, and the ball, sphere and manifold predicates built from it are in CombinatorialManifold. The definition and the standard-model computations follow Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2 (starring and stellar moves).

No claim is made here that a starring preserves the geometric realization; that identification is realization work, parallel to the corresponding open question for Subdivision.Basic. What is proved is the combinatorial shadow of it: the dimension is unchanged, the part of the subdivision away from the new vertex is exactly deletion K σ, and the link of the new vertex is exactly the boundary closedStar K σ ⊓ deletion K σ of the closed star, so the subdivision is glued from the same two pieces the geometric picture uses.

Main definitions

• PreAbstractSimplicialComplex.stellarSubdivision K σ v: the complex obtained from K by starring the face σ at the fresh vertex v.

Main results

• PreAbstractSimplicialComplex.mem_stellarSubdivision_iff_of_notMem and insert_mem_stellarSubdivision_iff: the two halves of the face description, one for faces missing the new vertex and one for faces containing it.
• PreAbstractSimplicialComplex.singleton_mem_stellarSubdivision_iff: the new vertex is a vertex of the subdivision exactly when σ was a face, and PreAbstractSimplicialComplex.self_notMem_stellarSubdivision: the starred face is destroyed, as long as the new vertex does not already lie in it.
• PreAbstractSimplicialComplex.deletion_stellarSubdivision_singleton and link_stellarSubdivision_singleton: away from the new vertex the subdivision is deletion K σ, and the link of the new vertex is the boundary closedStar K σ ⊓ deletion K σ of the closed star.
• PreAbstractSimplicialComplex.map_stellarSubdivision: injective relabeling commutes with stellar subdivision.
• PreAbstractSimplicialComplex.dimension_stellarSubdivision: starring preserves the dimension.
• PreAbstractSimplicialComplex.finite_faces_stellarSubdivision_iff: a genuine starring preserves and reflects finiteness.
• PreAbstractSimplicialComplex.isCone_stellarSubdivision_of_closedStar_eq_self: starring a complex that is its own closed star at σ produces a cone with apex the new vertex; for a simplex, PreAbstractSimplicialComplex.link_stellarSubdivision_simplex_self identifies the link of that apex with the simplex boundary.

def PreAbstractSimplicialComplex.stellarSubdivision {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (σ : Finset ι) (v : ι) : PreAbstractSimplicialComplex ι

The stellar subdivision (or starring) of K at the face σ, using the new vertex v.

Its faces are the faces τ of K with v ∉ τ that do not contain σ, together with the sets insert v ρ for which ρ does not contain σ and ρ ∪ σ is a face of K. Under the intended freshness hypothesis, equivalently, the closed star of σ is removed and replaced by the cone with apex v on the boundary of that closed star.

The intended hypotheses are that σ is a face of K and that v is fresh, i.e. {v} ∉ K; they are not part of the definition, and the degenerate values are pinned by stellarSubdivision_empty and stellarSubdivision_eq_self_of_notMem.

Equations

• K.stellarSubdivision σ v = { faces := {τ : Finset ι | v ∉ τ ∧ τ ∈ K ∧ ¬σ ⊆ τ ∨ v ∈ τ ∧ ¬σ ⊆ τ.erase v ∧ τ.erase v ∪ σ ∈ K}, isRelLowerSet_faces := ⋯ }

theorem PreAbstractSimplicialComplex.mem_stellarSubdivision_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} {v : ι} : τ ∈ K.stellarSubdivision σ v ↔ v ∉ τ ∧ τ ∈ K ∧ ¬σ ⊆ τ ∨ v ∈ τ ∧ ¬σ ⊆ τ.erase v ∧ τ.erase v ∪ σ ∈ K

The defining description of the faces of a stellar subdivision, split by whether the new vertex occurs.

@[simp]

theorem PreAbstractSimplicialComplex.mem_stellarSubdivision_iff_of_notMem {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} {v : ι} (hvτ : v ∉ τ) : τ ∈ K.stellarSubdivision σ v ↔ τ ∈ K ∧ ¬σ ⊆ τ

A set missing the new vertex is a face of the stellar subdivision exactly when it is a face of K not containing the starred face: these are precisely the faces of deletion K σ.

@[simp]

theorem PreAbstractSimplicialComplex.insert_mem_stellarSubdivision_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ ρ : Finset ι} {v : ι} (hvρ : v ∉ ρ) : insert v ρ ∈ K.stellarSubdivision σ v ↔ ¬σ ⊆ ρ ∧ ρ ∪ σ ∈ K

A set containing the new vertex is a face of the stellar subdivision exactly when the rest of it is a face of the boundary of the closed star of σ: it must not contain σ, while its union with σ must remain a face.

@[simp]

theorem PreAbstractSimplicialComplex.singleton_mem_stellarSubdivision_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} : {v} ∈ K.stellarSubdivision σ v ↔ σ ∈ K

The new vertex becomes a vertex of the stellar subdivision exactly when the starred set was a face to begin with.

theorem PreAbstractSimplicialComplex.self_notMem_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hvσ : v ∉ σ) : σ ∉ K.stellarSubdivision σ v

Starring destroys the starred face, as long as the new vertex does not already lie in σ: every face of the subdivision either avoids σ or contains the new vertex, and in the latter case avoids σ after erasing it. The hypothesis v ∉ σ is needed, since for v ∈ σ one has σ.erase v ∪ σ = σ, so σ survives the starring whenever it was a face.

theorem PreAbstractSimplicialComplex.stellarSubdivision_ne_self {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hvσ : v ∉ σ) (hσ : σ ∈ K) : K.stellarSubdivision σ v ≠ K

Starring a genuine face at a vertex outside that face genuinely changes the complex.

@[simp]

theorem PreAbstractSimplicialComplex.stellarSubdivision_empty {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (v : ι) : K.stellarSubdivision ∅ v = ⊥

Starring at the empty set gives the bottom precomplex.

theorem PreAbstractSimplicialComplex.stellarSubdivision_eq_self_of_notMem {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hv : {v} ∉ K) (hσne : σ.Nonempty) (hσ : σ ∉ K) : K.stellarSubdivision σ v = K

Starring at a nonempty set that is not a face changes nothing, provided the new vertex is fresh: no face of K can contain the starred set, and freshness makes the new vertex occur in no face of K and in no face of the subdivision. Freshness is needed: without it, starring can destroy the faces of K that contain v.

The two pieces glued by a starring

Away from the new vertex a stellar subdivision is the deletion deletion K σ, and the link of the new vertex is the boundary closedStar K σ ⊓ deletion K σ of the closed star of σ. Together with closedStar_sup_deletion these say that the subdivision is the union of deletion K σ and the cone with apex v on that boundary, which is the geometric description of the move.

@[simp]

theorem PreAbstractSimplicialComplex.deletion_stellarSubdivision_singleton {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hv : {v} ∉ K) : (K.stellarSubdivision σ v).deletion {v} = K.deletion σ

The faces of a stellar subdivision missing the new vertex form exactly the deletion of the starred face.

theorem PreAbstractSimplicialComplex.deletion_le_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hv : {v} ∉ K) : K.deletion σ ≤ K.stellarSubdivision σ v

The deletion of the starred face survives untouched inside the stellar subdivision.

@[simp]

theorem PreAbstractSimplicialComplex.link_stellarSubdivision_singleton {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hv : {v} ∉ K) : (K.stellarSubdivision σ v).link {v} = K.closedStar σ ⊓ K.deletion σ

The link of the new vertex in a stellar subdivision is the boundary of the closed star of the starred face, namely closedStar K σ ⊓ deletion K σ: the faces ρ with ρ ∪ σ a face of K that do not themselves contain σ. This is the combinatorial form of "v is coned off over ∂σ ∗ link K σ".

Relabeling

@[simp]

theorem PreAbstractSimplicialComplex.map_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} {κ : Type u_2} [DecidableEq κ] (f : ι → κ) (hf : Function.Injective f) : (K.stellarSubdivision σ v).map f = (K.map f).stellarSubdivision (Finset.image f σ) (f v)

An injective relabeling commutes with stellar subdivision.

Dimension and finiteness

@[simp]

theorem PreAbstractSimplicialComplex.dimension_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hv : {v} ∉ K) (hσne : σ.Nonempty) : (K.stellarSubdivision σ v).dimension = K.dimension

Starring a nonempty set at a fresh vertex preserves the dimension.

theorem PreAbstractSimplicialComplex.finite_faces_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hfin : K.faces.Finite) : (K.stellarSubdivision σ v).faces.Finite

Starring a complex with finitely many faces again gives finitely many faces: a face either is a face of K, or is the new vertex adjoined to a subset of a face of K.

theorem PreAbstractSimplicialComplex.finite_faces_stellarSubdivision_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : {v} ∉ K) : (K.stellarSubdivision σ v).faces.Finite ↔ K.faces.Finite

A genuine stellar subdivision preserves and reflects finiteness of the face collection.

Starring a closed star, and the standard model

When K is its own closed star at σ — the case of a simplex starred at its top face — every face can absorb the new vertex, so the subdivision is a cone with apex v.

theorem PreAbstractSimplicialComplex.isCone_stellarSubdivision_of_closedStar_eq_self {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hstar : K.closedStar σ = K) : (K.stellarSubdivision σ v).IsCone v

Starring a complex that is its own closed star at σ produces a cone with apex the new vertex.

theorem PreAbstractSimplicialComplex.isCone_stellarSubdivision_simplex_self {ι : Type u_1} [DecidableEq ι] {V : Finset ι} {v : ι} (hV : V.Nonempty) : ((simplex V).stellarSubdivision V v).IsCone v

Starring a simplex at its whole vertex set produces a cone with apex the new vertex.

theorem PreAbstractSimplicialComplex.link_stellarSubdivision_simplex_self {ι : Type u_1} [DecidableEq ι] {V : Finset ι} {v : ι} (hv : v ∉ V) : ((simplex V).stellarSubdivision V v).link {v} = simplexBoundary V

The starred simplex is the cone on the simplex boundary: the link of the new vertex is exactly simplexBoundary V. This is the standard model of the move, and pins the convention.

theorem PreAbstractSimplicialComplex.dimension_stellarSubdivision_simplex_self {ι : Type u_1} [DecidableEq ι] {V : Finset ι} {v : ι} (hv : v ∉ V) (hV : V.Nonempty) : ((simplex V).stellarSubdivision V v).dimension = ↑(V.card - 1)

Starring a simplex at its whole vertex set leaves the dimension at V.card - 1.