Regular level sets of a Fredholm map #
Let f : E โ F be a map between Banach spaces which is strictly differentiable at a point a of
the level set {x | f x = c}, and whose derivative f' there is a surjective Fredholm
operator. This file shows that the level set is, near a, homeomorphic to an open subset of
ker f', a space whose dimension is exactly the Fredholm index of f'; and it packages that
local model, when the index is a fixed n along the whole level set, as a ChartedSpace
structure on {x | f x = c} modelled on Fin n โ ๐.
This is the local half of the standard "a moduli space is the zero set of a Fredholm section, and
at a regular point it is a manifold of dimension the index" package (McDuff--Salamon,
J-holomorphic Curves and Symplectic Topology, Appendix A.3). The linear half is already available:
ContinuousLinearMap.IsFredholm provides the
finite-dimensional, topologically complemented kernel, and
ContinuousLinearMap.index_of_surjective identifies its dimension with the index. What is
added here is the nonlinear half, which is Mathlib's implicit function theorem for a map with
surjective derivative and complemented kernel,
HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented, restricted to the level set:
that homeomorphism carries {x | f x = c} to the "vertical" slice {c} ร ker f', and the chart
below is the resulting homeomorphism of the level set with an open subset of ker f'.
Three consequences record that the dimension count is not vacuous, and are stated with Mathlib's
accumulation-point vocabulary AccPt. A point where the derivative is injective with closed range
โ in particular a regular point of index 0 โ is isolated in the level set through it, so a
compact piece of such a level set is finite: one ingredient in the well-definedness of a
Floer-type differential, which counts index-0 solutions; making such a count well defined also
needs a separate compactness result placing the counted solutions inside one such piece, which is
not proved here. Where the kernel is nontrivial โ in particular at a regular point of nonzero index
โ the level set on the contrary accumulates at the point, so a level set is locally the single
point a precisely when the index vanishes.
What is proved is exactly a ChartedSpace structure, that is, a covering family of local models;
nothing more is claimed. In particular this is not the assertion that the level set is a
topological manifold in the usual sense, which would additionally need global hypotheses such as
second countability, and none are assumed here. Smooth compatibility of the charts, under a
ContDiff hypothesis on f, is TauCeti.isManifold_levelSet in
TauCeti/Analysis/Fredholm/LevelSet/Manifold.lean; the preferred charts installed below are
already cut down to TauCeti.levelSetImplicitCoordSource so that they can be compared smoothly.
Main declarations #
TauCeti.levelSetChart: the chart{x | f x = c} โ ker f'at a regular pointa, given by projectingx - aontoker f'along the chosen complement.ContinuousLinearMap.kerModelEquiv: the identification ofker f'with the model spaceFin n โ ๐, whenker f'is finite-dimensional of dimensionn.TauCeti.levelSetChartModel: the chart read through that identification.TauCeti.levelSetImplicitCoordSource: the neighbourhood of a point of the level set to which the preferred chart there is cut down.TauCeti.levelSetChartedSpace: a regular level set on which the index is constantlynis a charted space modelled onFin n โ ๐; byContinuousLinearMap.index_of_surjectivethe model dimension is the Fredholm index.TauCeti.not_accPt_levelSet_of_injective_of_isClosed_rangeandTauCeti.not_accPt_levelSet_of_index_eq_zero: a point where the derivative is injective with closed range, in particular a regular point of index0, is isolated in the level set through it.TauCeti.isDiscrete_levelSet_inter_of_injective_of_isClosed_range,TauCeti.finite_levelSet_inter_of_injective_of_isClosed_rangeandTauCeti.finite_levelSet_inter_of_index_eq_zero: hence such a piece of a level set is discrete, and a compact one is finite.TauCeti.accPt_levelSet_of_nontrivial_kerandTauCeti.accPt_levelSet_of_index_ne_zero: where the kernel is nontrivial, in particular in nonzero index, the level set accumulates at the point.
The chart of a level set at a regular point #
The chart of the level set {x | f x = c} at a point a where f is strictly differentiable
with surjective derivative f' of complemented kernel: it sends x to the projection of x - a
onto ker f' along the complement chosen by hker, and is a homeomorphism from a neighbourhood
of a in the level set onto an open subset of ker f'.
This is Mathlib's implicit-function homeomorphism x โฆ (f x, proj (x - a)) restricted to the
level set, on which its first component is constantly c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The source of the chart of a level set is the source of Mathlib's implicit-function homeomorphism, seen inside the level set.
The target of the chart of a level set is the slice {c} ร ker f' of the target of Mathlib's
implicit-function homeomorphism, read in ker f'.
The chart of a level set is computed by the projection onto ker f' chosen by hker, applied
to x - a.
On its target, the inverse of the chart of a level set is the implicit function of f at the
constant value c: the inverse of Mathlib's implicit-function homeomorphism, read on the slice
{c} ร ker f'.
The chart of a level set is normalised at its base point: it sends a to the origin of
ker f'.
The base point of the chart of a level set lies in its source.
The origin of ker f', the value of the chart at its base point, lies in its target.
The inverse of the chart of a level set is normalised at its base point: it sends the origin
of ker f' back to a.
The chart in the model space #
The identification of the kernel of a continuous linear map with the model space Fin n โ ๐,
when that kernel is finite-dimensional of dimension n โ by
ContinuousLinearMap.index_of_surjective, for a surjective Fredholm operator, the Fredholm
index.
Equations
- T.kerModelEquiv hfin hn = ContinuousLinearEquiv.ofFinrankEq โฏ
Instances For
The chart of a regular level set, read in the model space Fin n โ ๐ through
ContinuousLinearMap.kerModelEquiv.
Equations
- TauCeti.levelSetChartModel hf hf' hker hfin hn ha = (TauCeti.levelSetChart hf hf' hker ha).transHomeomorph (f'.kerModelEquiv hfin hn).toHomeomorph
Instances For
The model chart is the chart of the level set read through
ContinuousLinearMap.kerModelEquiv.
The inverse of the model chart is the inverse of the chart of the level set, read through
ContinuousLinearMap.kerModelEquiv.
The model chart has the same source as the chart of the level set it is read from.
The target of the model chart is the target of the chart of the level set it is read from,
pulled back along ContinuousLinearMap.kerModelEquiv.
The model chart is normalised at its base point: it sends a to the origin of Fin n โ ๐.
The base point of the model chart lies in its source.
The origin of Fin n โ ๐, the value of the model chart at its base point, lies in its
target.
A regular level set of constant index is a charted space #
Along a regular level set on which the Fredholm index is constantly n, the kernel of the
derivative at a point of the level set has dimension n, so Fin n โ ๐ is the local model
there.
The neighbourhood of a point z of a regular level set to which the preferred chart at z is
cut down: the set on which the coordinate map of the implicit function theorem keeps an invertible
derivative, HasStrictFDerivAt.implicitCoordSource, read inside the level set.
Equations
- TauCeti.levelSetImplicitCoordSource hf hsurj hker z = Subtype.val โปยน' โฏ.implicitCoordSource โฏ โฏ
Instances For
Membership in TauCeti.levelSetImplicitCoordSource is membership of the ambient point in
HasStrictFDerivAt.implicitCoordSource.
The preferred chart at a point of a regular level set along which the Fredholm index is
constantly n.
It is the implicit-function chart TauCeti.levelSetChartModel, cut down to
TauCeti.levelSetImplicitCoordSource. That restriction costs nothing โ the set is an open
neighbourhood of the base point โ and it buys the smoothness that the inverse chart lacks away from
its own centre, so that two of these charts can be smoothly compatible.
Equations
- TauCeti.levelSetChartAt hf hFred hsurj hindex z = (TauCeti.levelSetChartModel โฏ โฏ โฏ โฏ โฏ โฏ).restrOpen (TauCeti.levelSetImplicitCoordSource hf hsurj โฏ z) โฏ
Instances For
The source of the preferred chart at z is the source of the chart of the level set at z,
cut down to TauCeti.levelSetImplicitCoordSource.
The target of the preferred chart at z is the target of the chart of the level set at z,
pulled back along ContinuousLinearMap.kerModelEquiv, cut down to the part of
TauCeti.levelSetImplicitCoordSource that the chart sees.
The preferred chart at z is the chart of the level set at z, read in the model space
through ContinuousLinearMap.kerModelEquiv.
The inverse of the preferred chart at z is the inverse of the chart of the level set at z,
read through ContinuousLinearMap.kerModelEquiv.
The preferred chart at z is normalised at z: it sends z to the origin of Fin n โ ๐.
The inverse of the preferred chart at z sends the origin of Fin n โ ๐ back to z.
A point of a regular level set lies in the source of its preferred chart.
The origin of Fin n โ ๐, the value of the preferred chart at its base point, lies in its
target.
A regular level set of a Fredholm map is locally modelled on Fin n โ ๐, n its index.
If f is strictly differentiable at every point of the level set {x | f x = c} with surjective
Fredholm derivative of index n there, then the level set is a charted space modelled on
Fin n โ ๐, the charts being the implicit-function charts TauCeti.levelSetChartAt.
This is a ChartedSpace structure only: no global hypothesis such as second countability is
assumed, so this does not by itself say that the level set is a topological manifold.
The definition is irreducible: its behaviour is available through
TauCeti.levelSetChartedSpace_chartAt and TauCeti.levelSetChartedSpace_atlas, which together
with the TauCeti.levelSetChartAt_* lemmas describe the installed charts, so no consumer needs to
unfold the structure literal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The preferred chart of the charted-space structure at z is TauCeti.levelSetChartAt.
The atlas of the charted-space structure is the range of its preferred charts.
Isolated points, discreteness and accumulation #
A point at which f is differentiable with injective derivative of closed range is
isolated in the level set through it: it is not an accumulation point of {x | f x = c}. No
relation between f a and c is assumed; if f a โ c this is the statement that a is not an
accumulation point of a set it does not belong to.
A point at which the derivative is surjective of index zero, with finite-dimensional
kernel, is isolated in the level set through it: the local model ker f' is then the zero space.
Finite-dimensionality of the kernel is what rules out the reading of index f' = 0 in which both
finrank values are the junk value 0; the full Fredholm property is not needed, and for a
surjective operator is anyway equivalent to it by
TauCeti.isFredholm_iff_finite_ker_of_surjective.
A piece {x | f x = c} โฉ K of a level set along which the derivative is injective with closed
range is discrete. Only the points of that piece are constrained: nothing is assumed about f
away from it.
A compact piece of a level set along which the derivative is injective with closed range is finite.
A compact piece {x | f x = c} โฉ K of a level set along which the derivative is surjective
of index zero with finite-dimensional kernel is finite. When f is continuous the level set is
closed, so for a compact K the compactness hypothesis is
hK.inter_left (isClosed_eq hcont continuous_const).
This is one ingredient in the well-definedness of a count of index-zero solutions, such as a Floer differential: it makes the counted set finite once a separate compactness result has placed the solutions to be counted inside such a piece.
At a point of a level set where the derivative is surjective with complemented nontrivial
kernel, the level set is not locally the single point a: it accumulates at a.
At a point of a level set where the derivative is surjective with complemented kernel and of
nonzero index the level set accumulates. With
TauCeti.not_accPt_levelSet_of_index_eq_zero this says that the level set reduces to the point a
near a โ equivalently, that the local model ker f' is trivial โ exactly when the index
vanishes. No finiteness of the kernel is assumed: a nonzero index already forces a nonzero, hence
positive, finrank of the kernel.