Analytic maps on manifolds, read in charts #
On a manifold modelled without boundary, Mathlib's C^ω maps (ContMDiffAt I I' ω f x) are
exactly the maps whose coordinate expressions in charts are analytic in the sense of convergent
power series (AnalyticAt). This file records that dictionary, so that results about analytic
functions on open subsets of a normed space (identity theorem, semianalytic presentations,
complexification) can be applied to analytic functions on analytic manifolds chart by chart.
- The change of coordinates between two charts of the maximal
C^ωatlas is analytic on its (open) domain. - A map is
C^ωatxif and only if it is continuous atxand its coordinate expression in any charts of the maximal atlases atxandf xis analytic at the coordinate ofx; for a function with values in a normed space, continuity is automatic. Only the converse direction needs a complete target. On an open subset of a chart domain, beingC^ωis analyticity of the coordinate expression on the image of that subset. - The identity theorem: two functions that are
C^ωon a preconnected set and agree near one of its points agree on all of it.
The model is assumed boundaryless throughout, so that chart images of open sets are open and
C^ω within the model's range is C^ω on a neighbourhood.
Main results #
ModelWithCorners.analyticOnNhd_extendCoordChange,ModelWithCorners.analyticAt_extendCoordChange,TauCeti.analyticOnNhd_ext_coord_change,OpenPartialHomeomorph.analyticOnNhd_extendTrans_symm_trans, andOpenPartialHomeomorph.analyticOnNhd_extendTrans_symm_trans_map: changes of coordinates in aC^ωatlas, and the coordinate expression of aC^ωmap in two charts, are analytic; the first is the special case of the second for the identity.ContMDiffAt.analyticAt_extend_comp_extend_symm,ContMDiffAt.analyticAt_writtenInExtChartAt,TauCeti.contMDiffAt_omega_iff_of_mem_maximalAtlasandTauCeti.contMDiffAt_omega_iff:C^ωmaps between manifolds in arbitrary and in preferred charts.ContMDiffAt.analyticAt_comp_extend_symm,TauCeti.contMDiffAt_omega_iff_analyticAt_of_mem_maximalAtlasandTauCeti.contMDiffAt_omega_iff_analyticAt:C^ωfunctions with values in a normed space;TauCeti.contMDiffAt_modelSpace_omega_iff_analyticAtis the case of the trivial model.TauCeti.contMDiffOn_omega_iff_analyticOnNhd_of_mem_maximalAtlas: the same on open subsets of a chart domain.TauCeti.eqOn_of_preconnected_of_eventuallyEq_of_contMDiffAtandContMDiff.eq_of_eventuallyEq: the identity theorem.
Changes of coordinates #
Changes of coordinates are analytic. For a boundaryless model, the change of coordinates
between two charts of the maximal C^ω atlas is analytic on its domain.
Changes of coordinates are analytic. For a boundaryless model, the change of coordinates
between two charts of the maximal C^ω atlas is analytic at the coordinate of every point of both
chart domains.
For a boundaryless model, the change of coordinates between the preferred charts at two
points of a C^ω manifold is analytic on its domain.
The coordinate expression of an open partial homeomorphism Φ, which is C^ω on its source,
in two C^ω charts followed by homeomorphisms Ψ, Ψ' with Ψ.symm and Ψ' of class C^ω is
analytic on its source.
For a boundaryless model, the transition map between two maximal C^ω-atlas charts
c₁, c₂, read in E and moved to F by homeomorphisms Ψ₁, Ψ₂ with Ψ₁.symm and Ψ₂ of class
C^ω, is analytic on its open source. This is the case Φ = refl of
OpenPartialHomeomorph.analyticOnNhd_extendTrans_symm_trans_map.
C^ω maps in charts #
A function with values in a normed space that is C^ω at x has an analytic coordinate
expression at the coordinate of x in any chart at x of the maximal C^ω atlas.
A map that is C^ω at x has an analytic coordinate expression at the coordinate of x in
any charts e at x and e' at f x of the maximal C^ω atlases.
A map that is C^ω at x has an analytic coordinate expression in the preferred charts at x
and f x, at the coordinate of x.
C^ω maps in charts. For boundaryless models, a map is C^ω at x if and only if it is
continuous at x and its coordinate expression in charts e at x and e' at f x of the
maximal C^ω atlases is analytic at the coordinate of x.
C^ω maps in charts. For boundaryless models, a map is C^ω at x if and only if it is
continuous at x and its coordinate expression in the preferred charts at x and f x is analytic
at the coordinate of x.
Analytic functions in charts. For a boundaryless model, a function with values in a
complete normed space is C^ω at x if and only if its coordinate expression in a chart e at x
of the maximal C^ω atlas is analytic at the coordinate of x.
Analytic functions in charts. For a boundaryless model, a function with values in a
complete normed space is C^ω at x if and only if its coordinate expression in the preferred
chart at x is analytic at the coordinate of x.
Analytic functions on a normed space. With the trivial model 𝓘(𝕜, E), a function with
values in a complete normed space is C^ω at x if and only if it is analytic at x.
Analytic functions on a chart domain. For a boundaryless model and an open subset U of
the domain of a chart e of the maximal C^ω atlas, a function with values in a normed space is
C^ω on U if and only if its coordinate expression is analytic on the image of U.
The identity theorem #
The identity theorem on analytic manifolds. On a C^ω manifold modelled without boundary
on a locally connected space, two functions with values in a normed space that are C^ω at every
point of a preconnected set U, and agree on a neighbourhood of a point of U, agree on U.
The identity theorem on analytic manifolds. On a preconnected C^ω manifold modelled
without boundary on a locally connected space, two C^ω functions with values in a normed space
that agree on a neighbourhood of a point are equal.