Finite-dimensional normed spaces

Over a complete nontrivially normed field every linear functional on a finite-dimensional normed space is continuous, so the continuous dual E →L[𝕜] 𝕜 coincides with the algebraic dual Module.Dual 𝕜 E. Mathlib records that coincidence as the linear equivalence LinearMap.toContinuousLinearMap; this file reads off the one consequence of it that dimension counts need, namely that the continuous dual has the same dimension as the space.

Two complements of the same space in a finite-dimensional space are continuously linearly isomorphic. This allows pointwise choices of complements to be identified with a single model.

Main results

• ContinuousLinearMap.dual_finrank_eq: in finite dimensions the continuous dual has the same dimension as the space.
• TauCeti.nonempty_continuousLinearEquiv_of_prod_continuousLinearEquiv: complements of the same space in a finite-dimensional space are isomorphic.
• TauCeti.continuous_det_div_conj: the determinant phase det A / conj (det A) of a continuous family of continuous linear automorphisms varies continuously.

theorem ContinuousLinearMap.dual_finrank_eq {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] : Module.finrank 𝕜 (E →L[𝕜] 𝕜) = Module.finrank 𝕜 E

In finite dimensions the continuous dual E →L[𝕜] 𝕜 has the same dimension as E: every linear functional on a finite-dimensional space is continuous, so the continuous dual coincides with the algebraic one.

theorem TauCeti.nonempty_continuousLinearEquiv_of_prod_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {V : Type u_3} {W : Type u_4} {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [AddCommGroup V] [TopologicalSpace V] [Module 𝕜 V] [AddCommGroup W] [TopologicalSpace W] [Module 𝕜 W] [FiniteDimensional 𝕜 W] {F' : Type u_6} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (e : (V × F) ≃L[𝕜] W) (e' : (V × F') ≃L[𝕜] W) : Nonempty (F ≃L[𝕜] F')

Over a complete field, two complements of the same space V in a finite-dimensional space W are continuously linearly isomorphic: both have dimension finrank W - finrank V.

theorem TauCeti.continuous_det_div_conj {𝕜 : Type u_3} {E : Type u_4} {X : Type u_5} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [StarRing 𝕜] [ContinuousStar 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace X] (A : X → E ≃L[𝕜] E) (hA : Continuous fun (x : X) => ↑(A x)) : Continuous fun (x : X) => LinearMap.det ↑↑(A x) / (starRingEnd 𝕜) (LinearMap.det ↑↑(A x))

The determinant phase det A / conj (det A) of a continuous family of continuous linear automorphisms varies continuously. Over ℂ this is the Maslov phase ρ(L, A L) of a maximal totally real subspace L.