The inverse function theorem for manifolds #
Mathlib knows that a C^n local diffeomorphism has invertible differentials
(IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv) and lists the converse as a TODO in
Mathlib/Geometry/Manifold/LocalDiffeomorph.lean. This file proves that converse at interior
points of Banach manifolds: a map which is C^n on an open set, with 1 โค n, and whose mfderiv
at a point of that set is a continuous linear equivalence, is a C^n local diffeomorphism there.
The interior-point form applies to maps between manifolds with boundary whenever the source point lies away from the boundary; invertibility of the differential then forces its image to be an interior point as well. On a boundaryless source manifold the source condition is automatic, even when either ambient model has boundary, yielding the usual global criterion from invertibility of every differential.
The file also records that maximal-atlas charts and their inverses are local diffeomorphisms, and that being a local diffeomorphism at a point is an open condition: the partial diffeomorphism witnessing it at one point witnesses it at every nearby point, and that a local diffeomorphism can be cancelled on either side of a composite local diffeomorphism. Conversely, an open partial homeomorphism to the model space which is a local diffeomorphism on its source is a chart of the maximal atlas.
The extended-chart constructor lets maximal-atlas coordinates, including Frobenius flat charts, serve as partial diffeomorphisms in constructions of local submanifolds.
Main results #
IsLocalDiffeomorph.coe_diffeomorphOfBijective: the associated global diffeomorphism has the original forward map.OpenPartialHomeomorph.toPartialDiffeomorphOfMemMaximalAtlas: extend any maximal-atlas chart for a boundaryless model to a partial diffeomorphism onto the model vector space.TauCeti.extChartPartialDiffeomorph: an extended chart restricted to the interior of its target, as a partial diffeomorphism onto an open subset of the model space.TauCeti.exists_partialDiffeomorph_comp_extChartAt: a diffeomorphism of the model space composed with an extended chart restricted to an open set, as a partial diffeomorphism with its derivative.TauCeti.PartialDiffeomorph.ofOpenPartialHomeomorph: an open partial homeomorphism between model spaces which isC^nin both directions, as a partial diffeomorphism.TauCeti.isLocalDiffeomorphAt_of_mfderiv_eq: the inverse function theorem for manifolds.TauCeti.isLocalDiffeomorphAt_iff_exists_mfderiv_eq: the resulting characterisation ofIsLocalDiffeomorphAtat an interior point, for a map which isC^non an open set.TauCeti.isLocalDiffeomorphAt_of_injective_mfderiv: in equal finite dimensions, an injective differential suffices.TauCeti.isLocalDiffeomorphAt_of_eqOn: a map agreeing with a partial diffeomorphism on its source is a local diffeomorphism there.OpenPartialHomeomorph.isLocalDiffeomorphAt_of_mem_maximalAtlas: a maximal-atlas chart is a local diffeomorphism at every point of its source.OpenPartialHomeomorph.isLocalDiffeomorphAt_symm_of_mem_maximalAtlas: its inverse is a local diffeomorphism at every point of its target.IsManifold.mem_maximalAtlas_iff_forall_isLocalDiffeomorphAt: conversely, an open partial homeomorphism to the model space which is a local diffeomorphism at every point of its source is a maximal-atlas chart.PartialDiffeomorph.trans_mem_maximalAtlas: a partial diffeomorphism followed by a maximal-atlas chart is a maximal-atlas chart.IsLocalDiffeomorphAt.exists_mem_maximalAtlas_eventuallyEq: a maximal-atlas chart pulls back along a local diffeomorphism to a maximal-atlas chart.IsLocalDiffeomorphAt.exists_mem_maximalAtlas_extend_eventuallyEq: the pulled back chart can be chosen so that coordinate expressions ofg โ fagree with those ofg.IsLocalDiffeomorphAt.eventually: being a local diffeomorphism at a point is an open condition.IsLocalDiffeomorphAt.exists_mem_nhds_injOn: a local diffeomorphism is locally injective.Set.InjOn.exists_isOpen_superset_isLocalDiffeomorphOn: a local diffeomorphism injective on a compact set is injective, and a local diffeomorphism, on an open neighbourhood of it.IsLocalDiffeomorphAt.of_comp_right: a map whose composite with a local diffeomorphism is a local diffeomorphism is itself one.IsLocalDiffeomorphAt.isLocalDiffeomorphAt_comp_iff: the resulting characterisation of local diffeomorphisms out of the target of a local diffeomorphism.IsLocalDiffeomorphAt.of_comp_left: a continuous map followed by a local diffeomorphism is a local diffeomorphism if the composite is one.TauCeti.isLocalDiffeomorph_of_mfderiv_eq: the global version.
A maximal-atlas chart for a boundaryless model, followed by the model, as a partial diffeomorphism to the model vector space.
Instances For
Extending a maximal-atlas chart preserves its source.
The target of the extended chart is read through the inverse model.
The extended chart is the chart followed by the model.
The extended maximal-atlas chart evaluates as the model applied to the original chart.
The inverse extended chart is the inverse model followed by the inverse chart.
The inverse partial diffeomorphism of the extended maximal-atlas chart is the inverse of the extended chart.
The diffeomorphism associated to a bijective local diffeomorphism has the given forward map. This computation rule lets callers use the constructor without unfolding its choice of inverse.
Precomposing a map with a local diffeomorphism does not change the image of its differential.
No differentiability of g is assumed: when g is not differentiable at ฯ x, neither is
g โ ฯ at x, and both differentials are zero.
The extended chart at x, restricted to the interior of its target and regarded as a partial
diffeomorphism from M to the model space E.
Instances For
The source of the restricted extended chart consists of points in the original chart source whose chart coordinates lie in the interior of the chart target.
The center of the restricted extended chart belongs to its source exactly when it is an interior point of the manifold.
The target of the restricted extended chart is the interior of the original chart target.
The forward function of the restricted extended chart agrees with the original extended chart.
The inverse of the restricted extended chart agrees pointwise with the inverse extended chart.
A diffeomorphism of the model space, composed with the extended chart at xโ restricted to the
preimage of an open set Vโ inside the interior of the chart target, is a C^n partial
diffeomorphism with source the restricted chart source, and its differential at a point of the
source is the differential of the diffeomorphism after that of the extended chart.
An open partial homeomorphism between model spaces which is C^n in both directions is a
partial diffeomorphism.
Instances For
A map agreeing with a partial diffeomorphism on its source is a C^n local diffeomorphism at
every point of that source.
A chart in the C^n maximal atlas is a local diffeomorphism at every point of its source.
The inverse of a chart in the C^n maximal atlas is a local diffeomorphism at every point of
its target.
The maximal atlas consists of the local diffeomorphisms to the model. An open partial
homeomorphism to the model space lies in the C^n maximal atlas exactly when it is a C^n local
diffeomorphism at every point of its source.
A partial diffeomorphism ฮฆ : M โ N' followed by a chart e of the maximal C^n atlas of
N' is a chart of the maximal C^n atlas of M.
A chart e of the maximal C^n atlas of N' at f x pulls back along a C^n local
diffeomorphism f at x to a chart of the maximal C^n atlas of M at x, which agrees with
e โ f near x.
A chart c of the maximal C^n atlas of N' at f x pulls back along a C^n local
diffeomorphism f at x to a chart e of the maximal C^n atlas of M at x with the same
extended coordinates at x, in which the coordinate expression of every g โ f is the coordinate
expression of g in c.
Being a local diffeomorphism at a point is an open condition. A C^n local diffeomorphism
at x is a C^n local diffeomorphism at every nearby point.
A local diffeomorphism is locally injective. A C^n local diffeomorphism at x is
injective on a neighbourhood of x, where its local inverse is a left inverse.
A local diffeomorphism injective on a compact set is injective near it. A map into a
Hausdorff manifold which is injective on a compact set K and a C^n local diffeomorphism at every
point of K is injective, and a C^n local diffeomorphism, on an open neighbourhood of K.
Cancelling a local diffeomorphism on the right. If e is a C^n local diffeomorphism at
x and f โ e is a C^n local diffeomorphism at x, then f is a C^n local diffeomorphism at
e x: near e x it is f โ e composed with a local inverse of e.
Composing with a local diffeomorphism on the right. If e is a C^n local diffeomorphism
at x, then f โ e is a C^n local diffeomorphism at x exactly when f is one at e x.
Cancelling a local diffeomorphism on the left. If f is a C^n local diffeomorphism at
e x, the map e is continuous at x, and f โ e is a C^n local diffeomorphism at x, then
e is a C^n local diffeomorphism at x: near x it is f โ e followed by a local inverse of
f. Continuity of e cannot be dropped, since it is what keeps e near x inside the domain of
that local inverse.
The inverse function theorem for manifolds. If f is C^n on an open set s with
1 โค n, x belongs to s and is an interior point, and the differential at x is a
continuous linear equivalence, then f is a C^n local diffeomorphism at x.
Mathlib's Mathlib/Geometry/Manifold/LocalDiffeomorph.lean lists this implication as a TODO.
For a map which is C^n on an open set, with 1 โค n, being a C^n local diffeomorphism at an
interior point is exactly invertibility of the differential there.
The inverse function theorem for manifolds, injective form: between manifolds of the same
finite dimension, a map which is C^n on an open set, with 1 โค n, and has injective differential
at an interior point x of that set is a C^n local diffeomorphism at x.
The inverse function theorem for manifolds, global form: a C^n map (1 โค n) from a
boundaryless source manifold, all of whose differentials are continuous linear equivalences, is a
C^n local diffeomorphism.