Linear isotopies fixing the origin

A real linear map with positive determinant on a finite-dimensional normed space is smoothly isotopic to the identity through linear automorphisms. The motion fixes the origin at every time. More generally, two linear equivalences with orientation-preserving relative map are smoothly isotopic, even when their source and target are different normed spaces. This is the linear step in the disc theorem, before transporting and extending the isotopy in an ambient manifold.

The smooth family comes from ContinuousLinearMap.exists_contDiff_det_pos, which uses transvection generation and a positive diagonal factor.

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

theorem ContinuousLinearEquiv.exists_smoothIsotopy_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : E ≃L[ℝ] E) (hL : 0 < (↑L).det) : ∃ (F : TauCeti.SmoothIsotopy ContMDiffMap.id ↑L.toDiffeomorph), (∀ (t : ↑unitInterval), F (t, 0) = 0) ∧ ∀ (t : ↑unitInterval), ∃ (A : E ≃L[ℝ] E), 0 < (↑A).det ∧ ∀ (x : E), F (t, x) = A x

A positive-determinant linear map is smoothly isotopic to the identity, fixing the origin throughout the motion. The time slices are linear automorphisms with positive determinant.

theorem ContinuousLinearEquiv.exists_smoothIsotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L₀ L₁ : E ≃L[ℝ] F) (hL : 0 < (↑(L₀.trans L₁.symm)).det) : ∃ (G : TauCeti.SmoothIsotopy (TauCeti.SmoothEmbedding.ofContinuousLinearEquiv L₀).toContMDiffMap (TauCeti.SmoothEmbedding.ofContinuousLinearEquiv L₁).toContMDiffMap), ∀ (t : ↑unitInterval), G (t, 0) = 0

Linear equivalences with orientation-preserving relative map are smoothly isotopic, fixing the origin. The source is finite-dimensional; the target need not be given an orientation.