Face counts under simplicial collapse

An elementary simplicial collapse removes exactly its free face and unique coface. This file turns that description into cardinality control: every elementary collapse removes two faces, while an arbitrary collapse can only decrease the face cardinality. For finite complexes this also gives subtraction, strictness, and parity results for natural-valued face counts.

These facts are basic bookkeeping for the collapse track in layer 11 of the geometric-topology roadmap. In particular, they provide a termination measure for finite collapse arguments and the parity obstruction that any proposed collapse certificate must satisfy. The definitions of free pairs and collapse are those in ElementaryCollapse and Collapse.Basic, following Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 3.

Main results

• ElementaryCollapsesTo.encard_faces_add_two: the face counts before and after an elementary collapse differ by two.
• CollapsesTo.encard_faces_le: an arbitrary collapse can only decrease the face cardinality.

theorem PreAbstractSimplicialComplex.ElementaryCollapsesTo.encard_faces_add_two {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.ElementaryCollapsesTo L) : L.faces.encard + 2 = K.faces.encard

An elementary collapse removes exactly two faces.

theorem PreAbstractSimplicialComplex.ElementaryCollapsesTo.ncard_faces_add_two {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.ElementaryCollapsesTo L) (hK : K.faces.Finite) : L.faces.ncard + 2 = K.faces.ncard

An elementary collapse of a finite complex removes exactly two faces.

theorem PreAbstractSimplicialComplex.ElementaryCollapsesTo.ncard_faces_eq_sub_two {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.ElementaryCollapsesTo L) (hK : K.faces.Finite) : L.faces.ncard = K.faces.ncard - 2

The face count after an elementary collapse is the original face count minus two.

theorem PreAbstractSimplicialComplex.ElementaryCollapsesTo.ncard_faces_lt {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.ElementaryCollapsesTo L) (hK : K.faces.Finite) : L.faces.ncard < K.faces.ncard

An elementary collapse strictly decreases the number of faces of a finite complex.

theorem PreAbstractSimplicialComplex.ElementaryCollapsesTo.ncard_faces_mod_two {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.ElementaryCollapsesTo L) (hK : K.faces.Finite) : L.faces.ncard % 2 = K.faces.ncard % 2

An elementary collapse preserves the parity of the number of faces.

theorem PreAbstractSimplicialComplex.CollapsesTo.encard_faces_le {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.CollapsesTo L) : L.faces.encard ≤ K.faces.encard

A collapse can only decrease the face cardinality.

theorem PreAbstractSimplicialComplex.CollapsesTo.ncard_faces_le {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.CollapsesTo L) (hK : K.faces.Finite) : L.faces.ncard ≤ K.faces.ncard

A collapse of a finite complex can only decrease its number of faces.

theorem PreAbstractSimplicialComplex.CollapsesTo.ncard_faces_mod_two {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.CollapsesTo L) (hK : K.faces.Finite) : L.faces.ncard % 2 = K.faces.ncard % 2

A collapse of a finite complex preserves the parity of its number of faces.