The Lefschetz–Whitehead rank estimate

Let g, h : E → F be maps into a finite-dimensional space and consider the swept map (y, t) ↦ g y + t • h y, which moves the point g y along the line through it in the direction h y. Its derivative at (x, t) sends (e, s) to g' e + t • h' e + s • h x, so its range is range (g' + t • h') ⊔ 𝕜 ∙ h x: a pencil in t, together with the fixed line spanned by h x. If the swept map has rank at most p at (x, t) for infinitely many t, for instance for all t near 0, then the rank bound passes to the direction of the pencil (LinearMap.finrank_range_sup_le_of_infinite). When h x is transverse to the range of h', the line 𝕜 ∙ h x contributes one more dimension, so h has rank at most p - 1 at x.

This is Lemma 2 of Łojasiewicz's triangulation of semianalytic sets, where h takes values in an (m - 1)-dimensional submanifold S of an m-dimensional space with u ∉ T_u S for u ∈ S. The range of h' lies in the tangent space of S at h x, so the transversality hypothesis h x ∉ range h' used here is implied by the one in the source. In Łojasiewicz's Lemma 3, directions are represented by unit vectors and S is the unit sphere; then transversality holds because the derivative of a map of constant nonzero norm is orthogonal to its value.

Main results

• HasFDerivAt.finrank_range_lt_of_infinite: the Lefschetz–Whitehead rank estimate for a direction field h with h x ∉ range h'.
• HasFDerivAt.finrank_range_lt_of_infinite_of_norm_eq: the same for a direction field of locally constant nonzero norm, such as a map into the unit sphere.

References

• S. Łojasiewicz, Triangulation of semi-analytic sets, Ann. Scuola Norm. Sup. Pisa (3) 18 (1964), 449–474, §2, Lemma 2.

theorem HasFDerivAt.finrank_range_lt_of_infinite {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g h : E → F} {g' h' : E →L[𝕜] F} {x : E} [FiniteDimensional 𝕜 F] (hh : HasFDerivAt h h' x) (hg : HasFDerivAt g g' x) (hx : h x ∉ (↑h').range) {p : ℕ} (hp : {t : 𝕜 | Module.finrank 𝕜 ↥(↑(fderiv 𝕜 (fun (q : E × 𝕜) => g q.1 + q.2 • h q.1) (x, t))).range ≤ p}.Infinite) : Module.finrank 𝕜 ↥(↑h').range < p

The Lefschetz–Whitehead rank estimate. Let g and h be differentiable at x, with h x outside the range of the derivative h' of h. If the swept map (y, t) ↦ g y + t • h y has rank at most p at (x, t) for infinitely many t, for instance for every t near 0, then h has rank less than p at x.

theorem HasFDerivAt.finrank_range_lt_of_infinite_of_norm_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {g h : E → F} {g' h' : E →L[ℝ] F} {x : E} (hh : HasFDerivAt h h' x) (hg : HasFDerivAt g g' x) (hn : ∀ᶠ (y : E) in nhds x, ‖h y‖ = ‖h x‖) (h0 : h x ≠ 0) {p : ℕ} (hp : {t : ℝ | Module.finrank ℝ ↥(↑(fderiv ℝ (fun (q : E × ℝ) => g q.1 + q.2 • h q.1) (x, t))).range ≤ p}.Infinite) : Module.finrank ℝ ↥(↑h').range < p

The Lefschetz–Whitehead rank estimate for unit directions. Let g and h be differentiable at x, where h x ≠ 0 and ‖h‖ is constant near x, for instance a map into the unit sphere. If the swept map (y, t) ↦ g y + t • h y has rank at most p at (x, t) for infinitely many t, then h has rank less than p at x.