Smooth paths of real matrices with positive determinant

Over any nontrivially normed field, a special-linear matrix admits a smooth determinant-one family from the identity, parameterized by the field.

Every real matrix with positive determinant is joined to the identity by a smooth family of matrices with positive determinant, defined on all of ℝ. First use generation by elementary transvections to construct a determinant-one family. Then restore the determinant by multiplying one coordinate by exp (t * log (det A)). This also covers the zero-dimensional space.

Such families give linear isotopies fixing the origin, the linear step in the disc theorem.

The algebraic input is the transvection generation theorem Matrix.SpecialLinearGroup.closure_range_toSpecialLinearGroup_eq_top_of_field. Reference: M. Hirsch, Differential Topology, Chapter 4, §6, Theorem 6.6.

theorem Matrix.SpecialLinearGroup.exists_contDiff_det_eq_one {𝕜 : Type u_1} {ι : Type u_2} [NontriviallyNormedField 𝕜] [Fintype ι] [DecidableEq ι] (A : SpecialLinearGroup ι 𝕜) : ∃ (γ : 𝕜 → Matrix ι ι 𝕜), ContDiff 𝕜 (↑⊤) γ ∧ γ 0 = 1 ∧ γ 1 = ↑A ∧ ∀ (t : 𝕜), (γ t).det = 1

A special-linear matrix over a nontrivially normed field admits a smooth matrix family from the identity whose determinant is one for every parameter in the field.

theorem Matrix.exists_contDiff_det_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) (hA : 0 < A.det) : ∃ (γ : ℝ → Matrix ι ι ℝ), ContDiff ℝ (↑⊤) γ ∧ γ 0 = 1 ∧ γ 1 = A ∧ ∀ (t : ℝ), 0 < (γ t).det

A real matrix with positive determinant is joined to the identity by a smooth family with positive determinant at every real parameter. No positive-dimensional assumption is needed.