Parameter maps on universal Fredholm level sets #
Let f : E × Λ → F be a parametrized equation and suppose that its total linearization at a
solution (x, l) is D₁.coprod D₂. When this linearization is surjective with complemented
kernel, TauCeti.levelSetChart parametrizes the universal level set near (x, l) by
ker (D₁.coprod D₂). Composing its inverse with the projection to Λ gives the local parameter
map TauCeti.levelSetParameterMap.
This file calculates that map's derivative at the chart origin. It is exactly
D₁.parameterProj D₂, the linear parameter projection developed in
TauCeti.Analysis.Fredholm.Parametric. Every statement about that linear map therefore transfers
to the derivative at the origin: it is surjective exactly when D₁ is, by
TauCeti.surjective_fderiv_levelSetParameterMap_iff; it has the same index as D₁, by
TauCeti.index_fderiv_levelSetParameterMap; and over a complete RCLike field it is Fredholm as
soon as D₁ is, by TauCeti.isFredholm_fderiv_levelSetParameterMap.
The same calculation is then carried out at the other points of the chart, where the level set may
have turned and the derivative of the inverse chart is described in general by the kernel section
of TauCeti.Analysis.Fredholm.LevelSet.Tangent rather than by an inclusion. That upgrades the
regularity criterion from the chart origin to a whole neighbourhood of it, and the file closes
with local Sard--Smale in the resulting geometric form: the parameters near l which carry a
nearby solution where the fixed-parameter linearization fails to be surjective form a closed
nowhere dense set of values.
These results are the local nonlinear calculation in the parametric transversality package of McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3. Passing from this one chart to a residual set of parameters for a whole universal moduli space requires smooth compatibility and a countable cover, and is not asserted here.
Main results #
TauCeti.hasStrictFDerivAt_levelSetParameterMap: the derivative at the chart origin is the linear parameter projection.TauCeti.levelSetParameterMap_levelSetChart: on the chart source, the local parameter map is the parameter projection of the universal level set.TauCeti.exists_apply_levelSetParameterMap_eq: every value of the local parameter map is a parameter at which the equation has a solution.TauCeti.surjective_fderiv_levelSetParameterMap_iff: the chart origin is a regular point of the local parameter map exactly when the fixed-parameter linearization is surjective.TauCeti.index_fderiv_levelSetParameterMap: that derivative has the index of the fixed-parameter linearization.TauCeti.isFredholm_fderiv_levelSetParameterMap: over a complete normed field, that derivative is Fredholm as soon as the fixed-parameter linearization is.TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints_levelSetParameterMap: local Sard--Smale for the parameter map of a universal level set.TauCeti.hasFDerivAt_levelSetParameterMap_of_mem: the derivative of the local parameter map at a nearby chart point.TauCeti.surjective_fderiv_levelSetParameterMap_iff_of_mem: a nearby chart point is a regular point of the local parameter map exactly when the linearization of the equation at the solution it names is surjective.TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_not_surjective_levelSetParameterMap: local parametric transversality.
References #
- D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix A.3.
- S. Smale, An infinite dimensional version of Sard's theorem, Amer. J. Math. 87 (1965), 861--866.
The local projection from a universal level set to its parameter space, written in the
regular-level-set chart at (x, l).
The function is meaningful on the target of the level-set chart, a neighbourhood of the origin.
As with TauCeti.levelSetChart, its value outside that target is an irrelevant total extension.
Equations
- TauCeti.levelSetParameterMap hf hD hker hxl k = (↑(↑(TauCeti.levelSetChart hf ⋯ hker hxl).symm k)).2
Instances For
The local parameter map reads the parameter component of the inverse level-set chart.
At the chart origin, the local parameter map returns the base parameter.
On the source of the level-set chart, the local parameter map really is the parameter
projection of the universal level set: it sends the chart image of a solution z back to the
parameter component of z.
Every value of the local parameter map is a parameter for which the equation has a solution: the chart parametrizes the universal level set, so the point it produces solves the equation at the parameter that the map returns.
The local parameter map is as smooth at the chart origin as the parametrized equation.
The derivative at the chart origin of the local parameter map is the restriction of the ambient parameter projection to the kernel of the total linearization.
The Fréchet derivative of the local parameter map at the chart origin is the linear parameter projection.
Regularity at the chart origin. The derivative of the local parameter map at the chart
origin is surjective exactly when the fixed-parameter linearization is. This is the
transversality criterion the parametric package is aimed at, transported to the nonlinear map by
TauCeti.fderiv_levelSetParameterMap.
The derivative of the local parameter map at the chart origin has the same index as the
fixed-parameter linearization. Neither map is assumed Fredholm: both indices are differences of
Module.finranks, junk values included.
The regularity criterion away from the chart origin #
The derivative of the local parameter map at a chart point of the coordinate neighbourhood:
the parameter component of the kernel section of the derivative of f there.
TauCeti.hasStrictFDerivAt_levelSetParameterMap is the case k = 0, where the kernel section is
the inclusion of ker (D₁.coprod D₂) and the composite is D₁.parameterProj D₂.
Regularity away from the chart origin. At a chart point of the coordinate neighbourhood,
the derivative of the local parameter map is surjective exactly when the fixed-parameter part of
the derivative of f there is.
This is TauCeti.surjective_fderiv_levelSetParameterMap_iff with the chart origin replaced by an
arbitrary nearby point: criticality of the local parameter map at k is failure of regularity of
the equation at the solution k names. No surjectivity hypothesis on the derivative at that
solution is needed, because HasStrictFDerivAt.surjective_of_mem_implicitCoordSource supplies it.
Every derivative is of the displayed coproduct shape, by
ContinuousLinearMap.coprod_comp_inl_inr.
If the fixed-parameter linearization is Fredholm, then so is the derivative at the origin of the local parameter map.
Local parametric Sard--Smale. In a regular chart of a universal level set whose fixed-parameter linearization is Fredholm, the critical values of the local parameter map coming from a sufficiently small neighbourhood of the chart origin form a closed nowhere dense set.
The neighbourhood is contained in the target of the level-set chart, on which the local parameter
map really is the parameter projection of the universal level set rather than the irrelevant total
extension of TauCeti.levelSetParameterMap. It can also be confined to any prescribed
neighbourhood U of the chart origin, as
TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints allows; take U = univ for
the plain statement.
Here criticality is defined intrinsically for the local parameter map;
TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_not_surjective_levelSetParameterMap
rewrites it as failure of regularity of the original equation.
The differentiability threshold is the one currently supplied by
TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints, rewritten using the fact
that the kernel of D₁.parameterProj D₂ has the same dimension as ker D₁.
Local parametric transversality. Near a regular solution of a parametrized equation whose fixed-parameter linearization is Fredholm, the parameters carrying a nearby solution at which the fixed-parameter linearization fails to be surjective form a closed nowhere dense set of values.
This is
TauCeti.exists_mem_nhds_isClosed_isNowhereDense_image_criticalPoints_levelSetParameterMap with
the intrinsic critical set of the local parameter map replaced by the geometric condition it
encodes: by TauCeti.surjective_fderiv_levelSetParameterMap_iff_of_mem the two agree at every
chart point close enough to the origin, so the statement is about non-regular parameters of the
original equation rather than about a chart. Every value of the parameter map really is a
parameter at which the equation has a solution, by
TauCeti.exists_apply_levelSetParameterMap_eq.
Only a neighbourhood of one solution is described: passing to a residual set of parameters for a whole universal moduli space needs a countable cover, which is not asserted here. The differentiability threshold is the one supplied by the local Sard--Smale theorem.