Linearizing an embedding at a fixed point

Let f : E → F be a C^(n+1) map between real normed spaces, with F complete, which is a C^n smooth embedding, fixes the origin, and has a continuous linear equivalence L as its derivative there. Rescaling f about the origin gives the embeddings x ↦ t⁻¹ • f (t • x) for 0 < t ≤ 1, which converge to L as t → 0. Hadamard's factorization f y = A y y, with A y the derivative of f averaged along the segment from 0 to y (hadamardFactor f 0), writes the rescaled map as x ↦ A (t • x) x. This formula still makes sense at t = 0, where it is L, and is jointly C^n in (t, x). The result is a smooth isotopy TauCeti.linearizationIsotopy from L to f through embeddings, all of which fix the origin.

The isotopy supplies the vector-space linearization step in the proof of the disc theorem, replacing an embedding of ℝⁿ fixing the origin by its derivative there. In this vector-space case, connecting the derivatives uses the connectedness of the group of linear maps of positive determinant. The general-manifold disc theorem says that two embeddings of ℝⁿ into a manifold, sending 0 to the same point, whose derivatives at 0 differ by a linear map of positive determinant, are isotopic rel 0. That case also requires shrinking the embeddings into a common chart and assembling the isotopy; these steps are not supplied by this construction.

Main definitions and results

• TauCeti.linearizationIsotopy: the smooth isotopy from the derivative L at the origin to f.
• TauCeti.linearizationIsotopy_apply_of_ne_zero: at a nonzero time t the isotopy is the rescaling x ↦ t⁻¹ • f (t • x); at time 0 it is L (SmoothIsotopy.apply_zero).
• TauCeti.linearizationIsotopy_apply_mk_zero: every stage of the isotopy fixes the origin.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 4, Theorem 6.6 (the disc theorem) and the isotopy of tubular neighbourhoods used in its proof.
• R. Palais, Extending diffeomorphisms, Proc. Amer. Math. Soc. 11 (1960), 274–277, for the disc theorem.

noncomputable def TauCeti.linearizationIsotopy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {n : ℕ∞} (f : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ F) (↑n) E F) (L : E ≃L[ℝ] F) (hf : ContDiff ℝ (↑n + 1) ⇑f) (hL : HasFDerivAt (⇑f) (↑L) 0) (hf0 : f 0 = 0) : SmoothIsotopy (SmoothEmbedding.ofContinuousLinearEquiv L).toContMDiffMap f.toContMDiffMap

The linearization isotopy. A smooth embedding f : E → F which is C^(n+1), fixes the origin, and has derivative a continuous linear equivalence L there, is smoothly isotopic to L. At time t ≠ 0 the isotopy is the rescaling x ↦ t⁻¹ • f (t • x) (linearizationIsotopy_apply_of_ne_zero), at time 0 it is L, and it fixes the origin throughout (linearizationIsotopy_apply_mk_zero).

theorem TauCeti.linearizationIsotopy_apply_of_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {n : ℕ∞} {g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ F) (↑n) E F} {L : E ≃L[ℝ] F} {hg : ContDiff ℝ (↑n + 1) ⇑g} {hL : HasFDerivAt (⇑g) (↑L) 0} {hg0 : g 0 = 0} {t : ↑unitInterval} (ht : ↑t ≠ 0) (x : E) : (linearizationIsotopy g L hg hL hg0) (t, x) = (↑t)⁻¹ • g (↑t • x)

At a nonzero time t, the linearization isotopy is the rescaling x ↦ t⁻¹ • g (t • x).

@[simp]

theorem TauCeti.linearizationIsotopy_apply_mk_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {n : ℕ∞} {g : SmoothEmbedding (modelWithCornersSelf ℝ E) (modelWithCornersSelf ℝ F) (↑n) E F} {L : E ≃L[ℝ] F} {hg : ContDiff ℝ (↑n + 1) ⇑g} {hL : HasFDerivAt (⇑g) (↑L) 0} {hg0 : g 0 = 0} (t : ↑unitInterval) : (linearizationIsotopy g L hg hL hg0) (t, 0) = 0

Every stage of the linearization isotopy fixes the origin.