The tangent space of a regular level set away from its base point

TauCeti.levelSetChart parametrizes the level set {x | f x = c} near a regular point a by the kernel of the derivative f' there, and TauCeti.hasStrictFDerivAt_coe_levelSetChart_symm computes the derivative of that parametrization at the chart origin: it is the inclusion of ker f' into the ambient space. At any other point of the chart the derivative need not be that inclusion, because the level set may have turned: its tangent space there is the kernel of the derivative of f at that point, which need not be the kernel at a.

This file computes the derivative at those other points. At a chart point k whose image z lies in HasStrictFDerivAt.implicitCoordSource, the neighbourhood on which the implicit-function coordinate map keeps an invertible derivative, the inverse chart is differentiable with derivative ContinuousLinearMap.kerSection A P, where A is the derivative of f at z and P is the projection chosen by the complementation hypothesis. That map is injective with range exactly ker A: the chart identifies the fixed model space ker f' with the moving tangent space of the level set, linearly and isomorphically.

Two consequences deserve naming on their own. The derivative of f is automatically surjective at every point of that neighbourhood (HasStrictFDerivAt.surjective_of_mem_implicitCoordSource), so "regular point" is not an extra hypothesis nearby; and the tangent space is therefore complemented, being the range of a section.

This is the pointwise input that turns a statement proved at one point of a Fredholm level set into a statement about a neighbourhood of it, which is what the parametric transversality package of McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3, needs: there the conclusion must hold at every nearby solution, not only at the one the chart is centred on.

Main results

• TauCeti.hasFDerivAt_coe_levelSetChart_symm_of_mem: the derivative of the inverse chart at a point of the coordinate neighbourhood is the kernel section of the derivative there.
• TauCeti.range_fderiv_coe_levelSetChart_symm_of_mem: its range is the kernel of that derivative, the tangent space of the level set.
• TauCeti.fderiv_coe_levelSetChart_symm_injective_of_mem: it is injective, so the chart is an immersion.

References

• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix A.3.

theorem TauCeti.hasFDerivAt_coe_levelSetChart_symm_of_mem {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E → F} {f' : E →L[K] F} {a : E} {c : F} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (ha : f a = c) {k : ↥(↑f').ker} (hk : k ∈ (levelSetChart hf hf' hker ha).target) (hmem : ↑(↑(levelSetChart hf hf' hker ha).symm k) ∈ hf.implicitCoordSource hf' hker) {A : E →L[K] F} (hA : HasFDerivAt f A ↑(↑(levelSetChart hf hf' hker ha).symm k)) : HasFDerivAt (fun (k : ↥(↑f').ker) => ↑(↑(levelSetChart hf hf' hker ha).symm k)) (A.kerSection (Classical.choose hker)) k

The derivative of the inverse regular-level-set chart away from its origin. At a chart point k whose image lies in the neighbourhood HasStrictFDerivAt.implicitCoordSource, the inverse chart is differentiable, with derivative the section ContinuousLinearMap.kerSection A (Classical.choose hker) of the derivative A of f there.

TauCeti.hasStrictFDerivAt_coe_levelSetChart_symm is the case k = 0, where A may be taken to be f' and the section is the inclusion of ker f'.

theorem TauCeti.fderiv_coe_levelSetChart_symm_of_mem {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E → F} {f' : E →L[K] F} {a : E} {c : F} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (ha : f a = c) {k : ↥(↑f').ker} (hk : k ∈ (levelSetChart hf hf' hker ha).target) (hmem : ↑(↑(levelSetChart hf hf' hker ha).symm k) ∈ hf.implicitCoordSource hf' hker) {A : E →L[K] F} (hA : HasFDerivAt f A ↑(↑(levelSetChart hf hf' hker ha).symm k)) : fderiv K (fun (k : ↥(↑f').ker) => ↑(↑(levelSetChart hf hf' hker ha).symm k)) k = A.kerSection (Classical.choose hker)

The Fréchet derivative of the inverse regular-level-set chart at a point of the coordinate neighbourhood.

theorem TauCeti.range_fderiv_coe_levelSetChart_symm_of_mem {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E → F} {f' : E →L[K] F} {a : E} {c : F} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (ha : f a = c) {k : ↥(↑f').ker} (hk : k ∈ (levelSetChart hf hf' hker ha).target) (hmem : ↑(↑(levelSetChart hf hf' hker ha).symm k) ∈ hf.implicitCoordSource hf' hker) {A : E →L[K] F} (hA : HasFDerivAt f A ↑(↑(levelSetChart hf hf' hker ha).symm k)) : (↑(fderiv K (fun (k : ↥(↑f').ker) => ↑(↑(levelSetChart hf hf' hker ha).symm k)) k)).range = (↑A).ker

The tangent space of a regular level set. The derivative of the inverse chart at a point of the coordinate neighbourhood has range exactly the kernel of the derivative of f there.

theorem TauCeti.fderiv_coe_levelSetChart_symm_injective_of_mem {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E → F} {f' : E →L[K] F} {a : E} {c : F} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (ha : f a = c) {k : ↥(↑f').ker} (hk : k ∈ (levelSetChart hf hf' hker ha).target) (hmem : ↑(↑(levelSetChart hf hf' hker ha).symm k) ∈ hf.implicitCoordSource hf' hker) {A : E →L[K] F} (hA : HasFDerivAt f A ↑(↑(levelSetChart hf hf' hker ha).symm k)) : Function.Injective ⇑(fderiv K (fun (k : ↥(↑f').ker) => ↑(↑(levelSetChart hf hf' hker ha).symm k)) k)

The inverse chart is an immersion: its derivative at a point of the coordinate neighbourhood is injective.