Regular levels of maps into finite-dimensional spaces #
Let ๐ be an RCLike field, such as โ or โ, and let f : M โ F be a map from a
boundaryless manifold modelled on a finite-dimensional ๐-space E to a finite-dimensional
normed ๐-space F.
Suppose f is Cยน at every point of the level fโปยน(c) and c is a regular value of f. Then
the actual subtype {x // f x = c} carries the atlas TauCeti.regularLevelChartedSpace, modelled
on Fin n โ ๐ for n = dim E - dim F, and is a C^m manifold when f is C^m at the points
of the level, m โฅ 1 (TauCeti.isManifold_regularLevel). No Hausdorff or second-countability
hypothesis is used, and the level may be empty. When it is nonempty, regularity forces
dim F โค dim E, so the natural-number subtraction is exact. The model dimension is a parameter
n together with a proof of dim E - dim F = n, so that special cases can fix a convenient
expression for it: for scalar functions, F = ๐, users take n = dim E - 1, with the proof
by rw [finrank_self].
The atlas is the section-zero atlas TauCeti.sectionZeroChartedSpace of the section f - c of
the trivial bundle with fibre F over the self-modelled copy TauCeti.BoundarylessModel I M,
transported to fโปยน(c) along the identity of points. The trivialization coordinate of this
section is f - c itself, and the linearization at x is the derivative
D_x = fderiv ๐ (f โ (extChartAt I x).symm) (extChartAt I x x)
of f in the preferred extended chart. Writing ฯ_x for the chosen projection of E onto
ker D_x and K_x : ker D_x โ (Fin n โ ๐) for the index-model identification, the preferred
chart at x is
w โฆ K_x (ฯ_x (extChartAt I x w - extChartAt I x x))
(TauCeti.regularLevelChartAt_apply). Its inverse is the inverse preferred extended chart of M
applied to the inverse implicit-function chart of f - c on the zero slice
(TauCeti.coe_regularLevelChartAt_symm_apply).
For this atlas the level is an embedded submanifold: the inclusion {x // f x = c} โ M is a
C^m immersion with complement F and a topological embedding, hence a smooth embedding
(TauCeti.isSmoothEmbedding_coe_regularLevel), and its differential at x has range
ker (mfderiv I ๐(๐, F) f x) (TauCeti.range_mfderiv_coe_regularLevel).
In particular, over โ and at order m = โ (or m = ฯ), this constructs the complex-manifold
atlas and holomorphic embedding of a regular holomorphic level in arbitrary codimension
dim โ F. The tangent-kernel equation is complex-linear. The RCLike assumption is used to
obtain strict differentiability from Cยน regularity; the underlying section-zero construction
works over arbitrary complete nontrivially normed fields when strict differentiability is given.
Main declarations #
TauCeti.regularLevelChartAtandTauCeti.regularLevelChartedSpace: the preferred charts and the atlas of a regular level.TauCeti.regularLevelChartAt_apply,TauCeti.regularLevelChartAt_source,TauCeti.regularLevelChartAt_symm_zero,TauCeti.mem_regularLevelChartAt_target_iffandTauCeti.coe_regularLevelChartAt_symm_apply: the chart formulas.TauCeti.isManifold_regularLevel: the level is a manifold of dimensiondim E - dim F.TauCeti.isImmersionOfComplement_coe_regularLevelandTauCeti.isSmoothEmbedding_coe_regularLevel: the inclusion of the level is an immersion with complementFand a smooth embedding.TauCeti.range_mfderiv_coe_regularLevel: the tangent space of the level atxis the kernel of the differential offatx.TauCeti.ker_mfderiv_eq_of_forall_eq_imp: two defining maps of a regular level have the same tangent kernels along it.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Corollary 5.14 (regular level sets) and Proposition 5.38 (their tangent spaces).
The section-zero data of a regular level #
The preferred chart at a point x of a regular level fโปยน(c), modelled on Fin n โ ๐ for
n = dim E - dim F: the section-zero chart of f - c at x. It reads a point w as the kernel
component of extChartAt I x w - extChartAt I x x for the derivative of f in the preferred
extended chart at x (TauCeti.regularLevelChartAt_apply).
Instances For
Every point of the level lies in the source of its preferred chart.
The atlas of a regular level fโปยน(c): the section-zero atlas of f - c, with preferred
charts TauCeti.regularLevelChartAt. It is modelled on Fin n โ ๐ for n = dim E - dim F.
Instances For
The installed preferred charts are TauCeti.regularLevelChartAt.
The installed atlas consists exactly of the preferred charts.
The preferred chart at x reads the displacement extChartAt I x w - extChartAt I x x through
the chosen projection onto the kernel of the preferred-chart derivative D of f at x,
followed by the identification of that kernel with Fin n โ ๐.
A preferred chart is centred at its point.
The origin belongs to the target of every preferred chart.
The inverse preferred chart at x sends the origin to x.
The source of the preferred chart at x: points of the level in the preferred chart of M
at x whose extended coordinates lie in the source of the implicit-function chart of f - c and
in the neighbourhood where its derivative stays invertible.
The target of the preferred chart at x: model points k whose kernel vector K.symm k
gives a point (0, K.symm k) of the implicit-function chart target of f - c, whose inverse lies
in the regular neighbourhood and in the target of the preferred extended chart at x.
On its target, the inverse preferred chart at x is the inverse preferred extended chart of
M at x, applied to the inverse implicit-function chart of f - c on the zero slice.
The level as a submanifold #
A regular level fโปยน(c) of a map which is C^m at the points of the level, with m โฅ 1, is
a C^m manifold of dimension dim E - dim F for its preferred atlas.
The inclusion of a regular level is an immersion with complement F. For the preferred
atlas TauCeti.regularLevelChartedSpace, the inclusion of a regular level fโปยน(c) of a map which
is C^m at the points of the level, m โฅ 1, is a C^m immersion whose normal forms have the
space F of values of f as complement.
A regular level is an embedded submanifold. For the preferred atlas
TauCeti.regularLevelChartedSpace, the inclusion of a regular level fโปยน(c) of a map which is
C^m at the points of the level, m โฅ 1, is a C^m smooth embedding.
The tangent space of a regular level is the kernel of df. At a point x of a regular
level fโปยน(c), the differential of the inclusion, for the preferred atlas
TauCeti.regularLevelChartedSpace, has range the kernel of the differential of f at x.
Two defining maps of a regular level have the same tangent kernels. If the regular level
fโปยน(c) of a map which is Cยน near the level is contained in the level gโปยน(c') of a second map
into the same space, then ker dg_x = ker df_x at each of its points x which is a regular point
of g.