Smooth paths of orientation-preserving linear maps

Transport the smooth positive-determinant matrix path through a finite basis. The resulting family of continuous linear maps starts at the identity, ends at the given map, and remains invertible for every real parameter. It supplies linear isotopies fixing the origin.

Reference: M. Hirsch, Differential Topology, Chapter 4, §6, Theorem 6.6.

theorem ContinuousLinearMap.exists_contDiff_det_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : E →L[ℝ] E) (hL : 0 < L.det) : ∃ (γ : ℝ → E →L[ℝ] E), ContDiff ℝ (↑⊤) γ ∧ γ 0 = ContinuousLinearMap.id ℝ E ∧ γ 1 = L ∧ ∀ (t : ℝ), 0 < (γ t).det

A real continuous linear map of positive determinant admits a smooth path from the identity through linear maps of positive determinant, on the whole real parameter line.