Regular points and regular values of maps between manifolds #
A point x is a regular point of a map f : M → N between manifolds when the manifold
derivative mfderiv I J f x is surjective, and y : N is a regular value of f when every
point of the fibre f ⁻¹' {y} is a regular point. A value outside the range of f is regular.
These are the points and values at which a mapping degree is counted. Sard's theorem
(TauCeti.dense_isRegularValue) says that the regular values of a differentiable map from a
Lindelöf real manifold to a real manifold, both modelled on finite-dimensional spaces of the same
dimension and of class at least C¹, are dense.
Read in the extended charts at arbitrary points x₀ and y₀ whose sources contain x and
f x, the point x is regular exactly when the Fréchet derivative of the coordinate expression
of f within range I is surjective. This is how flat statements about critical points transfer
to manifolds, including manifolds with boundary or corners.
Main definitions #
TauCeti.IsRegularPoint I J f x: the manifold derivative offatxis surjective.TauCeti.IsRegularValue I J f y: every point of the fibre offoveryis regular.
Main results #
TauCeti.isRegularValue_iff_notMem_image: the regular values are the complement of the image of the set of non-regular points.TauCeti.IsRegularValue.restrict: restricting the source to an open subset preserves regular values.TauCeti.exists_isRegularValue_forall_mem_Ioc: a continuous real function on a compact manifold takes all its values strictly above one regular value and at most another.TauCeti.isRegularPoint_iff_surjective_fderivWithin: regularity read in arbitrary charts.TauCeti.isRegularPoint_iff_surjective_fderiv_extChartAt: the same on a boundaryless source, with the Fréchet derivative of the coordinate expression.TauCeti.isRegularPoint_iff_surjective_fderiv: for maps between normed spaces, regularity is surjectivity of the Fréchet derivative.TauCeti.isRegularPoint_iff_injective_mfderiv: between models of the same finite dimension, regularity is injectivity of the manifold derivative.TauCeti.isRegularPoint_iff_isInvertible_mfderiv: between models of the same finite dimension over a complete field, regularity is invertibility of the manifold derivative.TauCeti.isRegularPoint_comp_iff: a composite of differentiable maps is regular exactly when the derivative of the outer map sends the tangent image of the inner map onto the target.TauCeti.IsRegularPoint.mdifferentiableAt: a map into a normed space is differentiable at its regular points.TauCeti.range_mfderiv_le_ker_mfderiv_of_eventually_eq: a map into a level setf ⁻¹' {y}near a point has tangent images there in the kernel of the derivative off.TauCeti.IsRegularPoint.finrank_ker_mfderiv_add_finrankandTauCeti.IsRegularPoint.range_mfderiv_eq_ker_mfderiv: at a regular point the kernel of the derivative has codimension the dimension of the target, and it is the tangent image of every immersion into the level from a manifold of that dimension.TauCeti.IsRegularPoint.surjective_fderiv_comp_extChartAt_symm,TauCeti.IsRegularPoint.finrank_ker_fderiv_comp_extChartAt_symm_add_finrankandTauCeti.IsRegularPoint.finrank_ker_fderiv_comp_extChartAt_symm: on a boundaryless manifold, at a regular point of a map into a normed space the derivative in the preferred extended chart is surjective, with kernel of codimension the dimension of the target, so of codimension one for scalar functions.
References #
- J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Graduate Texts in Mathematics 218, Springer, 2013, Chapter 4 (regular points and values) and Theorem 6.10 (Sard).
A point x is a regular point of f when the manifold derivative of f at x is
surjective. Where f is not differentiable its manifold derivative is 0, so such a point is
regular only when the model of the target is the zero space.
Instances For
A value y is a regular value of f when every point of the fibre of f over y is a
regular point. In particular every value outside the range of f is regular.
Instances For
A point of the fibre over a regular value is a regular point.
A value is regular exactly when it is not the image of a non-regular point.
The set of regular values is the complement of the image of the non-regular points.
A value outside the range of f is a regular value.
Read in the extended charts at x₀ and y₀, whose sources contain x and f x, a point
x at which f is differentiable is regular exactly when the Fréchet derivative within
range I of the coordinate expression of f is surjective at the chart image of x. The charts
need not be centred at x and f x.
For a map into a normed space, regularity is surjectivity of the vector-valued manifold derivative. The canonical target tangent-space identification preserves surjectivity.
The vector-valued manifold derivative has the same kernel as the manifold derivative: the canonical target tangent-space identification does not change the kernel.
For a scalar function, regularity is equivalent to a nonzero differential, read in the
scalar field using mvfderiv. No differentiability hypothesis is needed.
For a map between normed spaces, a regular point is a point at which the Fréchet derivative is surjective.
Between manifolds modelled on finite-dimensional spaces of the same dimension, a point is regular exactly when the manifold derivative there is injective.
Between manifolds modelled on finite-dimensional spaces of the same dimension over a complete field, a point is regular exactly when the manifold derivative there is invertible.
A regular point of a map into a normed space is a point of differentiability. Without
differentiability the derivative is 0, so the target is the zero space and the map is constant.
A composite is regular at a point if both maps are regular at the corresponding points. Where
a map is not differentiable its manifold derivative is 0, so regularity then forces the target
tangent space to be trivial and the composite is regular for that reason.
A composite f ∘ g of differentiable maps is regular at p exactly when the derivative of
f at g p maps the tangent image of g at p onto the tangent space of the target. For the
inclusion g of a submanifold this reads regularity of the restriction of f on the tangent
space of the submanifold.
Every point of an open subset is a regular point of its inclusion.
Restricting the source to an open subset preserves regular values.
The tangent images at p of a map into a level set f ⁻¹' {y} near p lie in the kernel of
the derivative of f. No differentiability is needed: where g or f is not differentiable, the
tangent image is 0 or the kernel is everything.
Dimension of the tangent space of a regular level. At a regular point the kernel of the
derivative has codimension dim N.
The tangent space of a regular level. Let g : P → M map into the level f ⁻¹' {y} near
p, with injective derivative at p, from a manifold of the dimension of the level. If g p is a
regular point of f, the tangent image of g at p is the kernel of the derivative of f.
On a boundaryless source, read in the extended charts at x₀ and y₀, whose sources contain
x and f x, a point x at which f is differentiable is regular exactly when the Fréchet
derivative of the coordinate expression of f is surjective at the chart image of x.
At a regular point of a map into a normed space on a boundaryless manifold, the coordinate expression in the preferred extended chart has surjective derivative.
At a regular point of a map into a normed space on a boundaryless manifold, the kernel of the preferred-chart derivative has codimension the dimension of the target.
At a regular point of a scalar function on a boundaryless manifold, the kernel of the preferred-chart derivative has codimension one.
On a compact manifold, a continuous real function f has values a < f ≤ b everywhere that
are regular values, lying outside its range, so that the band f⁻¹[a, b] is all of M.