A manifold derivative read in arbitrary charts #
A map f : M → M' with manifold derivative f' at x' becomes, in the extended charts centred at
any x and y whose sources contain x' and f x', a map between model vector spaces. Its
Fréchet derivative within range I is f' conjugated by the derivatives of the two charts.
Mathlib's mdifferentiableAt_iff_of_mem_source records differentiability in such charts, but not
the value of the derivative. Change-of-variables arguments on a manifold need that value, because
they integrate the absolute Jacobian determinant of f read in fixed charts.
For a map into a normed space on a boundaryless manifold, the coordinate expression in the
preferred extended chart at x is an honest function on the model space, C^n or differentiable
whenever f is, and its Fréchet derivative at the chart image of x is the vector-valued
manifold derivative mvfderiv I f x. This is how critical points defined through the preferred
chart, as in Morse theory, are identified with the zeros of mvfderiv.
Main results #
TauCeti.Manifold.mdifferentiableAt_iff_of_chartAt_eq: preferred-chart invariance of manifold differentiability.TauCeti.Manifold.mfderiv_eq_of_chartAt_eq: retaining the preferred charts preserves manifold derivatives when the source atlas changes.HasMFDerivAt.hasFDerivWithinAt_of_mem_source: the derivative offread in the extended charts atxandy.TauCeti.mfderiv_eq_fderiv_comp_mfderiv_extChartAtandTauCeti.fderiv_comp_extChartAt_symm_injective: for a map into a normed space, the manifold derivative at any point of a chart's source, in terms of the Fréchet derivative of the coordinate expression, and the resulting transfer of injectivity.TauCeti.mfderiv_eq_zero_iff_fderiv_comp_extChartAt_symm_eq_zero: the zeros of the manifold derivative are the zeros of the Fréchet derivative of the coordinate expression in any chart.TauCeti.eventually_mfderiv_eq_zero_iff_extChartAt_symm: local uniqueness of critical points of aC¹family in the extended chart atxtransfers to the manifold.ContMDiffAt.contDiffAt_comp_extChartAt_symmandMDifferentiableAt.differentiableAt_comp_extChartAt_symm: on a boundaryless manifold, the coordinate expression of aC^n(resp. differentiable) map into a normed space isC^n(resp. differentiable) at the chart image of the point.ContMDiffAt.contDiffAt_writtenInExtChartAtandMDifferentiableAt.differentiableAt_writtenInExtChartAt: the same for a map between manifolds, read in the extended charts at the point and at its image.MDifferentiableAt.tangentSpaceCastModel_mfderiv_apply: on a boundaryless source, the coordinate derivative is the manifold derivative transported by the canonical tangent-to-model casts.TauCeti.mdifferentiableAt_iff_differentiableAt_comp_extChartAt_symm: conversely, a map into a normed space is differentiable whenever its preferred coordinate expression is.TauCeti.mvfderiv_eq_fderiv_comp_extChartAt_symm: on a boundaryless manifold, the vector-valued manifold derivative is the Fréchet derivative of the coordinate expression.MDifferentiableAt.mfderiv_eq_fderiv_extChartAt_conj: on a boundaryless manifold, the manifold derivative of a map between manifolds is the Fréchet derivative of its expression in the extended charts at the point and at its image.ContMDiffAt.hasStrictFDerivAt_extChartAt_conj: overℝorℂ, a map out of a boundaryless manifold that isC¹at a point, read in the extended charts at that point and at its image, is strictly differentiable at the chart image of the point.TauCeti.contMDiffAt_iff_contDiffAt_comp_extChartAt_symmandTauCeti.contMDiffAt_iff_contDiffAt_comp_extend_symm: on a boundaryless manifold, a map into a normed space isC^nat a point exactly when its coordinate expression in the preferred chart, or in any chart of theC^nmaximal atlas, isC^nthere.ContMDiffAt.contDiffAt_comp_chartAt_symmandTauCeti.fderiv_comp_chartAt_symm: the corresponding regularity and derivative formulas for a manifold modelled on its model space, withTauCeti.ker_mvfderiv_eq_ker_fderiv_comp_chartAt_symmreading the kernel of the differential as a subspace of the model space.TauCeti.mvfderiv_eq_zero_iff_fderiv_comp_extend_symm_eq_zero: on a boundaryless manifold, the differential of a map into a normed space vanishes at a point exactly when the derivative of its coordinate expression in any chart of theC¹maximal atlas vanishes there.MDifferentiableAt.fderivWithin_comp_extChartAt_symm: read a model-valued manifold derivative after an inverse chart, including derivatives within the model range.MDifferentiableAt.fderivWithin_extChartAt_comp_extChartAt_symm: the same for a map between manifolds read in arbitrary preferred charts of the source and the target.ContMDiffAt.contDiffAt_extChartAt_comp_extChartAt_symm: aC^nmap between manifolds, read in arbitrary preferred charts, isC^nat interior points of the source chart target.HasMFDerivAt.hasFDerivAt_extChartAt_comp: read the coordinate derivative of a map from a normed source by composing its manifold derivative with the tangent chart.MDifferentiableAt.fderiv_extChartAt_comp_apply: the same, with the manifold derivative of the chart in place of the tangent chart.MDifferentiableAt.differentiableAt_chartAt_comp: a differentiable map from a normed space into a manifold modelled on a normed space is differentiable in the preferred chart at its image.MDifferentiableAt.fderiv_chartAt_comp: the derivative in that chart is the manifold derivative with the canonical source tangent identification.TauCeti.mfderivWithin_extChartAt_symm_of_subset: within a subset of the chart target with unique derivatives, the derivative of the inverse chart is its derivative within the model range.TauCeti.eventually_differentiableAt_chart_comp_of_eventually_mdifferentiableAtandTauCeti.eventually_mdifferentiableAt_chart_symm_comp_of_eventually_differentiableAt: transport differentiability near a point between a product of manifolds and model spaces using maximal-atlas charts.TauCeti.writtenInExtChartAt_chartAt_comp_eventuallyEq,TauCeti.hasMFDerivAt_chartAt_compandTauCeti.contMDiffAt_chartAt_comp: for a space charted over a charted spaceX, with the composite charts, the preferredX-valued chart atxreads as the identity nearx, so it is smooth atxwith the identity as its derivative there.MDifferentiableAt.differentiableWithinAt_fderivWithin_extChart_comp_eq_zero: where the manifold differential vanishes at a point of differentiability, the coordinate expression in extended charts is differentiable within the model range with zero derivative.TauCeti.fderiv_comp_extChartAt_symm_apply_zero_one: the preferred chart ofM × 𝕜is the identity on𝕜, so the derivative of a coordinate expression in the direction(0, 1)is the derivative along𝕜, read without any chart.ContMDiff.continuous_deriv_prodMk: the derivative along𝕜of aC¹function onM × 𝕜is continuous.
Preferred charts determine manifold differentiability independently of the rest of the atlas.
Changing the source atlas while retaining its preferred charts preserves manifold derivatives for maps to any charted target.
Read in the extended charts at x and y, a map with manifold derivative f' at x' has
Fréchet derivative within range I equal to f' pre- and post-composed with the derivatives of
the inverse chart at x and of the chart at y. The charts need only contain x' and f x' in
their sources; they need not be centred there.
Maps into a normed space, read in a chart of the source #
At a point y of the source of the extended chart at x, the manifold derivative of a map
into a normed space is the Fréchet derivative of its coordinate expression
f ∘ (extChartAt I x).symm at the chart image of y, composed with the manifold derivative of
the chart. The chart need not be centred at y.
Read in a chart, a map into a normed space whose manifold derivative at y is injective has
injective Fréchet derivative at the chart image of y.
Read in a chart whose source contains y, a map into a normed space with differentiable
coordinate expression has zero manifold derivative at y exactly when that coordinate expression
has zero Fréchet derivative at the chart image of y.
If the critical point of the coordinate expression fun v ↦ f (q.1, (extChartAt I x).symm v)
of a C¹ family is, near (p, extChartAt I x x), uniquely η q.1, then the zero of the manifold
derivative of fun y ↦ f (q.1, y) near (p, x) is uniquely (extChartAt I x).symm (η q.1).
Maps into a normed space on a boundaryless manifold #
On a boundaryless manifold, a map into a normed space is C^n at x exactly when its
coordinate expression in the preferred extended chart at x is C^n at the chart image of x.
On a boundaryless manifold, a map into a normed space is C^n at x exactly when its
coordinate expression in a chart of the C^n maximal atlas containing x is C^n at the chart
image of x.
On a boundaryless manifold, the differential of a map into a normed space vanishes exactly
when the derivative of its coordinate expression in a chart of the C¹ maximal atlas containing
x vanishes at the chart image of x. Both sides are 0 when the map is not differentiable
at x.
On a boundaryless manifold, a map into a normed space which is C^n at x has a C^n
coordinate expression in the preferred extended chart at x.
On a boundaryless manifold, a map into a normed space which is differentiable at x has a
differentiable coordinate expression in the preferred extended chart at x.
On a boundaryless source, a map between manifolds which is C^n at x has a C^n coordinate
expression in the extended charts at x and at f x.
On a boundaryless source, a map between manifolds which is differentiable at x has a
differentiable coordinate expression in the extended charts at x and at f x.
On a boundaryless manifold, the manifold derivative of g : M → M' at x is the Fréchet
derivative of g read in the extended charts at x and at y = g x, with the tangent spaces at
x and g x identified with the model spaces. Naming the image point y allows a self-map
fixing x to be read in the single chart at x.
On a boundaryless source, the manifold derivative, transported to the model spaces by the canonical tangent casts, is the Fréchet derivative of the preferred coordinate expression.
On a boundaryless manifold, a map into a normed space is differentiable at x exactly when
its coordinate expression in the preferred extended chart is differentiable at the chart image
of x.
On a boundaryless manifold, the vector-valued manifold derivative of a map into a normed space
is the Fréchet derivative of its coordinate expression in the preferred extended chart. Both sides
are 0 when the map is not differentiable at the point.
On a manifold modelled on its model space, the preferred-chart coordinate expression of a
C^n map into a normed space is C^n at the chart image of the point.
On a manifold modelled on its model space, the derivative of the preferred-chart coordinate
expression is the vector-valued manifold derivative. Both sides are 0 when the map is not
differentiable at the point.
On a manifold modelled on its model space, the kernel of the vector-valued manifold derivative is the kernel of the derivative of the preferred-chart coordinate expression, a subspace of the model space.
On a manifold modelled on its model space, a map into a normed space whose coordinate
expression in a chart of the C¹ maximal atlas is differentiable at a coordinate is manifold
differentiable at the corresponding point.
Preferred charts of a composite charted space #
For the composite charts ChartedSpace.comp H X N of a space charted over a charted space X,
the preferred X-valued chart at x, read in the composite chart at x and the chart of X at
its image, is the identity near the image of x.
For the composite charts ChartedSpace.comp H X N, the preferred X-valued chart at x has
the identity as its manifold derivative at x.
For the composite charts ChartedSpace.comp H X N, the preferred X-valued chart at x is
C^n at x, for every n.
On a subset of a chart overlap, the derivative of the extended coordinate change is its Fréchet derivative within the full model range, including at boundary and corner points.
On a subset of the chart target with unique derivatives, the derivative of the inverse chart within the subset is its derivative within the model range.
The derivative of a model-valued map in an arbitrary preferred chart is its actual manifold derivative composed with the inverse tangent chart.
In a preferred chart, a manifold derivative from a normed source gives the ordinary coordinate derivative by composing with the tangent chart.
Read in a preferred chart, the derivative of a map from a normed space is its manifold derivative followed by the manifold derivative of the chart.
The coordinate expression of a map between manifolds in arbitrary preferred charts at β
and α has, as its derivative within the model range, the manifold derivative composed with the
tangent coordinate changes of the two charts.
A map between manifolds which is C^n at the point with coordinate y in the preferred chart
at β, and sends it into the source of the preferred chart at α, is C^n at y when read in
these charts, provided y lies in the interior of the chart target.
A map out of a manifold without boundary that is C¹ at y, read in the extended charts at
y and at f y, has a strict derivative at the image of y.
A map from a normed space into a manifold modelled on a normed space, differentiable at x,
read in the preferred chart at its image, is differentiable at x.
For a normed source and a manifold modelled on a normed space, the derivative in the preferred chart at the image is the manifold derivative, using the canonical tangent-space identifications.
The representative of a map differentiable near a point in maximal-atlas product charts is Fréchet differentiable near the corresponding model-space point.
Pulling a map differentiable near a model-space point back through maximal-atlas product charts gives a map differentiable near the original point, provided its value lies in the target of the output chart.
The chain rule transfers a vanishing manifold differential to the coordinate expression
extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm, computed within the model range: at a point u
of the chart target whose image (extChartAt I x).symm u is a point of differentiability of f
with zero differential, mapped into the source of the target chart, the expression is
differentiable within the range with zero derivative.
The preferred extended chart at x has the identity as its manifold derivative at x. This
is mfderiv_extChartAt_self without any smoothness hypothesis on the atlas, in the form of a
HasMFDerivAt statement.
The manifold derivative of the preferred extended chart at its centre is the identity, with no smoothness hypothesis on the atlas.
The derivative along the scalar factor of M × 𝕜 #
The derivative along 𝕜 in coordinates. At the chart image of a point (x, s) of the
chart source, the derivative of the coordinate expression of f : X × 𝕜 → F in the direction
(0, 1) is the derivative of the slice of f through x.
The derivative along 𝕜 of a C¹ function on X × 𝕜 is continuous. On a boundaryless
manifold X, the map (x, t) ↦ ∂ₜ f (x, t) is continuous; near each point it is the derivative of
the coordinate expression of f in the direction of the last factor, which is unchanged by the
charts.