Smoothly varying left inverses

Let 𝕜 → 𝕜' be a normed field extension. Let A x be a continuous 𝕜'-linear map from a Banach space G to a normed space F, depending C^n over 𝕜 on a point x of a manifold. If A x₀ has a continuous left inverse P, then the compression P ∘ A x is the identity at x₀, hence invertible near x₀, and (P ∘ A x)⁻¹ ∘ P is a left inverse of A x for x near x₀. Operator inversion is analytic over the ground field on the invertible operators, so this left inverse is again C^n over 𝕜 at x₀, while retaining its 𝕜'-linearity. The supplied ground-field scalar structures are preserved. This is the smooth counterpart of ContinuousAt.exists_continuousAt_leftInverse.

For G = (𝕜')ᵏ and A x the operator c ↦ ∑ i, c i • X i x of a family of linearly independent vectors depending smoothly on x, the left inverse sends a vector of the span of the X i x to its coordinates. So coordinates in a smoothly moving basis depend smoothly on the base point, which is what makes the local trivializations of a subbundle spanned by smooth local frames smoothly compatible.

Main results

• ContMDiffAt.exists_contMDiffAt_leftInverse: C^n varying left inverses of a C^n family of operators whose member at x₀ has a continuous left inverse.
• ContMDiffAt.of_clm_apply: regularity can be tested after a smoothly varying split injection.
• ContMDiffOn.exists_isOpen_contMDiffOn_sub_comp_inverse_comp: near a point where a left inverse compresses a smooth family of operators to the identity, the projections of a fixed covector annihilating the central member are smooth and nonzero, and the compression stays invertible, on an open neighborhood.

theorem ContMDiffAt.exists_contMDiffAt_leftInverse {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {EM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_4} [TopologicalSpace HM] {I : ModelWithCorners 𝕜 EM HM} {M : Type u_5} [TopologicalSpace M] [ChartedSpace HM M] {G : Type u_6} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜' G] [IsScalarTower 𝕜 𝕜' G] [CompleteSpace G] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {A : M → G →L[𝕜'] F} {x₀ : M} (hA : ContMDiffAt I (modelWithCornersSelf 𝕜 (G →L[𝕜'] F)) n A x₀) (h : (A x₀).HasLeftInverse) : ∃ (L : M → F →L[𝕜'] G), ContMDiffAt I (modelWithCornersSelf 𝕜 (F →L[𝕜'] G)) n L x₀ ∧ ∀ᶠ (x : M) in nhds x₀, Function.LeftInverse ⇑(L x) ⇑(A x)

Left inverses vary smoothly. Let A x be a continuous linear map into a normed space from a Banach space, linear over the extension field 𝕜' and depending C^n over the ground field 𝕜 on a manifold point x at x₀. If A x₀ has a continuous 𝕜'-linear left inverse, then there are continuous 𝕜'-linear maps L x, depending C^n over 𝕜 on x at x₀, such that L x is a left inverse of A x for all x near x₀.

theorem ContMDiffAt.of_clm_apply {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {EM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_4} [TopologicalSpace HM] {I : ModelWithCorners 𝕜 EM HM} {M : Type u_5} [TopologicalSpace M] [ChartedSpace HM M] {G : Type u_6} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedSpace 𝕜' G] [IsScalarTower 𝕜 𝕜' G] [CompleteSpace G] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {n : WithTop ℕ∞} {A : M → G →L[𝕜'] F} {v : M → G} {x₀ : M} (hAv : ContMDiffAt I (modelWithCornersSelf 𝕜 F) n (fun (x : M) => (A x) (v x)) x₀) (hA : ContMDiffAt I (modelWithCornersSelf 𝕜 (G →L[𝕜'] F)) n A x₀) (h : (A x₀).HasLeftInverse) : ContMDiffAt I (modelWithCornersSelf 𝕜 G) n v x₀

Ground-field smoothness can be tested after a smoothly varying extension-linear split injection. No regularity of v is assumed in advance.

theorem ContMDiffOn.exists_isOpen_contMDiffOn_sub_comp_inverse_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {EM : Type u_3} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_4} [TopologicalSpace HM] {I : ModelWithCorners 𝕜 EM HM} {M : Type u_5} [TopologicalSpace M] [ChartedSpace HM M] {G : Type u_6} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G] {F : Type u_7} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {A : M → G →L[𝕜] F} {S : Set M} (hA : ContMDiffOn I (modelWithCornersSelf 𝕜 (G →L[𝕜] F)) n A S) (hS : IsOpen S) {x : M} (hxS : x ∈ S) {P : F →L[𝕜] G} (hP : Function.LeftInverse ⇑P ⇑(A x)) {a : F →L[𝕜] 𝕜} (ha : a ≠ 0) (haA : a ∘SL A x = 0) : ∃ (W : Set M), IsOpen W ∧ x ∈ W ∧ W ⊆ S ∧ ContMDiffOn I (modelWithCornersSelf 𝕜 (F →L[𝕜] 𝕜)) n (fun (y : M) => a - a ∘SL A y ∘SL (P ∘SL A y).inverse ∘SL P) W ∧ ∀ y ∈ W, (P ∘SL A y).IsInvertible ∧ a - a ∘SL A y ∘SL (P ∘SL A y).inverse ∘SL P ≠ 0

Near a point where a smooth family of operators A y : G → F is compressed by a left inverse P to the identity and a is a covector killing A x, the covectors a - a (A y) (P (A y))⁻¹ P are smooth and nonzero, and the compression P (A y) is invertible, on an open neighborhood of x inside the domain of smoothness. They annihilate A y by ContinuousLinearMap.sub_comp_inverse_comp_comp_eq_zero.