Calculus in the charts of a manifold modelled on its own model space #
Let M be a manifold modelled on a normed space E over π with the trivial model π(π, E), so
that a chart e of the maximal atlas is an honest map M β E. If f = h β e on the source of e
for a map f : M β F into a normed space F, then the differential of f is the FrΓ©chet
derivative of h composed with the derivative of the chart, which is invertible, so the
differential of f vanishes at a point in the source of e if and only if the FrΓ©chet derivative
of h vanishes at its image under e. This file records these facts and their consequences in the
preferred chart: the coordinate expression of a C^n map is C^n, the differential of a
differentiable map vanishes at a point if and only if the FrΓ©chet derivative of its coordinate
expression vanishes there, and the points where the differential of a C^1 map is nonzero form an
open set.
Main results #
TauCeti.mfderiv_eq_fderiv_comp_of_eqOn:df_y = dh_{e y} β de_ywheref = h β e.TauCeti.isInvertible_mfderiv_chart: the derivative of a chart of theC^1maximal atlas is invertible.TauCeti.contDiffAt_symm_trans_of_mem_maximalAtlas: a transition map between two charts of theC^nmaximal atlas isC^non its source, andTauCeti.contDiffAt_symm_trans_symm_of_mem_maximalAtlas: its inverse isC^non its target.TauCeti.exists_hasFDerivAt_symm_trans: such a transition map, forn β 0, has an invertible derivative at each point of its source, which is strict overβorβ(TauCeti.exists_hasStrictFDerivAt_symm_trans).TauCeti.fderiv_symm_trans_comp_eq: the chain rule for transitions between charts of the maximal atlas, read through the preferred chart.TauCeti.trans_mem_maximalAtlas_of_contDiffAt: a chart of theC^nmaximal atlas followed by aC^nchart of the model space withC^ninverse is again in the maximal atlas.TauCeti.mfderiv_eq_zero_iff_of_eqOn: on the source ofe, the differential offvanishes atyif and only if the FrΓ©chet derivative ofhvanishes ate y.TauCeti.mfderiv_eq_zero_iff_fderiv_comp_extChartAt_symm: the differential offvanishes atxif and only if the FrΓ©chet derivative of its coordinate expression in the preferred chart vanishes atextChartAt π(π, E) x x.TauCeti.isOpen_setOf_mfderiv_ne_zero: the points where the differential of aC^1map is nonzero form an open set.
If f = h β e on the source of a chart e of the C^1 maximal atlas, then
df_y = dh_{e y} β de_y.
isInvertible_mfderiv_extend for a chart of the C^1 maximal atlas of a manifold modelled on
its own model space, where the extended chart is the chart itself.
Where f = h β e on the source of a chart e of the C^1 maximal atlas, the differential of
f vanishes at y in the source if and only if the FrΓ©chet derivative of h vanishes at e y.
A transition map q.symm.trans q' between two charts of the maximal atlas is C^n at every
point of its source.
Chain rule for chart transitions. Read through the preferred chart at y, the derivative
at q y of the transition e β qβ»ΒΉ between two charts of the maximal atlas, composed with the
derivative A of the transition to q, is the derivative B of the transition to e.
The inverse of a transition map q.symm.trans q' between two charts of the maximal atlas is
C^n at every point of its target.
A chart q of the maximal atlas followed by a chart e of the model space which is C^n on
its source, with C^n inverse on its target, is again a chart of the maximal atlas.
The transition map q.symm.trans q' between two charts of the C^n maximal atlas, n β 0,
has an invertible derivative at each point of its source.
Over β or β, the invertible derivative of exists_hasFDerivAt_symm_trans is strict.
The coordinate expression of f in the preferred chart at p.
The coordinate expression of a C^n function is C^n on the chart target.
The differential of f vanishes at x if and only if the FrΓ©chet derivative of the
coordinate expression of f in the preferred extended chart at x vanishes at
extChartAt π(π, E) x x.
The points where the differential of a C^1 function is nonzero form an open set.