Continuous left inverses of injective operators

Mathlib's ContinuousLinearMap.HasLeftInverse records that a continuous linear map has a left inverse which is itself continuous and linear. This file adds two facts about it, and the corresponding statement for continuous pseudo-inverses.

• Over ℝ or ℂ, every continuous linear map f out of a finite-dimensional space has a continuous pseudo-inverse g, with f ∘ g ∘ f = f, whatever the locally convex codomain: its range is finite-dimensional, hence has a closed complement by the Hahn–Banach theorem. When f is injective, g is a continuous left inverse of f.
• Having a continuous left inverse is stable in families. If A x depends continuously on x and A x₀ has a continuous left inverse, then so does A x for x near x₀, and the left inverses can be chosen to depend continuously on x at x₀. If P is a left inverse of A x₀, then P ∘ A x is invertible near x₀, and (P ∘ A x)⁻¹ ∘ P is a left inverse of A x.

The second fact is what makes coordinates with respect to a moving family of linearly independent vectors depend continuously on the base point, as in the local trivializations of a subbundle spanned by local frames.

Main results

• ContinuousLinearMap.exists_comp_comp_eq_self: a continuous linear map out of a finite-dimensional space over ℝ or ℂ has a continuous pseudo-inverse.
• ContinuousLinearMap.HasLeftInverse.of_injective_of_finiteDimensional_domain: an injective continuous linear map out of a finite-dimensional space over ℝ or ℂ has a continuous left inverse.
• ContinuousAt.exists_continuousAt_leftInverse: continuously varying left inverses of a continuous family of operators whose member at x₀ has a continuous left inverse.

theorem ContinuousLinearMap.exists_comp_comp_eq_self {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {G : Type u_2} [TopologicalSpace G] [AddCommGroup G] [Module 𝕜 G] [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G] {F : Type u_3} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] [IsRCLikeNormedField 𝕜] [PolynormableSpace 𝕜 F] [FiniteDimensional 𝕜 G] (f : G →L[𝕜] F) : ∃ (g : F →L[𝕜] G), f ∘SL g ∘SL f = f

Over ℝ or ℂ, a continuous linear map f out of a finite-dimensional space into a locally convex (polynormable) space has a continuous pseudo-inverse: a continuous linear map g in the opposite direction with f ∘ g ∘ f = f. This is the continuous counterpart of LinearMap.exists_comp_comp_eq_self.

theorem ContinuousLinearMap.HasLeftInverse.of_injective_of_finiteDimensional_domain {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {G : Type u_2} [TopologicalSpace G] [AddCommGroup G] [Module 𝕜 G] [IsTopologicalAddGroup G] [ContinuousSMul 𝕜 G] {F : Type u_3} [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] [IsRCLikeNormedField 𝕜] [PolynormableSpace 𝕜 F] [FiniteDimensional 𝕜 G] {f : G →L[𝕜] F} (hf : Function.Injective ⇑f) : f.HasLeftInverse

Over ℝ or ℂ, an injective continuous linear map out of a finite-dimensional space into a locally convex (polynormable) space has a continuous left inverse: any continuous pseudo-inverse g of f (ContinuousLinearMap.exists_comp_comp_eq_self) is one, since f (g (f v)) = f v.

theorem ContinuousAt.exists_continuousAt_leftInverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {X : Type u_4} [TopologicalSpace X] {A : X → G →L[𝕜] F} {x₀ : X} (hA : ContinuousAt A x₀) (h : (A x₀).HasLeftInverse) : ∃ (L : X → F →L[𝕜] G), ContinuousAt L x₀ ∧ ∀ᶠ (x : X) in nhds x₀, Function.LeftInverse ⇑(L x) ⇑(A x)

Left inverses vary continuously. Let A x be a continuous linear map depending continuously on x at x₀, into a normed space from a Banach space. If A x₀ has a continuous left inverse, then there are continuous linear maps L x, depending continuously on x at x₀, such that L x is a left inverse of A x for all x near x₀.