Characteristic maps under ordered simplicial maps

A simplicial map that is injective on a face sends its cell to a cell of the same dimension. If it also preserves the order of that face's vertices, its realization carries the chosen characteristic map to the chosen characteristic map of the image cell, and the image of its j-th deleted-vertex face is the j-th face of the image cell. The hypothesis is local to the face: vertices belonging to different faces may be identified or have their order reversed. The equality holds on the whole characteristic-map domain, including the constant extension outside the closed ball.

References

• A. Hatcher, Algebraic Topology, Chapter 0 (simplicial complexes as CW complexes).
• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

def AbstractSimplicialComplex.RealizationCell.map {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {n : ℕ} [DecidableEq β] (c : K.RealizationCell n) (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (hf : Set.InjOn ⇑f ↑↑↑c) : L.RealizationCell n

The image cell of a simplicial cell under a map injective on that cell's vertices.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.map_face {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {n : ℕ} [DecidableEq β] (c : K.RealizationCell n) (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (hf : Set.InjOn ⇑f ↑↑↑c) : ↑(c.map f hf) = (TauCeti.PreAbstractSimplicialComplex.SimplicialMap.faceOrderHom f) ↑c

The face underlying the image cell is the image of the original face.

theorem AbstractSimplicialComplex.RealizationCell.coe_map_face {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {n : ℕ} [DecidableEq β] (c : K.RealizationCell n) (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (hf : Set.InjOn ⇑f ↑↑↑c) : ↑↑↑(c.map f hf) = ⇑f '' ↑↑↑c

The vertices of the image cell form the image of the original vertex set.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.map_id {α : Type u_1} {K : AbstractSimplicialComplex α} {n : ℕ} [DecidableEq α] (c : K.RealizationCell n) : c.map (PreAbstractSimplicialComplex.SimplicialMap.id K.toPreAbstractSimplicialComplex) ⋯ = c

The identity simplicial map fixes each cell.

theorem AbstractSimplicialComplex.RealizationCell.map_map {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {n : ℕ} [DecidableEq β] {γ : Type u_3} [DecidableEq γ] {P : AbstractSimplicialComplex γ} (c : K.RealizationCell n) (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (hf : Set.InjOn ⇑f ↑↑↑c) (g : L.SimplicialMap P.toPreAbstractSimplicialComplex) (hg : Set.InjOn ⇑g ↑(Finset.image ⇑f ↑↑c)) : (c.map f hf).map g ⋯ = c.map (g.comp f) ⋯

Mapping a cell successively agrees with mapping it along the composite simplicial map.

theorem AbstractSimplicialComplex.RealizationCell.vertexEmbedding_map {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {n : ℕ} [LinearOrder α] [LinearOrder β] (c : K.RealizationCell n) (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (hf : StrictMonoOn ⇑f ↑↑↑c) : ⇑(c.map f ⋯).vertexEmbedding = ⇑f ∘ ⇑c.vertexEmbedding

A vertex map increasing on a cell carries its increasing enumeration to the increasing enumeration of the image cell.

theorem AbstractSimplicialComplex.RealizationCell.face_map {α : Type u_1} {β : Type u_2} {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {n : ℕ} [LinearOrder α] [LinearOrder β] (c : K.RealizationCell (n + 1)) (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (hf : StrictMonoOn ⇑f ↑↑↑c) (j : Fin (n + 2)) : (c.face j).map f ⋯ = (c.map f ⋯).face j

A vertex map increasing on a cell carries its j-th deleted-vertex face to the j-th deleted-vertex face of the image cell.

theorem PreAbstractSimplicialComplex.SimplicialMap.strictMonoOn_id_realizationCell {α : Type u_1} [LinearOrder α] (K : AbstractSimplicialComplex α) (n : ℕ) (c : K.RealizationCell n) : StrictMonoOn ⇑(id K.toPreAbstractSimplicialComplex) ↑↑↑c

The identity simplicial map is strictly increasing on every cell.

theorem PreAbstractSimplicialComplex.SimplicialMap.strictMonoOn_comp_realizationCell {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {γ : Type u_3} [LinearOrder γ] {P : AbstractSimplicialComplex γ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (hf : ∀ (n : ℕ) (c : K.RealizationCell n), StrictMonoOn ⇑f ↑↑↑c) (g : L.SimplicialMap P.toPreAbstractSimplicialComplex) (hg : ∀ (n : ℕ) (c : L.RealizationCell n), StrictMonoOn ⇑g ↑↑↑c) (n : ℕ) (c : K.RealizationCell n) : StrictMonoOn ⇑(g.comp f) ↑↑↑c

Simplexwise strictly increasing simplicial maps remain so under composition.

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_characteristicMap {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {n : ℕ} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (c : K.RealizationCell n) (hf : StrictMonoOn ⇑f ↑↑↑c) (x : Fin n → ℝ) : f.realizationMap (↑c.characteristicMap x) = ↑(c.map f ⋯).characteristicMap x

On a cell where the vertex map preserves order strictly, realization carries its characteristic map to the characteristic map of its image cell. No hypothesis is imposed on vertices outside that cell.