The realization homeomorphism for barycentric subdivision

The canonical map from the realization of the barycentric subdivision of a simplicial complex to the realization of the original complex is a homeomorphism. The forward map sends a face-vertex to the barycenter of that face and extends affinely over subdivision simplices.

Continuity of the inverse is proved simplex by simplex, using the weak topology on realizations. Each original simplex is covered by the finitely many closed chambers obtained by ordering its barycentric coordinates. On one chamber the inverse has a fixed affine formula: cardinality-scaled consecutive coordinate differences are the coefficients of the nested initial faces in that order. These formulas are continuous and agree on chamber intersections because the forward map is injective. Sorting the coordinates only establishes that the chambers cover the simplex; the chosen order need not vary continuously with the point.

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

Main definition

• AbstractSimplicialComplex.barycentricSubdivisionRealizationHomeomorph: the canonical homeomorphism from the realization of the barycentric subdivision to the original realization.

noncomputable def AbstractSimplicialComplex.barycentricSubdivisionRealizationHomeomorph {ι : Type u_1} (K : AbstractSimplicialComplex ι) : (TauCeti.PreAbstractSimplicialComplex.barycentricSubdivision K.toPreAbstractSimplicialComplex).Realization ≃ₜ K.Realization

The canonical homeomorphism from the realization of the barycentric subdivision of K to the realization of K. It sends every face-vertex to the barycenter of that face.

Equations

• K.barycentricSubdivisionRealizationHomeomorph = { toEquiv := Equiv.ofBijective K.barycentricSubdivisionRealizationMap ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

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

The subdivision realization homeomorphism has the canonical affine map as its forward map.