Homotopy groups of a real topological vector space

Any two generalized loops with the same basepoint in a real topological vector space are homotopic relative to the cube boundary: Mathlib's affine homotopy ContinuousMap.Homotopy.affine, which interpolates linearly at each point of the cube, is constant at the basepoint on the boundary. Consequently every homotopy group of such a space is a subsingleton.

Main declarations

• GenLoop.homotopic_of_topologicalVectorSpace: generalized loops in a real topological vector space with the same basepoint are homotopic.
• HomotopyGroup.subsingleton_of_topologicalVectorSpace: all homotopy groups of a real topological vector space are subsingletons.

theorem GenLoop.homotopic_of_topologicalVectorSpace {N : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {x : E} (f g : ↑(GenLoop N E x)) : Homotopic f g

Any two generalized loops based at the same point in a real topological vector space are homotopic relative to the cube boundary. The homotopy is pointwise linear interpolation.

instance HomotopyGroup.subsingleton_of_topologicalVectorSpace {N : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {x : E} : Subsingleton (HomotopyGroup N E x)

Every homotopy group of a real topological vector space is a subsingleton. This includes dimension zero: a real topological vector space is path connected.