Contraction of realized cones

If {v} is a face and adjoining v to every face gives another face, the weak realization contracts onto v. The contraction is affine in barycentric coordinates and fixes the apex throughout. No finiteness or local finiteness is needed: joint continuity follows from the closed-simplex cylinder criterion in Realization.Homotopy.

This supplies actual nullhomotopies for maps into cones, rather than only vanishing homotopy groups. In particular the realization of the combinatorial cone on any abstract simplicial complex is contractible.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 2 (cones and polyhedra).

noncomputable def AbstractSimplicialComplex.coneContraction {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} (h : K.IsCone v) : (ContinuousMap.id K.Realization).HomotopyRel (ContinuousMap.const K.Realization (K.vertex v)) {K.vertex v}

The affine contraction of a weak realized cone onto its apex, relative to the apex. At time t the coordinate vector is (1 - t) • x + t • single v 1.

@[simp]

theorem AbstractSimplicialComplex.coneContraction_val {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} (h : K.IsCone v) (t : ↑unitInterval) (x : K.Realization) : ↑((coneContraction h) (t, x)) = (1 - ↑t) • ↑x + ↑t • Finsupp.single v 1

The coordinate formula characterizing the cone contraction.

@[simp]

theorem AbstractSimplicialComplex.coneContraction_vertex {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} (h : K.IsCone v) (t : ↑unitInterval) : (coneContraction h) (t, K.vertex v) = K.vertex v

The contraction fixes the apex at every time.

theorem AbstractSimplicialComplex.contractibleSpace_realization_of_isCone {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} (h : K.IsCone v) : ContractibleSpace K.Realization

The weak realization of a cone is contractible, without any finiteness hypothesis.

theorem AbstractSimplicialComplex.contractibleSpace_realization_cone {ι : Type u_1} (K : AbstractSimplicialComplex ι) : ContractibleSpace K.cone.Realization

The realization of the combinatorial cone on any abstract complex is contractible.