Characteristic maps of simplicial cells

An enumeration of the vertices of a face identifies its closed simplex with the closed unit ball of Fin n → ℝ, with the sup norm used by Mathlib's classical CW complexes. The sphere maps exactly onto the proper faces, and the open ball maps exactly onto the points whose barycentric support is the whole face. These are the characteristic maps for the cell structure on a weak geometric realization, including zero-dimensional cells.

The enumeration is an explicit argument: an ordered enumeration can therefore fix the orientation used in cellular boundary formulas. The ambient complex may be infinite. The maps compose realizationTopHomeomorphPiClosedBall with the face relabeling realizationTopHomeomorphFace. Outside the closed ball the characteristic map takes the value at the origin.

Reference: C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2 (simplices and polyhedra); A. Hatcher, Algebraic Topology, Chapter 0 (the cell structure of a simplicial complex).

noncomputable def AbstractSimplicialComplex.simplexCharacteristicMap {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : PartialEquiv (Fin n → ℝ) K.Realization

The characteristic map of an enumerated simplicial cell. Its source is the sup-norm open unit ball, and its target consists of the points whose support equals the face. It is continuous on the closed ball and parametrizes all proper faces on the sphere.

@[simp]

theorem AbstractSimplicialComplex.simplexCharacteristicMap_source {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : (K.simplexCharacteristicMap f hf).source = Metric.ball 0 1

The source of a simplicial characteristic map is the open unit ball.

@[simp]

theorem AbstractSimplicialComplex.simplexCharacteristicMap_target {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : (K.simplexCharacteristicMap f hf).target = {x : K.Realization | (↑x).support = Finset.image (⇑f) Finset.univ}

The open cell consists exactly of points with the enumerated face as their support.

theorem AbstractSimplicialComplex.simplexCharacteristicMap_apply {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) {x : Fin n → ℝ} (hx : x ∈ Metric.closedBall 0 1) : ↑(K.simplexCharacteristicMap f hf) x = ↑((K.simplexClosedBallHomeomorph f hf) ⟨x, hx⟩)

On the closed ball the characteristic map agrees with the closed-simplex homeomorphism.

theorem AbstractSimplicialComplex.injOn_simplexCharacteristicMap_closedBall {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : Set.InjOn (↑(K.simplexCharacteristicMap f hf)) (Metric.closedBall 0 1)

The characteristic map is injective on the closed ball.

@[simp]

theorem AbstractSimplicialComplex.simplexCharacteristicMap_apply_symm {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) (y : { x : K.Realization // (↑x).support ⊆ Finset.image (⇑f) Finset.univ }) : ↑(K.simplexCharacteristicMap f hf) ↑((K.simplexClosedBallHomeomorph f hf).symm y) = ↑y

The characteristic map sends the inverse closed-simplex homeomorphism of a point back to that point.

theorem AbstractSimplicialComplex.simplexCharacteristicMap_apply_of_notMem_closedBall {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) {x : Fin n → ℝ} (hx : x ∉ Metric.closedBall 0 1) : ↑(K.simplexCharacteristicMap f hf) x = ↑((K.simplexClosedBallHomeomorph f hf) ⟨0, ⋯⟩)

Outside the closed ball the characteristic map takes its value at the origin.

theorem AbstractSimplicialComplex.simplexCharacteristicMap_symm_apply {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) {y : K.Realization} (hy : (↑y).support = Finset.image (⇑f) Finset.univ) : ↑(K.simplexCharacteristicMap f hf).symm y = ↑((K.simplexClosedBallHomeomorph f hf).symm ⟨y, ⋯⟩)

On the open cell, the inverse characteristic map is the inverse closed-simplex homeomorphism followed by the inclusion into the ambient coordinate space.

theorem AbstractSimplicialComplex.continuousOn_simplexCharacteristicMap {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : ContinuousOn (↑(K.simplexCharacteristicMap f hf)) (Metric.closedBall 0 1)

The characteristic map is continuous on its closed cell domain.

theorem AbstractSimplicialComplex.continuousOn_simplexCharacteristicMap_symm {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : ContinuousOn (↑(K.simplexCharacteristicMap f hf).symm) (K.simplexCharacteristicMap f hf).target

The inverse of a simplicial characteristic map is continuous on the open cell.

@[simp]

theorem AbstractSimplicialComplex.image_simplexCharacteristicMap_closedBall {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : ↑(K.simplexCharacteristicMap f hf) '' Metric.closedBall 0 1 = {x : K.Realization | (↑x).support ⊆ Finset.image (⇑f) Finset.univ}

The closed ball maps onto the whole closed simplex.

@[simp]

theorem AbstractSimplicialComplex.image_simplexCharacteristicMap_sphere {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : ↑(K.simplexCharacteristicMap f hf) '' Metric.sphere 0 1 = {x : K.Realization | (↑x).support ⊂ Finset.image (⇑f) Finset.univ}

The sphere maps onto exactly the proper faces of the closed simplex.