Realization of simplicial maps

A simplicial vertex map extends affinely over each closed simplex to a continuous map of weak realizations. Coordinates of vertices with the same image are added, so injectivity of the vertex map is unnecessary. Identity and composition are preserved, and mutually inverse simplicial maps induce a homeomorphism. These maps transport simplicial local models and their relabelings to the polyhedra used in triangulations and piecewise-linear charts.

For a vertex map f, the barycentric coordinate at a target vertex b is the sum of the source coordinates over vertices sent to b. On each face, the induced map is the affine extension of f into the simplex on the image vertex set; realizationMap_comp_faceInclusion characterizes this restriction. The induced map is injective exactly when the vertex map is.

Main definitions

• AbstractSimplicialComplex.StandardSimplex.map: affine pushforward on a closed simplex.
• PreAbstractSimplicialComplex.SimplicialMap.realizationMap: the induced continuous map.
• PreAbstractSimplicialComplex.SimplicialMap.realizationHomeomorph: the homeomorphism induced by mutually inverse simplicial maps.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

noncomputable def AbstractSimplicialComplex.StandardSimplex.map {α : Type u_1} {β : Type u_2} [DecidableEq β] {σ : Finset α} (x : StandardSimplex σ) (f : α → β) : StandardSimplex (Finset.image f σ)

Push barycentric coordinates forward along a vertex map, adding weights when vertices are identified. The resulting point lies in the simplex on the image vertex set.

Equations

• x.map f = ⟨Finsupp.mapDomain f ↑x, ⋯⟩

@[simp]

theorem AbstractSimplicialComplex.StandardSimplex.map_val {α : Type u_1} {β : Type u_2} [DecidableEq β] {σ : Finset α} (x : StandardSimplex σ) (f : α → β) : ↑(x.map f) = Finsupp.mapDomain f ↑x

The affine simplex map pushes forward its finitely supported coordinate vector.

theorem AbstractSimplicialComplex.StandardSimplex.map_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] {σ : Finset α} (x : StandardSimplex σ) (f : α → β) (b : β) : ↑(x.map f) b = ∑ a ∈ σ, if f a = b then ↑x a else 0

A target barycentric coordinate is the sum of the source coordinates mapping to it.

theorem AbstractSimplicialComplex.StandardSimplex.continuous_map {α : Type u_1} {β : Type u_2} [DecidableEq β] {σ : Finset α} (f : α → β) : Continuous fun (x : StandardSimplex σ) => x.map f

Affine pushforward between closed simplices is continuous for their coordinate topologies.

noncomputable def PreAbstractSimplicialComplex.SimplicialMap.realizationMap {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) : C(K.Realization, L.Realization)

The continuous map of weak realizations induced by a simplicial map, affine on each face.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_val {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (x : K.Realization) : ↑(f.realizationMap x) = Finsupp.mapDomain ⇑f ↑x

The induced map pushes forward barycentric coordinates, adding weights over each vertex fiber.

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_comp_faceInclusion {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (σ : TauCeti.SetLike.Face K) : ⇑f.realizationMap ∘ K.faceInclusion σ = L.faceInclusion ⟨Finset.image ⇑f ↑σ, ⋯⟩ ∘ fun (x : AbstractSimplicialComplex.StandardSimplex ↑σ) => x.map ⇑f

Restriction of the realization map to a face is its affine simplex map followed by the target face inclusion.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_vertex {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (a : α) : f.realizationMap (K.vertex a) = L.vertex (f a)

A simplicial map sends each realization vertex to the realization of its image vertex.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_id {α : Type u_1} {K : AbstractSimplicialComplex α} [DecidableEq α] : (id K.toPreAbstractSimplicialComplex).realizationMap = ContinuousMap.id K.Realization

Realization preserves the identity simplicial map.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {P : AbstractSimplicialComplex γ} (g : L.SimplicialMap P.toPreAbstractSimplicialComplex) (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) : (g.comp f).realizationMap = g.realizationMap.comp f.realizationMap

Realization preserves composition of simplicial maps.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_inclusion {α : Type u_1} {K : AbstractSimplicialComplex α} [DecidableEq α] {L : AbstractSimplicialComplex α} (h : K ≤ L) : ⇑(inclusion h).realizationMap = AbstractSimplicialComplex.realizationMap h

The simplicial realization of an inclusion agrees with the inclusion of polyhedra.

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationMap_injective_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) : Function.Injective ⇑f.realizationMap ↔ Function.Injective ⇑f

The realization map is injective exactly when its vertex map is injective.

noncomputable def PreAbstractSimplicialComplex.SimplicialMap.realizationHomeomorph {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} [DecidableEq α] (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (g : L.SimplicialMap K.toPreAbstractSimplicialComplex) (hgf : g.comp f = id K.toPreAbstractSimplicialComplex) (hfg : f.comp g = id L.toPreAbstractSimplicialComplex) : K.Realization ≃ₜ L.Realization

Mutually inverse simplicial maps induce a homeomorphism of their weak realizations.

Equations

• f.realizationHomeomorph g hgf hfg = { toFun := ⇑f.realizationMap, invFun := ⇑g.realizationMap, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationHomeomorph_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} [DecidableEq α] (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (g : L.SimplicialMap K.toPreAbstractSimplicialComplex) (hgf : g.comp f = id K.toPreAbstractSimplicialComplex) (hfg : f.comp g = id L.toPreAbstractSimplicialComplex) (x : K.Realization) : (f.realizationHomeomorph g hgf hfg) x = f.realizationMap x

The forward map of the realization homeomorphism is the given simplicial realization map.

@[simp]

theorem PreAbstractSimplicialComplex.SimplicialMap.realizationHomeomorph_symm_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} [DecidableEq α] (f : K.SimplicialMap L.toPreAbstractSimplicialComplex) (g : L.SimplicialMap K.toPreAbstractSimplicialComplex) (hgf : g.comp f = id K.toPreAbstractSimplicialComplex) (hfg : f.comp g = id L.toPreAbstractSimplicialComplex) (x : L.Realization) : (f.realizationHomeomorph g hgf hfg).symm x = g.realizationMap x

The inverse of the realization homeomorphism is the inverse simplicial realization map.