Assembling an atlas of vertex-star charts

Charts on all open vertex stars give a charted-space structure on the weak polyhedron. The preferred chart at a point uses a vertex with positive barycentric coordinate. In particular, the preferred chart at a vertex is its own vertex-star chart.

The atlas is exactly the supplied family. Consequently, checking its compatibility with a structure groupoid amounts to checking the transitions between these charts. The model space and the vertex type are arbitrary; neither finiteness nor countability is required. Local sphere or ball models can supply the charts, independently of their subsequent smooth or piecewise-linear compatibility.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2–3 (vertex-star atlases).

@[instance_reducible]

noncomputable def AbstractSimplicialComplex.starChartedSpace {ι : Type u_1} {H : Type u_2} [TopologicalSpace H] (K : AbstractSimplicialComplex ι) (e : ι → OpenPartialHomeomorph K.Realization H) (hs : ∀ (v : ι), (e v).source = K.openStarRealization v) : ChartedSpace H K.Realization

Assemble charts whose sources are all the open vertex stars into an atlas on the existing weak realization topology. At each point, use a vertex with positive coordinate.

@[simp]

theorem AbstractSimplicialComplex.starChartedSpace_atlas {ι : Type u_1} {H : Type u_2} [TopologicalSpace H] (K : AbstractSimplicialComplex ι) (e : ι → OpenPartialHomeomorph K.Realization H) (hs : ∀ (v : ι), (e v).source = K.openStarRealization v) : atlas H K.Realization = Set.range e

The atlas consists exactly of the supplied vertex-star charts.

theorem AbstractSimplicialComplex.starChartedSpace_chartAt {ι : Type u_1} {H : Type u_2} [TopologicalSpace H] (K : AbstractSimplicialComplex ι) (e : ι → OpenPartialHomeomorph K.Realization H) (hs : ∀ (v : ι), (e v).source = K.openStarRealization v) (x : K.Realization) : chartAt H x = e ⋯.choose

The preferred chart uses a vertex whose coordinate at the point is positive.

@[simp]

theorem AbstractSimplicialComplex.starChartedSpace_chartAt_vertex {ι : Type u_1} {H : Type u_2} [TopologicalSpace H] (K : AbstractSimplicialComplex ι) (e : ι → OpenPartialHomeomorph K.Realization H) (hs : ∀ (v : ι), (e v).source = K.openStarRealization v) (v : ι) : chartAt H (K.vertex v) = e v

At a vertex, the preferred chart is the supplied chart for that vertex.