Relabeling simplicial collapses

Simplicial collapse is intrinsic to a complex and must not depend on its ambient vertex names. This file proves that an injective relabeling preserves and reflects free pairs, elementary collapses, finite collapse sequences, and collapsibility.

This is functorial infrastructure for the collapse track in layer 11 of the geometric-topology roadmap. It lets later subdivision and product constructions replace a complex by an isomorphic copy before forming collapse sequences. The definitions of free pairs and collapse follow Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 3; the results here are the standard invariance of those definitions under a change of vertex labels.

Main results

• PreAbstractSimplicialComplex.IsFreePair.map: an injective vertex map preserves a free pair.
• PreAbstractSimplicialComplex.IsFreePair.map_iff_of_injective: an injective vertex map preserves and reflects a free pair.
• PreAbstractSimplicialComplex.ElementaryCollapsesTo.map: an injective vertex map preserves an elementary collapse.
• PreAbstractSimplicialComplex.ElementaryCollapsesTo.map_iff_of_injective: an injective vertex map preserves and reflects an elementary collapse.
• PreAbstractSimplicialComplex.CollapsesTo.map: an injective vertex map preserves a finite collapse sequence.
• PreAbstractSimplicialComplex.CollapsesTo.map_iff_of_injective: an injective vertex map preserves and reflects a collapse sequence.
• PreAbstractSimplicialComplex.CollapsesTo.map_equiv_iff: relabeling by a vertex equivalence preserves and reflects a collapse sequence.
• PreAbstractSimplicialComplex.Collapsible.map_iff_of_injective: an injective vertex map preserves and reflects collapsibility.
• PreAbstractSimplicialComplex.Collapsible.map_equiv_iff: relabeling by a vertex equivalence preserves and reflects collapsibility.

@[simp]

theorem PreAbstractSimplicialComplex.map_point {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (v : α) : (point v).map f = point (f v)

Mapping a one-vertex complex along any vertex map gives the one-vertex complex at the image vertex.

@[simp]

theorem PreAbstractSimplicialComplex.map_deletion {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (hf : Function.Injective f) (K : PreAbstractSimplicialComplex α) (σ : Finset α) : (K.deletion σ).map f = (K.map f).deletion (Finset.image f σ)

An injective vertex map commutes with deletion: a face contains the image of σ exactly when its unique preimage face contains σ.

theorem PreAbstractSimplicialComplex.IsFreePair.map {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {σ τ : Finset α} (h : K.IsFreePair σ τ) (f : α → β) (hf : Function.Injective f) : (K.map f).IsFreePair (Finset.image f σ) (Finset.image f τ)

An injective relabeling of the vertices of a complex carries a free pair to a free pair in the image complex.

theorem PreAbstractSimplicialComplex.IsFreePair.map_iff_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} {σ τ : Finset α} (f : α → β) (hf : Function.Injective f) : (K.map f).IsFreePair (Finset.image f σ) (Finset.image f τ) ↔ K.IsFreePair σ τ

An injective relabeling preserves and reflects a free pair.

theorem PreAbstractSimplicialComplex.ElementaryCollapsesTo.map {α : Type u_1} {β : Type u_2} [DecidableEq β] {K L : PreAbstractSimplicialComplex α} (h : K.ElementaryCollapsesTo L) (f : α → β) (hf : Function.Injective f) : (K.map f).ElementaryCollapsesTo (L.map f)

An injective relabeling preserves an elementary collapse. The deleted free pair is sent to its image pair.

theorem PreAbstractSimplicialComplex.ElementaryCollapsesTo.map_iff_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq β] {K L : PreAbstractSimplicialComplex α} (f : α → β) (hf : Function.Injective f) : (K.map f).ElementaryCollapsesTo (L.map f) ↔ K.ElementaryCollapsesTo L

An injective relabeling preserves and reflects an elementary collapse.

theorem PreAbstractSimplicialComplex.CollapsesTo.map {α : Type u_1} {β : Type u_2} [DecidableEq β] {K L : PreAbstractSimplicialComplex α} (h : K.CollapsesTo L) (f : α → β) (hf : Function.Injective f) : (K.map f).CollapsesTo (L.map f)

An injective relabeling carries every finite collapse sequence to the corresponding sequence between the image complexes.

theorem PreAbstractSimplicialComplex.CollapsesTo.map_iff_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq β] {K L : PreAbstractSimplicialComplex α} (f : α → β) (hf : Function.Injective f) : (K.map f).CollapsesTo (L.map f) ↔ K.CollapsesTo L

An injective relabeling preserves and reflects finite collapse sequences.

@[simp]

theorem PreAbstractSimplicialComplex.CollapsesTo.map_equiv_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {K L : PreAbstractSimplicialComplex α} (e : α ≃ β) : (K.map ⇑e).CollapsesTo (L.map ⇑e) ↔ K.CollapsesTo L

Relabeling both complexes by a vertex equivalence preserves and reflects the existence of a finite collapse sequence.

theorem PreAbstractSimplicialComplex.Collapsible.map {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} (h : K.Collapsible) (f : α → β) (hf : Function.Injective f) : (K.map f).Collapsible

An injective relabeling preserves collapsibility, with the image of a terminal vertex as the terminal vertex of the image collapse.

theorem PreAbstractSimplicialComplex.Collapsible.map_iff_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} (f : α → β) (hf : Function.Injective f) : (K.map f).Collapsible ↔ K.Collapsible

An injective relabeling preserves and reflects collapsibility.

@[simp]

theorem PreAbstractSimplicialComplex.Collapsible.map_equiv_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : PreAbstractSimplicialComplex α} (e : α ≃ β) : (K.map ⇑e).Collapsible ↔ K.Collapsible

Relabeling a complex by a vertex equivalence preserves and reflects collapsibility.