Composing immersions with diffeomorphisms, and immersions into finite dimensions #
Mathlib defines Manifold.IsImmersion by a normal form in charts — f looks like u ↦ (u, 0)
for suitable charts of the source and the target — and lists IsImmersion.comp as a TODO in
Mathlib/Geometry/Manifold/Immersion.lean, because a general composite has to combine two
complements and needs the differential to split.
This file settles the special case that is elementary: composing with a diffeomorphism on
either side. Nothing has to be recombined, because a diffeomorphism carries charts to charts: if
φ is a chart of M in the maximal atlas and e : M' ≃ₘ M is a diffeomorphism, then φ ∘ e is
a chart of M' in the maximal atlas, and reading f ∘ e in it produces literally the same normal
form that f had in φ. The same argument on the other side pulls an ambient chart back along
e⁻¹. So both composites are immersions with the same complement.
Since a diffeomorphism is invertible, every composition rule here is in fact an equivalence, and
each is also stated in _iff form. The one-directional statements remain the primitive ones: they
need a manifold structure only on the manifold e introduces, whereas the _iff forms need one on
both sides, in order to apply the rule to e.symm as well.
Main results #
Diffeomorph.transOpenPartialHomeomorph_mem_maximalAtlas(inTauCeti.Geometry.Manifold.PullbackGroupoid): a diffeomorphism pulls a chart of the maximal atlas back to a chart of the maximal atlas. This is the only geometric input.TauCeti.isImmersion_comp_diffeomorphand Mathlib’sManifold.IsImmersion.comp_diffeomorph, together with theirManifold.IsImmersionAt,Manifold.IsImmersionAtOfComplementandManifold.IsImmersionOfComplementcounterparts and the_iffcompanions of all of them: immersions are stable under composition with a diffeomorphism on either side.Diffeomorph.isImmersion: a diffeomorphism is an immersion.TauCeti.isImmersion_comp_continuousLinearEquivand itsManifold.IsImmersionAtandManifold.IsImmersionAtOfComplementcounterparts: precomposing a map on a vector space with a continuous linear equivalenceE₀ ≃L Epreserves immersions, although the source model changes fromEtoE₀.ContinuousLinearMap.HasLeftInverse.isImmersion: a continuous linear map with a continuous linear left inverse is an immersion.TauCeti.isImmersion_prodMkRight_of_extChartAt_eq_zero: the slicex ↦ (c, x)of a productN × Mis an immersion when the preferred chart ofNatcsendscto0.TauCeti.isImmersion_iff_forall_isImmersionAt: for a finite-dimensional target model, a map is an immersion exactly when it is an immersion at every point.Manifold.IsImmersion.nonempty_complement_continuousLinearEquiv: for nonempty manifolds modelled onℝᵏandℝᵐ, the complement of an immersion is a copy ofℝᵐ⁻ᵏ.Manifold.IsImmersion.of_le, together with itsManifold.IsImmersionAt,Manifold.IsImmersionAtOfComplement, andManifold.IsImmersionOfComplementcounterparts: lowering the regularity order preserves immersions.
Manifold.IsImmersion asks for one complement serving every point, so it is not obviously a
local property; Mathlib's docstring of Manifold.IsImmersion.isImmersionAt explains that the
converse of that lemma fails for infinite-dimensional targets. When the target model is
finite-dimensional, every complement of the source model has the same finite dimension, so any
two of them are isomorphic and pointwise immersions assemble to an immersion. This makes being
an immersion local, as needed to glue immersions defined on the pieces of an open cover.
References #
- M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 1, for immersions and their behaviour under composition.
Precomposing with a diffeomorphism of the source preserves the immersion normal form at a
point, with the same complement: the domain chart of the immersion is pulled back along the
diffeomorphism, and f ∘ e read in the new chart is what f was in the old one.
Precomposing with a diffeomorphism of the source preserves being an immersion at a point.
Precomposing an immersion with a fixed complement by a diffeomorphism of the source gives an immersion with the same complement.
Reparametrising an immersion by a diffeomorphism of the source gives an immersion.
Precomposition with a diffeomorphism of the source neither creates nor destroys the immersion normal form at a point.
Precomposition with a diffeomorphism of the source neither creates nor destroys an immersion at a point.
Precomposition with a diffeomorphism of the source neither creates nor destroys an immersion with a fixed complement.
Precomposition with a diffeomorphism of the source neither creates nor destroys an immersion.
Postcomposition with a diffeomorphism of the target neither creates nor destroys the immersion normal form at a point.
Postcomposition with a diffeomorphism of the target neither creates nor destroys an immersion at a point.
Postcomposition with a diffeomorphism of the target neither creates nor destroys an immersion with a fixed complement.
Postcomposition with a diffeomorphism of the target neither creates nor destroys an immersion.
Every diffeomorphism is an immersion.
Changing the model of a vector space source by a linear equivalence #
Precomposing a map on a vector space with a continuous linear equivalence e : E₀ ≃L E
preserves the immersion normal form at a point, with the same complement, although the source
model changes from E to E₀: a domain chart ψ of E is carried to the chart e⁻¹ ∘ ψ ∘ e
of E₀, and the linear isomorphism of the normal form absorbs e.
Precomposing a map on a vector space with a continuous linear equivalence preserves being an immersion at a point.
Precomposing an immersion of a vector space with a continuous linear equivalence gives an immersion, for the new source model.
Linear maps with a continuous left inverse #
A continuous linear map f : E →L F with a continuous linear left inverse g is a C^n
immersion, with complement ker g: the continuous linear equivalence F ≃L E × ker g sending y
to (g y, y - f (g y)) carries f to the inclusion u ↦ (u, 0). For instance, the inclusion
of a closed complemented subspace is an immersion.
Slices of a product #
Slices of a product. If the preferred chart of N at c sends c to 0, then the slice
x ↦ (c, x) of the product N × M is a C^n immersion with complement E': in product charts
it is the inclusion u ↦ (0, u).
Immersions into finite-dimensional models #
For a finite-dimensional target model, being an immersion is a pointwise condition: the complements at different points are isomorphic, so they can be replaced by a single one.
Euclidean complements #
The complement of a C^n immersion of a nonempty manifold modelled on ℝᵏ, possibly with
boundary or corners, into a manifold modelled on ℝᵐ is a copy of ℝʲ, for j = m - k: the
immersion's normal form at any point splits ℝᵐ as ℝᵏ times the complement.
Monotonicity in the regularity order #
Lowering the regularity order preserves the immersion normal form at a point, with the same complement.
Lowering the regularity order preserves being an immersion at a point.
Lowering the regularity order preserves immersions with a fixed complement.
Lowering the regularity order preserves immersions.