Zero manifolds of smooth Fredholm sections #
Over ℝ or ℂ, a smooth section along a map from a Banach manifold has a smooth zero manifold
whenever its intrinsic linearization is surjective Fredholm of constant index at its zeros.
This file derives the fiber-coordinate hypotheses of the section-zero atlas from smoothness into
the total space. The inclusion of the zero manifold into the parameter space is a smooth
immersion, with tangent image equal to the kernel of the intrinsic linearization.
Smoothness is needed only at zeros, not everywhere. Fredholmness, surjectivity and the index
are stated intrinsically, so callers need not choose a trivialization or supply derivatives of
coordinate expressions. The source is a boundaryless manifold modelled on a Banach space.
As usual, IsManifold asserts smooth compatibility of charts, without imposing
second countability.
References #
- D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3, for regular zeros of Fredholm sections.
The construction consumes sectionZeroChartedSpace and isManifold_sectionZero.
Regular zeros of a smooth Fredholm section along a map from a Banach manifold form a smooth
manifold of dimension the intrinsic Fredholm index. Its inclusion into the parameter space is
a smooth immersion with complement F, and tangent image the intrinsic linearization's kernel.
Only smoothness at zeros is required, at a nonzero differentiability order.
The charted-space structure is supplied as a witness, so it can be installed locally with
letI. No chartwise derivative or smoothness hypotheses need to be supplied by the caller.
A globally smooth section with regular Fredholm zeros of index zero has finitely many zeros on a compact source. Its actual zero manifold is discrete, rather than merely having an assumed isolated-zero property.