The realization map of a barycentric subdivision

Every vertex of the barycentric subdivision of a simplicial complex K is a nonempty face of K. Send that vertex to the barycenter of its face and extend affinely over every simplex. Since the faces indexing a subdivision simplex form a chain, all their barycenters lie in the largest face in that chain. The affine extension therefore lands in the realization of K.

This file constructs that canonical continuous map. It is the forward map in the homeomorphism between the realizations of a complex and its barycentric subdivision required by Layer 11 of the GeometricTopology roadmap. The inverse is constructed and proved continuous in Subdivision.Homeomorph.

The construction follows Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2, "Derived Subdivisions".

Main definitions

• AbstractSimplicialComplex.barycentricSubdivisionRealizationMap: the canonical continuous map from the realization of the barycentric subdivision to the original realization.

Main results

• AbstractSimplicialComplex.barycentricSubdivisionRealizationMap_vertex: a subdivision vertex maps to the barycenter of the face it represents.
• AbstractSimplicialComplex.barycentricSubdivisionLinearMap_apply: the coordinates of a linear combination of face barycenters.

noncomputable def AbstractSimplicialComplex.barycentricSubdivisionLinearMap {ι : Type u_1} (K : AbstractSimplicialComplex ι) : (TauCeti.SetLike.Face K →₀ ℝ) →ₗ[ℝ] ι →₀ ℝ

The linear extension which sends every subdivision vertex to its face barycenter. The restriction of this map to the subdivision realization lands in the original realization.

Equations

• K.barycentricSubdivisionLinearMap = Finsupp.linearCombination ℝ K.faceBarycenter

@[simp]

theorem AbstractSimplicialComplex.barycentricSubdivisionLinearMap_single {ι : Type u_1} (K : AbstractSimplicialComplex ι) (σ : TauCeti.SetLike.Face K) : K.barycentricSubdivisionLinearMap (Finsupp.single σ 1) = K.faceBarycenter σ

theorem AbstractSimplicialComplex.barycentricSubdivisionLinearMap_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) (a : TauCeti.SetLike.Face K →₀ ℝ) (v : ι) : (K.barycentricSubdivisionLinearMap a) v = ∑ σ ∈ a.support, a σ * if v ∈ ↑σ then (↑(↑σ).card)⁻¹ else 0

The coordinates of a linear combination of face barycenters.

noncomputable def AbstractSimplicialComplex.barycentricSubdivisionRealizationMap {ι : Type u_1} (K : AbstractSimplicialComplex ι) : (TauCeti.PreAbstractSimplicialComplex.barycentricSubdivision K.toPreAbstractSimplicialComplex).Realization → K.Realization

The canonical map from the realization of the barycentric subdivision of K to the realization of K. It sends each face-vertex to that face's barycenter and is affine on each subdivision simplex.

Equations

• K.barycentricSubdivisionRealizationMap x = ⟨K.barycentricSubdivisionLinearMap ↑x, ⋯⟩

@[simp]

theorem AbstractSimplicialComplex.barycentricSubdivisionRealizationMap_val {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : (TauCeti.PreAbstractSimplicialComplex.barycentricSubdivision K.toPreAbstractSimplicialComplex).Realization) : ↑(K.barycentricSubdivisionRealizationMap x) = K.barycentricSubdivisionLinearMap ↑x

The realization map has the expected underlying affine formula.

theorem AbstractSimplicialComplex.barycentricSubdivisionRealizationMap_vertex {ι : Type u_1} (K : AbstractSimplicialComplex ι) (σ : TauCeti.SetLike.Face K) : ↑(K.barycentricSubdivisionRealizationMap ((TauCeti.PreAbstractSimplicialComplex.barycentricSubdivision K.toPreAbstractSimplicialComplex).vertex σ)) = K.faceBarycenter σ

A vertex of the barycentric subdivision maps to the barycenter of the original face it represents.

theorem AbstractSimplicialComplex.continuous_barycentricSubdivisionRealizationMap {ι : Type u_1} (K : AbstractSimplicialComplex ι) : Continuous K.barycentricSubdivisionRealizationMap

The barycentric-subdivision realization map is continuous for the weak topologies on both realizations.