Differentiability of coordinates for quotients by varying ranges

A continuous family of split injections admits a single complementary subspace on a neighbourhood of each parameter. In these coordinates, the quotient by the moving range has a fixed model fibre, and its coordinate operator has the same differentiability as the original family. Coordinate changes inherit this regularity as well.

Applied to the differential of an immersion in manifold charts, this supplies local models for intrinsic normal fibres without choosing a Riemannian metric. The fibre equivalence is ContinuousLinearMap.quotientRangeEquiv; differentiability is expressed on ambient representatives so it does not presuppose a differentiable structure on the total quotient bundle.

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

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

Complementary coordinate operators inherit the differentiability of a varying range parametrization at every parameter where the fixed complement is valid.

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

Complementary coordinate operators are C^n at valid parameters for a C^n family.

theorem ContDiffOn.quotientRangeCoordinate {𝕜 : Type u_1} {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X → E →L[𝕜] F} {s : Set X} {n : WithTop ℕ∞} [CompleteSpace (E × G)] (hA : ContDiffOn 𝕜 n A s) (B : G →L[𝕜] F) (h : ∀ x ∈ s, ((A x).coprod B).IsInvertible) : ContDiffOn 𝕜 n (fun (y : X) => (A y).quotientRangeCoordinate B) s

Complementary coordinates are C^n throughout an invertibility domain for a C^n family.

theorem ContDiffOn.exists_contDiffOn_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] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X → E →L[𝕜] F} {x : X} {s : Set X} {n : WithTop ℕ∞} [CompleteSpace F] (hA : ContDiffOn 𝕜 n A s) (hs : IsOpen s) (hx : x ∈ s) (h : (A x).HasLeftInverse) : ∃ (Q : Submodule 𝕜 F), IsClosed ↑Q ∧ ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ U ⊆ s ∧ (∀ y ∈ U, ((A y).coprod Q.subtypeL).IsInvertible) ∧ ContDiffOn 𝕜 n (fun (y : X) => (A y).quotientRangeCoordinate Q.subtypeL) U

A C^n family of operators which is split injective at one parameter admits C^n quotient coordinates with a fixed closed model fibre near that parameter. The neighbourhood is contained in the original open parameter domain.