The punctured circle contracts onto a point

The circle with the point -1 removed deformation retracts onto 1: for z ≠ -1 the chord from z to 1 never meets the closed negative real axis, in particular never meets 0, so its radial projection back to the circle is a path from z to 1 avoiding -1. These paths depend continuously on z and are constant at z = 1, which gives a homotopy relative to {1} from the identity of Circle ∖ {-1} to the constant map at 1.

A deformation retraction of a neighbourhood of the base point onto it is what the computation of the fundamental group of a wedge of circles needs from each circle.

Main declarations

• TauCeti.circleChordHomotopy: the deformation retraction of Circle ∖ {-1} onto 1, with TauCeti.coe_circleChordHomotopy_apply its formula.

noncomputable def TauCeti.circleChordHomotopy : (ContinuousMap.id ↑{z : Circle | z ≠ -1}).HomotopyRel (ContinuousMap.const ↑{z : Circle | z ≠ -1} ⟨1, ⋯⟩) {⟨1, ⋯⟩}

Circle ∖ {-1} deformation retracts onto 1: at time t a point z ≠ -1 is moved to the radial projection of the point (1 - t) z + t of the chord from z to 1 (TauCeti.coe_circleChordHomotopy_apply). The homotopy fixes 1 throughout.

Equations

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

@[simp]

theorem TauCeti.coe_circleChordHomotopy_apply (t : ↑unitInterval) (z : ↑{z : Circle | z ≠ -1}) : ↑↑(circleChordHomotopy (t, z)) = NormedSpace.normalize (↑(1 - ↑t) * ↑↑z + ↑↑t)