The inclusion of a regular level set

Let f : E → F be a map between Banach spaces which, along the level set {x | f x = c}, is strictly differentiable with surjective Fredholm derivative D x of constant index n. TauCeti.levelSetChartedSpace makes the level set a charted space modelled on Fin n → 𝕜, and TauCeti.isManifold_levelSet makes it a C^m manifold when f is C^m along the level set.

TauCeti.hasMFDerivAt_coe_levelSet computes the differential of the inclusion of the level set into E for that atlas: at z it is the inclusion of ker (D z), read in the model space through ContinuousLinearMap.kerModelEquiv. This file deduces that the inclusion is an immersion, and that its tangent space at z is ker (D z). These are the facts needed to restrict functions on E to the level set and to compare their differentials, for instance to pull back a function along the inclusion and compute its critical points.

Main results

• TauCeti.injective_mfderiv_coe_levelSet and TauCeti.range_mfderiv_coe_levelSet: the differential of the inclusion is injective, with range ker (D z).
• ContMDiff.codRestrict_levelSet: a smooth map into E with values in the level set is a smooth map into the level set.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition (2013), Corollary 5.14 and Proposition 5.38, for regular level sets and their tangent spaces.

theorem TauCeti.injective_mfderiv_coe_levelSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {c : F} {D : E → E →L[𝕜] F} {n : ℕ} (hf : ∀ x ∈ {x : E | f x = c}, HasStrictFDerivAt f (D x) x) (hFred : ∀ x ∈ {x : E | f x = c}, (D x).IsFredholm) (hsurj : ∀ x ∈ {x : E | f x = c}, Function.Surjective ⇑(D x)) (hindex : ∀ x ∈ {x : E | f x = c}, (D x).index = ↑n) (z : ↑{x : E | f x = c}) : Function.Injective ⇑(mfderiv% Subtype.val z)

The differential of the inclusion of a regular level set is injective: the inclusion is an immersion.

theorem TauCeti.range_mfderiv_coe_levelSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {c : F} {D : E → E →L[𝕜] F} {n : ℕ} (hf : ∀ x ∈ {x : E | f x = c}, HasStrictFDerivAt f (D x) x) (hFred : ∀ x ∈ {x : E | f x = c}, (D x).IsFredholm) (hsurj : ∀ x ∈ {x : E | f x = c}, Function.Surjective ⇑(D x)) (hindex : ∀ x ∈ {x : E | f x = c}, (D x).index = ↑n) (z : ↑{x : E | f x = c}) : (↑(mfderiv% Subtype.val z)).range = (↑(D ↑z)).ker

The tangent space of a regular level set is the kernel of the derivative. The range of the differential at z of the inclusion of a regular level set is ker (D z).

theorem ContMDiff.codRestrict_levelSet {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {c : F} {D : E → E →L[𝕜] F} {n : ℕ} (hf : ∀ x ∈ {x : E | f x = c}, HasStrictFDerivAt f (D x) x) (hFred : ∀ x ∈ {x : E | f x = c}, (D x).IsFredholm) (hsurj : ∀ x ∈ {x : E | f x = c}, Function.Surjective ⇑(D x)) (hindex : ∀ x ∈ {x : E | f x = c}, (D x).index = ↑n) {E' : Type u_4} {H : Type u_5} {M : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E' H} [TopologicalSpace M] [ChartedSpace H M] {m : WithTop ℕ∞} {g : M → E} (hg : ContMDiff I (modelWithCornersSelf 𝕜 E) m g) (hgc : ∀ (x : M), f (g x) = c) : ContMDiff I (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) m fun (x : M) => ⟨g x, ⋯⟩

Maps into a regular level set. A C^m map into E with values in the level set is a C^m map into the level set.