Fixed complements to nearby operator ranges

A continuous family of split injections with a complete ambient space has a single closed complement to its ranges near each parameter. The complement parametrizes all nearby quotients through ContinuousLinearMap.quotientRangeEquiv. This is the local linear input for quotient bundles, such as the intrinsic normal bundle of an immersion.

The proof uses Mathlib's ContinuousLinearEquiv.equivOfRightInverse and openness of invertibility. Completeness of the nearby complements — the complete model fibres above — follows from ContinuousLinearMap.completeSpace_of_isInvertible, which transfers completeness of the codomain back to the domain of an invertible operator. Complementary coordinate operators are continuous on a domain of valid splittings, using Mathlib's regularity of operator inversion.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, the normal-bundle construction preceding Theorem 6.24.

theorem ContinuousAt.exists_isInvertible_coprod_subtypeL {𝕜 : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace X] [CompleteSpace F] {A : X → E →L[𝕜] F} {x₀ : X} (hA : ContinuousAt A x₀) (h₀ : (A x₀).HasLeftInverse) : ∃ (Q : Submodule 𝕜 F), IsClosed ↑Q ∧ ∃ (U : Set X), IsOpen U ∧ x₀ ∈ U ∧ ∀ x ∈ U, ((A x).coprod Q.subtypeL).IsInvertible

A fixed complement to a split injection still parametrizes the quotient by every sufficiently nearby range. The source and ambient spaces may be infinite dimensional.

theorem ContinuousAt.quotientRangeCoordinate {𝕜 : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [TopologicalSpace X] [CompleteSpace (E × G)] {A : X → E →L[𝕜] F} {x : X} (hA : ContinuousAt A x) (B : G →L[𝕜] F) (h : ((A x).coprod B).IsInvertible) : ContinuousAt (fun (y : X) => (A y).quotientRangeCoordinate B) x

Complementary coordinate operators are continuous at a parameter where the operator family is continuous and the fixed complement is valid.

theorem Continuous.quotientRangeCoordinate {𝕜 : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [TopologicalSpace X] [CompleteSpace (E × G)] {A : X → E →L[𝕜] F} (hA : Continuous A) (B : G →L[𝕜] F) (h : ∀ (x : X), ((A x).coprod B).IsInvertible) : Continuous fun (x : X) => (A x).quotientRangeCoordinate B

A continuous operator family with a fixed valid complement has continuous complementary coordinate operators. The parameter space need only be topological.