Universal level sets of Fredholm families

Let f : E × Λ → F be a parametrized equation. At a zero (x, l), write its derivative as D₁.coprod D₂, where D₁ differentiates in the E direction and D₂ in the parameter direction. The implicit function theorem locally parametrizes the universal zero set near (x, l) once the total derivative is surjective and its kernel is topologically complemented.

The main result of this file obtains that complemented-kernel hypothesis from the condition used in Fredholm transversality: D₁ is Fredholm and D₁.coprod D₂ is surjective. The proof splits the finite-dimensional cokernel of D₁ using parameter directions, and then solves the remaining range component using a Fredholm decomposition. Thus it does not assume that the universal zero set already has a manifold chart.

This is the splitting step in the parametric transversality package of McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3. The resulting complement feeds Mathlib's complemented-kernel implicit function theorem, while ContinuousLinearMap.parameterProj describes the derivative of the projection from the universal zero set to the parameter space.

Main results

• ContinuousLinearMap.IsFredholm.hasRightInverse_coprod: a surjective total linearization whose fixed-parameter part is Fredholm admits a continuous linear right inverse.
• ContinuousLinearMap.IsFredholm.closedComplemented_ker_coprod: consequently, the kernel of the total linearization is topologically complemented.

References

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

theorem ContinuousLinearMap.IsFredholm.hasRightInverse_coprod {𝕜 : Type u_1} {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup Λ] [NormedSpace 𝕜 Λ] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {D₁ : E →L[𝕜] F} {D₂ : Λ →L[𝕜] F} [CompleteSpace 𝕜] (hD₁ : D₁.IsFredholm) (hD : Function.Surjective ⇑(D₁.coprod D₂)) : (D₁.coprod D₂).HasRightInverse

A surjective total linearization splits continuously when its fixed-parameter part is Fredholm.

If D₁ : E →L[𝕜] F is Fredholm and D₁.coprod D₂ : E × Λ →L[𝕜] F is surjective, then the latter has a continuous linear right inverse. Parameter directions first solve the finite-dimensional cokernel component of D₁; a Fredholm quasi-inverse then solves the remaining range component.

theorem ContinuousLinearMap.IsFredholm.closedComplemented_ker_coprod {𝕜 : Type u_1} {E : Type u_2} {Λ : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup Λ] [NormedSpace 𝕜 Λ] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {D₁ : E →L[𝕜] F} {D₂ : Λ →L[𝕜] F} [CompleteSpace 𝕜] (hD₁ : D₁.IsFredholm) (hD : Function.Surjective ⇑(D₁.coprod D₂)) : (↑(D₁.coprod D₂)).ker.ClosedComplemented

The kernel of a surjective total linearization is topologically complemented when its fixed-parameter part is Fredholm. This is the complemented-kernel hypothesis required by the Banach-space implicit function theorem for the universal zero set.