Nondegeneracy of the bilinear form of a continuous linear map into the dual

A continuous linear map L : E →L[𝕜] E →L[𝕜] 𝕜 carries a bilinear form ContinuousLinearMap.toBilinForm L, and that form is left-separating exactly when L is injective: both say that no nonzero vector is annihilated by L. Reading nondegeneracy of the form off injectivity of the map is the step that connects the two ways a Hessian is presented — as a map into the dual space and as a bilinear form — and it has nothing to do with the analysis that produces the Hessian, so it is recorded here, next to ContinuousLinearMap.toBilinForm itself, rather than with any of its users.

Main results

• ContinuousLinearMap.separatingLeft_toBilinForm_iff_injective: the bilinear form of a continuous linear map into the dual is left-separating if and only if the map is injective.
• ContinuousLinearMap.isInvertible_of_injective and ContinuousLinearMap.isInvertible_of_surjective: in finite dimensions an injective, equivalently a surjective, map into the dual is already invertible, the dual having the same dimension as the space (ContinuousLinearMap.dual_finrank_eq).

theorem ContinuousLinearMap.separatingLeft_toBilinForm_iff_injective {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (L : E →L[𝕜] E →L[𝕜] 𝕜) : LinearMap.SeparatingLeft L.toBilinForm ↔ Function.Injective ⇑L

The bilinear form of a continuous linear map into the dual space is left-separating exactly when the map is injective.

theorem ContinuousLinearMap.isInvertible_of_injective {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {L : E →L[𝕜] E →L[𝕜] 𝕜} (hinj : Function.Injective ⇑L) : L.IsInvertible

In finite dimensions an injective continuous linear map into the dual is invertible: injectivity makes it a linear equivalence onto its range, and the dual has the same finite dimension as the space, so that range is everything.

theorem ContinuousLinearMap.isInvertible_of_surjective {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {L : E →L[𝕜] E →L[𝕜] 𝕜} (hsurj : Function.Surjective ⇑L) : L.IsInvertible

In finite dimensions a surjective continuous linear map into the dual is invertible: the dual has the same finite dimension as the space, so surjectivity forces injectivity.