# 3 Global theory of open and ample relations

# 3.1 Preliminaries

## 3.1.1 Localisation data

In order to conveniently globalize the theory of the previous chapter, we’ll need a number of constructions and lemmas. By definition, manifolds are covered by open sets that are diffeomorphic to open sets of vector spaces. But for us it is slightly more convenient to work with smooth open embeddings of whole vector spaces. Here a smooth open embedding from a manifold \(X\) to a manifold \(Y\) is a smooth map \(φ : X → Y\) which is open and for which there is some smooth \(ψ : φ(X) → X\) such that \(ψ ∘ φ = \operatorname{Id}_X\) (hence also and \(φ ∘ ψ = \operatorname{Id}_{φ(X)}\)). Remember that a family of sets \(V_i\) in a topological space \(X\) is locally finite if every point of \(X\) has a neighborhood that intersects only finitely many \(V_i\). Note that in this whole text, every manifold is paracompact by definition. In particular their topology are metrizable and we will arbitrarily fix a compatible distance function on every manifold.

Given smooth open embeddings \(φ : X → M\) and \(ψ : Y → N\), the update of a map \(f : M → N\), using a map \(g : X → Y\) is the map from \(M\) to \(N\) sending \(m\) to \(ψ ∘ g ∘ φ⁻¹(m)\) if \(m ∈ φ(X)\) and \(f(m)\) otherwise.

Let \(φ : P × X → M\) and \(ψ : P × Y → N\) be families of smooth open embeddings. Let \(K\) be a set in \(X\) whose image in \(M\) is closed. Let \(f : P × M → N\) and \(g : P × X → Y\) be smooth families of maps. If for each \(p\) and for every \(x\) not in \(K\), \(f_p(φ(x)) = ψ(g_p(x))\) then the family of maps \(f_p\) updated using \(g_p\) is smooth from \(P × M\) to \(N\).

Note that \(P × M = (P × φ(X)) ∪ (P × φ(K)^c)\). Both those sets are open and the updated maps coincide with \((p, m) ↦ ψ ∘ g_p ∘ φ⁻¹(m)\) on the first one and \(f\) on the second one.

Let \(φ : X → M\) and \(ψ : Y → N\) be smooth open embeddings. Let \(K_X\) and \(K_P\) be compact sets in \(X\) and \(P\). Let \(f : P × M → N\) be a continuous family of maps such that, for each \(p\), \(f_p(φ(X)) ⊂ ψ(Y)\). For every continuous function \(ε : M → ℝ_{{\gt} 0}\), there is some positive number \(η\) such that, for every map \(g : P × X → Y\) and every \((p, p', x)\) in \(K_P × K_P × K_X\), \(d(g_{p'}(x), ψ⁻¹∘f_p∘φ(x)) {\lt} η\) implies \(d(f'_{p'}(φ(x)), f_p(φ(x))) {\lt} ε(φ(x))\) where \(f'\) is obtained by updating \(f\) using \(g\).

Let \(ε\) be a positive continuous function on \(M\). Since \(K_X\) is compact, we get a positive number \(ε₀\) such that \(ε(m) ≥ ε₀\) for each \(m\) in \(K_X\). We denote by \(K₁\) the closed \(1\)-thickening of the image of \(K_P × K_X\) under \((p, x) ↦ ψ⁻¹∘f_p∘φ(x)\). This is a compact set so \(ψ\) is uniformly continuous on \(K₁\) and we get a positive \(τ\) such that for all \(x\) and \(y\) in \(K₁\), \(d(x, y) {\lt} τ ⇒ d(ψ(x), ψ(y)) {\lt} ε₀\).

We now prove that \(η = \min (τ, 1)\) is suitable. Fix \((p, p', x)\) in \(K_P × K_P × K_X\) such that \(d(g_{p'}(x), ψ⁻¹∘f_p∘φ(x)) {\lt} η\). In particular \(d(g_{p'}(x), ψ⁻¹∘f_p∘φ(x)) {\lt} 1\) hence \(g_{p'}(x)\) is in \(K₁\). Since \(ψ⁻¹∘f_p∘φ(x)\) is also in \(K₁\) and \(d(g_{p'}(x), ψ⁻¹∘f∘φ(x)) {\lt} τ\), we get \(d(ψ∘ g_{p'}(x), ψ ∘ ψ⁻¹∘f_p∘φ(x)) {\lt} ε₀\). This precisely means that \(d(f'_{p'}(φ(x)), f_p(φ(x)) {\lt} ε₀\). Since \((p, p', x)\) is in \(K_P × K_P × K_X\), this is less than \(ε(m)\).

In order to handle in a uniform way compact and non-compact manifolds, we will index sequences by the family of sets \(\mathcal{I}_{N}\) defined for each natural number \(N\) by:

Let \(M\) be a manifold modelled on the normed space \(E\) and \((V_j)_{j ∈ J}\) a cover of \(M\) by open sets. There exists some natural number \(N\) and a family of smooth open embeddings \(φ : \mathcal{I}_{N} × E → M\) such that

for each \(i\) there is some \(j\) such that \(φ_i(E) \subseteq V_j\),

\(i ↦ φ_i(E)\) is a locally-finite collection of sets in \(M\),

\(⋃_i φ_i(B_E(0, 1)) = M\) where \(B_E(0, 1)\) is the open unit ball in \(E\).

The proof is a standard compact-exhaustion argument. Let \(K_0, K_1, K_2, \ldots \) be a compact exhaustion of \(M\) and define:

Thus:

\(C_n\) is compact,

\(U_n\) is open,

\(C_n \subseteq U_n\),

\(\bigcup _n C_n = M\),

\(U_n \cap U_m = \emptyset \) if \(|n - m| {\gt} 2\).

For any \(y \in E\) and \(r {\gt} 0\), fix a smooth diffeomorphism \(f_{y,r} : E \simeq B_E(y, r)\) such that \(f_{y,r}(0) = y\). For each \(n\) and \(x \in C_n\), let \(\psi _x\) be a smooth chart mapping an open neighbourhood of \(x\) to an open set of the model space \(E\). Writing \(y = \psi _x (x) \in E\), let:

for some \(r {\gt} 0\) (which may depend on \(n\), \(x\)) sufficiently small that:

\(B_E(y, r)\) lies in the target of the chart \(\psi _x\),

\(B_{n,x}\) is contained in \(U_n\),

\(B_{n,x}\) is contained in \(V_j\) for some \(j\).

Note that \(x \in W_{n,x}\). For each \(n\), choose a finite subcovering of \(C_n\) by \(W_{n, x_1}, \ldots , W_{n, x_{l_n}}\) and define \(\iota \subseteq ℕ \times M\) by:

Note that \(\iota \) is countable and furthermore:

for each \(i \in \iota \), there is some \(j\) such that \(B_i \subseteq V_j\),

\((B_i)_{i \in \iota }\) is locally-finite (indeed more is true: \(B_i\) meets only finitely-many \(B_{i'}\) for \(i, i' \in \iota \) since \(B_{m, x} \cap B_{n, x'} = \emptyset \) if \(|n - m| {\gt} 2\)),

\((W_i)_{i \in \iota }\) covers \(M\).

Given \(i = (n, x_j) \in \iota \), the required map \(\phi _i : E \to M\) is just:

Since \(ι\) is countable, it is in bijection with some \(\mathcal{I}_{N}\).

Let \(f : M → N\) be a continuous map between manifolds. A localisation data for \(f\) is a tuple \((E, F, N, ι, φ, ψ, j)\) where \(E\) and \(F\) are normed vector spaces, \(N\) is a natural number, \(ι\) is a set, \(φ : \mathcal{I}_{N} × E → M\) and \(ψ : ι × F → N\) are families of smooth open embeddings, and \(j : \mathcal{I}_{N} → ι\) such that:

\(⋃_i φ_i(B_E) = M\) where \(B_E\) is the open unit ball in \(E\),

\(⋃_i ψ_i(B_F) = N\) where \(B_F\) is the open unit ball in \(F\),

\(∀ i, f(φ_i(E)) ⊂ ψ_{j(i)}(B_F)\) where \(B_F\) is the open unit ball in \(F\),

\(i \mapsto ψ_i(F)\) is locally finite.

Such a tuple will be denoted by \((φ, ψ, j)\) for brevity.

Any continuous map between manifolds has some localisation data.

The preceding lemma (applied to the trivial cover of \(N\) by itself) gives a family of \(ψ : ι' × F → N\) of open smooth embeddings that the images of \(B_F\) cover \(N\). We then apply this lemma again to the cover of \(M\) given by all \(f⁻¹(ψ_j(B_F))\).

The general idea will be to apply the results of the previous chapters to all the \(ψ_{j(i)}⁻¹ ∘ f ∘ φ_i : E → F\) for some maps \(f\). However we must be careful that doing this for some \(i\) does not ruin the setup for the next \(i\). This is easier to control using a distance function on the target manifold as in Lemma 3.8 below. First we need a general lemma about a single metric space (actually the formalized statement is stronger, it assumes only closed sets instead of compact ones, but here we explain the easier proof which is sufficient for our purposes).

In a metric space \(X\), let \(U : ι → \operatorname{\mathcal{P}}{X}\) be a family of open subsets of \(X\) and let \(K : ι → \operatorname{\mathcal{P}}{X}\) be a locally-finite family of closed subsets such that \(K_i ⊂ U_i\) for all \(i\). There exists a continuous function \(δ : X → ℝ_{{\gt} 0}\) such that:

We first note that, for any given \(i\), compactness of \(K\) and openness of \(V_i\) give a positive number \(δ_i\) such that the \(δ_i\)-neighborhood of \(K_i\) is contained in \(V_i\). We now prove that solutions exist locally. Let \(x\) be any point in \(X\). From the local finiteness assumption, we get a neighborhood \(U\) of \(x\) such that \(\{ i | U ∩ V_i ≠ ∅\} \) is finite. The constant function with value the minimum of the corresponding \(δ_i\) is a solution on \(U\). Since the condition we put on \(δ\) is convex, we can glue those local solutions using Lemma 1.16.

Let \(f : M → N\) be a continuous map between manifolds, and let \((φ, ψ, i)\) be some localisation data for \(f\). There exists a continuous positive function \(ε : M → ℝ_{{\gt}0}\) such that:

Note that, in the preceding lemma, the conclusion \(g(φ_i(E)) ⊂ ψ_{j(i)}(F)\) is weaker than the condition \(f(φ_i(E)) ⊂ ψ_{j(i)}(B_F)\) that appears in the definition of localisation data.

The condition \(∀ m,\; d(g(m), f(m)) {\lt} ε(m)\) will be abbreviated \(d(g, f) {\lt} ε\).

The preceding lemma applied to the family of open sets \(ψ_j(F)\) and the family of compact sets \(ψ_j(\overline{B_F})\) give a positive continuous function \(δ : N → ℝ\) such that \(ε = δ ∘ f\) is suitable. Indeed, assume \(g : M → N\) satisfies \(d(g, f) {\lt} ε\) and fix some \(i\) and some \(m ∈ φ_i(E)\). We know \(f(m) ∈ ψ_{j(i)}(\overline{B_F})\) and our assumption on \(g\) gives \(d(g(m), f(m)) {\lt} δ(f(m))\). So the property of \(δ\) ensures \(g(m) ∈ ψ_{j(i)}(F)\).

## 3.1.2 Jets spaces

We now need to introduce the bundles that will replace the jet spaces \(E × F × \operatorname{Hom}(E, F)\) from the previous chapter. We need a couple of fiber bundles constructions.

For every bundle \(p : E → B\) and every map \(f \! :B' → B\), the pull-back bundle \(f^*E → B'\) is defined by \(f^*E = \{ (b', e) ∈ B' × E \; |\; p(e) = f(b')\} \) with the obvious projection to \(B'\).

Let \(E → B\) and \(F → B\) be two vector bundles over some smooth manifold \(B\). The bundle \(\operatorname{Hom}(E, F) → B\) is the set of linear maps from \(E_b\) to \(F_b\) for some \(b\) in \(B\), with the obvious projection map.

Set-theoretically, one can define \(\operatorname{Hom}(E, F)\) as the set of subsets \(S\) of \(E × F\) such that there exists \(b\) such that \(S ⊂ E_b × F_b\) and \(S\) is the graph of a linear map. But the type theory formalization will use other tricks here. The facts that really matter are listed in lemma 3.13 below.

Let \(M\) and \(N\) be smooth manifolds. Denote by \(p_1\) and \(p_2\) the projections of \(M × N\) to \(M\) and \(N\) respectively.

The space \(J^1(M, N)\) of \(1\)-jets of maps from \(M\) to \(N\) is \(Hom(p_1^*TM, p_2^*TN)\)

We will use notations like \((m, n, φ)\) to denote an element of \(J^1(M, N)\), but one should keep in mind that \(J^1(M, N)\) is not a product, since \(φ\) lives in \(\operatorname{Hom}(T_mM, T_nN)\) which depends on \(m\) and \(n\).

The \(1\)-jet of a smooth map \(f \! :M → N\) is the map from \(m\) to \(J^1(M, N)\) defined by \(j^1f(m) = (m, f(m), T_mf)\).

The composition of a section \(\mathcal{F}\! :M → J^1(M, N)\) with the projection onto \(N\) will sometimes be denoted by \(\operatorname{bs}\mathcal{F}\! :M → N\) and called the base map of \(\mathcal{F}\). For any \(m\), \(\mathcal{F}(m)_φ\) will denote the component of \(\mathcal{F}(m)\) living in \(\operatorname{Hom}(T_mM, T_{\operatorname{bs}\mathcal{F}(m)}N)\).

For every smooth map \(f \! :M → N\),

\(j^1f\) is smooth

\(j^1f\) is a section of \(J^1(M, N) → M\)

Points 2 and 3 are obvious by construction.

To show that \(j^1f\) is smooth, suppose that \(M\) is modelled over \(E\) with charts \(C_x : M \to E\) and coordinate change functions \(C_{x,x'}=C_{x'}C_x^{-1} : E \to E\) and similarly let \(C'_y\) be charts for \(N\). By construction of the 1-jet bundle, we need to check that for each \(x_0\) the map

is smooth at \(x_0\) (we occasionally omit the point where the tangent maps are taken). For \(x\) close to \(x_0\) the coordinate changes are smooth, so we can write

This is smooth since \(C'_{f(x_0)}fC_{x_0}\) is smooth.

A section \(\mathcal{F}\) of \(J^1(M, N) → M\) is called holonomic if it is the \(1\)–jet of its base map. Equivalently, \(\mathcal{F}\) is holonomic if there exists \(f \! :M → N\) such that \(\mathcal{F}= j^1f\), since such a map is necessarily \(\operatorname{bs}\mathcal{F}\).

# 3.2 First order differential relations

A first order differential relation for maps from \(M\) to \(N\) is a subset \(\mathcal{R}\) of \(J^1(M, N)\).

A formal solution of a differential relation \(\mathcal{R}⊂ J^1(M, N)\) is a section of \(J^1(M, N) → M\) taking values in \(\mathcal{R}\).

A homotopy of formal solutions of \(\mathcal{R}\) is a smooth family of sections \(\mathcal{F}: ℝ × M → J^1(M, N)\) such that each \(m ↦ \mathcal{F}(t, m)\) is a formal solution.

The next definition will be used in cases where \(X\) and \(Y\) are vector spaces, in order to relate the global theory to the local one.

Given manifolds \(M\), \(X\), \(N\) and \(Y\) and smooth open embeddings \(g : Y → N\) and \(h : X → M\) we get a transfer map \(ψ_{g, h} : J^1(X, Y) → J^1(M, N)\) defined by

and an operator on sections which sends \(\mathcal{F}: M → J^1(M, N)\) to \(Ψ_{g, h}\mathcal{F}: X → J^1(X, Y)\) defined when \(\operatorname{bs}\mathcal{F}(h(X)) ⊂ g(Y)\) by

Given a relation \(\mathcal{R}⊂ J^1(M, N)\), the induced relation in \(J^1(X, Y)\) is \(ψ_{g, h}⁻¹\mathcal{R}\).

The following is a localization lemma needed to take advantage of all the work from the previous chapter.

In the situation of the previous definition, given a section \(\mathcal{F}: M → J^1(M, N)\):

\(Ψ_{g, h}(\mathcal{F})\) is a smooth section of \(J^1(X, Y)\).

\(\mathcal{F}\) is holonomic on \(s ⊂ h(X) ∩ \operatorname{bs}\mathcal{F}⁻¹(g(Y))\) if and only if \(Ψ_{g, h}(\mathcal{F})\) is holonomic on \(h⁻¹(s)\).

\(\mathcal{F}\) is a formal solution of \(\mathcal{R}\) on \(h(X) ∩ \operatorname{bs}\mathcal{F}⁻¹(g(Y)\) if and only if \(Ψ_{g, h}(\mathcal{F})\) is a formal solution of the induced relation \(Ψ_{g, h}⁻¹\mathcal{R}\).

The first point is clear by composition. In order to prove the second point while keeping notations under control, we set \(f(x) = g⁻¹ ∘ \operatorname{bs}\mathcal{F}∘ h\). Using this notation \(Ψ_{g, h}\mathcal{F}(x) = (x, f(x), (T_{f(x)}g)⁻¹ ∘ \mathcal{F}(h(x))_φ ∘ T_xh)\). We have

hence \(Ψ_{g, h}\mathcal{F}\) is holonomic at \(x\) if and only if \(\left(T_{f(x)}g\right)⁻¹ ∘ \mathcal{F}(h(x))_φ ∘ T_xh = \left(T_{f(x)}g\right)⁻¹ ∘ T_{h(x)}\operatorname{bs}\mathcal{F}∘ T_x h\) and this is equivalent to \(\mathcal{F}(h(x))_φ = T_{h(x)}\operatorname{bs}\mathcal{F}\) which is the holonomy condition for \(\mathcal{F}\) at \(h(x)\).

The third point is a direct consequence of the easy formula \(ψ_{g, h} ∘ Ψ_{g, h}(\mathcal{F}) = F ∘ h\).

A first order differential relation \(\mathcal{R}⊂ J^1(M, N)\) satisfies the \(h\)-principle if every formal solution of \(\mathcal{R}\) is homotopic to a holonomic one. It satisfies the parametric \(h\)-principle if, for every manifold \(P\) and every closed set \(C\) in \(P × M\), every family \(\mathcal{F}: P × M → J^1(M, N)\) of formal solutions which are holonomic for \((p, m)\) near \(C\) is homotopic to a family of holonomic ones relative to \(C\).

## Parametricity for free

In many cases, relative parametric \(h\)-principles can be deduced from relative non-parametric ones with a larger source manifold. Let \(X\), \(P\) and \(Y\) be manifolds, with \(P\) seen a parameter space. Denote by \(Ψ\) the map from \(J^1(X × P, Y)\) to \(J^1(X, Y)\) sending \((x, p, y, ψ)\) to \((x, y, ψ ∘ ι_{x, p})\) where \(ι_{x, p} : T_xX → T_xX × T_pP\) sends \(v\) to \((v, 0)\).

To any family of sections \(F_p : x ↦ (f_p(x), φ_{p, x})\) of \(J^1(X, Y)\), we associate the section \(\bar F\) of \(J^1(X × P, Y)\) sending \((x, p)\) to \(\bar F(x, p) := (f_p(x), φ_{p, x} ⊕ ∂f/∂p(x, p))\).

In the above setup, we have:

\(\bar F\) is holonomic at \((x, p)\) if and only if \(F_p\) is holonomic at \(x\).

\(F\) is a family of formal solutions of some \(\mathcal{R}⊂ J^1(X, Y)\) if and only if \(\bar F\) is a formal solution of \(\mathcal{R}^P := Ψ^{-1}(\mathcal{R})\).

For the first part, the derivative of \(\bar F\) is \(∂f/∂x(x, p) ⊕ ∂f/∂p(x, p)\), which is equal to \(\bar F_φ\) iff \(∂f/∂x(x, p) = f_φ\).

The second part follows from \(Ψ ∘ \bar F(x,p)=F_p(x)\).

Let \(\mathcal{R}\) be a first order differential relation for maps from \(M\) to \(N\). If, for every manifold with boundary \(P\), \(\mathcal{R}^P\) satisfies the \(h\)-principle then \(\mathcal{R}\) satisfies the parametric \(h\)-principle. Likewise, the \(C^0\)-dense and relative \(h\)-principle for all \(\mathcal{R}^P\) imply the parametric \(C^0\)-dense and relative \(h\)-principle for \(\mathcal{R}\).

By lemma 3.21 we can turn a formal solution of \(\mathcal{R}\) into a formal solution of \(\mathcal{R}^P\), so we get a homotopy to a holonomic formal solution. We can turn this homotopy back to a homotopy of the original formal solution.

# 3.3 The \(h\)-principle for open and ample differential relations

In this chapter, \(X\) and \(Y\) are smooth manifolds and \(\mathcal{R}\) is a first order differential relation on maps from \(X\) to \(Y\): \(\mathcal{R}⊂ J^1(X, Y)\). For any \(σ = (x, y, φ)\) in \(\mathcal{R}\) and any dual pair \((λ, v) ∈ T^*_xX × T_xX\), we set:

where \(\operatorname{Conn}_a A\) is the connected component of \(A\) containing \(a\). In order to decipher this definition, it suffices to notice that \(φ + (w - φ(v))⊗λ\) is the unique linear map from \(T_xX\) to \(T_yY\) which coincides with \(φ\) on \(\ker λ\) and sends \(v\) to \(w\). In particular, \(w = φ(v)\) gives back \(φ\).

Of course we will want to deal with more than one point, so we will consider a vector field \(V\) and a \(1\)–form \(λ\) such that \(λ(V) = 1\) on some subset \(U\) of \(X\), a formal solution \(F\) (defined at least on \(U\)), and get the corresponding \(\mathcal{R}_{F, λ, v}\) over \(U\).

One easily checks that \(\mathcal{R}_{σ, κ^{-1}λ, κv} = κ\mathcal{R}_{σ, λ, v}\) hence the above definition only depends on \(\ker λ\) and the direction \(ℝV\).

A relation \(\mathcal{R}\) is ample if, for every \(σ = (x, y, φ)\) in \(\mathcal{R}\) and every \((λ, v)\), the slice \(\mathcal{R}_{σ, λ, v}\) is ample in \(T_yY\).

Given manifolds \(W\), \(X\), \(Y\) and \(Z\) and smooth open embeddings \(g : Z → Y\) and \(h : W → X\), the relation induced (in the sense of Definition 3.18) in \(J^1(W, Z)\) by an ample relation in \(J^1(X, Y)\) is ample.

By definition, the relation induced by \(\mathcal{R}\) is \(ψ_{g, h}⁻¹\mathcal{R}\) where \(ψ_{g, h}(w, z, φ) = (h(w), g(z), T_zg ∘ φ ∘ (T_wh)⁻¹)\). Fix \(σ =(w, z, φ) ∈ ψ_{g, h}⁻¹\mathcal{R}\) and a dual pair \((λ, v)\) on \(T_wW\). We set \(G = T_z g\) and \(H = T_w h\). Both those maps are linear isomorphisms. We compute the slice corresponding to \((σ, λ, v)\):

Hence the slice \(ψ_{g, h}⁻¹\mathcal{R}(σ, λ, v)\) is the image of a slice of \(\mathcal{R}\) under a linear isomorphism, hence ample.

The relation of immersions of \(M\) into \(N\) in positive codimension is open and ample.

For every \(σ = (x, y, φ)\) in the immersion relation \(\mathcal{R}\), and for every dual pair \((π, v)\), the slice \(\mathcal{R}(σ, π, v)\) is the set of \(w\) which do not belong to the image of \(\ker π\) under \(φ\). Since \(\dim M {\gt} \dim N\), this image has codimension at least \(2\) in \(T_yN\), and lemma 2.13 concludes.

For any manifolds \(X\) and \(Y\), any relation \(\mathcal{R}⊂ J^1(X, Y)\) that is open and ample satisfies the full \(h\)-principle (relative, parametric and \(C^0\)-dense).

We first explain how to get rid of parameters, using the relation \(\mathcal{R}^P\) for families of solutions parametrized by \(P\).

If \(\mathcal{R}\) is ample then, for any parameter space \(P\), \(\mathcal{R}^P\) is also ample.

We fix \(σ = (x, y, ψ)\) in \(\mathcal{R}^P\). For any \(λ = (λ_X, λ_P) ∈ T^*_xX × T^*_pP\) and \(v = (v_X, v_P) ∈ T_xX × T_pP\) such that \(λ(v) = 1\), we need to prove that \(\operatorname{Conv}\mathcal{R}^P_{σ, λ, v} = T_yY\). Unfolding the definitions gives:

A degenerate but easy case is when \(λ_X = 0\). Then the condition on \(w\) becomes \(ψ ∘ ι_{x, p} ∈ \mathcal{R}\), which is true by definition of \(\mathcal{R}^P\), so \(\mathcal{R}^P_{σ, λ, v} = T_yY\).

We now assume \(λ_X\) is not zero and choose \(u ∈ T_xX\) such that \(λ_X(u) = 1\). We then have \(\mathcal{R}^P_{σ, λ, v} = \mathcal{R}_{Ψσ, λ_X, u} + ψ(v) - ψ∘ι_{x, p}(u)\). Because \(\mathcal{R}\) is ample and taking convex hull commutes with translation, we get that \(\operatorname{Conv}\mathcal{R}^P_{σ, λ, v} = T_yY\).

Lemmas 3.22 and 3.27 prove we can assume there are no parameters. So we start with a single formal solution \(F₀\) of \(\mathcal{R}\), which is holonomic near some closed subset \(A ⊂ X\). We also fix a positive continuous function \(δ\) on \(X\) and we want to build a homotopy of formal solutions starting at \(F₀\) relative to \(A\) with base map staying at distance at most \(δ\) from the base map of \(F₀\) and ending at a holonomic solution.

We apply lemma 3.6 to get some localisation data \((φ \! :\mathcal{I}_{N} × E → \operatorname{\mathcal{P}}{X}, ψ \! :ι × E' → \operatorname{\mathcal{P}}{Y}, j)\) for \(\operatorname{bs}F₀ : X → Y\). Lemma 3.8 then provides a continuous function \(ε : X → ℝ_{{\gt} 0}\) such that every function \(g\) with \(d(\operatorname{bs}F₀, g) {\lt} ε\) sends each \(φ_i(E)\) into \(ψ_{j(i)}(E')\). We denote by \(τ\) the positive continuous function \(\min (δ, ε)\).

We then use the inductive construction of homotopies provided by Lemma B.6 starting with \(F₀\) and using the following local predicates. On maps \(F\) from \(X\) to \(J¹(X, Y)\) we use the background predicate \(P₀\) asserting that \(F\) is a smooth section of \(J¹(X, Y) → X\) that takes values in \(R\), coincides with \(F₀\) near \(A\) and satisfies \(d(\operatorname{bs}F, \operatorname{bs}F₀) {\lt} τ\). The background predicate for maps from \(ℝ × X\) to \(J¹(X, Y)\) is simply smoothness and the target local predicate \(P₁\) on maps from \(X\) to \(J¹(X, Y)\) is being holonomic. We use the family of sets \(U \! :i ↦ φ_i(E)\) and \(K \! :i ↦ φ_i(\bar{B}_E)\).

In order to check the induction assumption from Lemma B.6, we fix some \(i\) in \(\mathcal{I}_{N}\), and some formal solution \(F\) which coincides with \(F₀\) near \(A\) and such that \(d(\operatorname{bs}F₀, \operatorname{bs}F) {\lt} τ\). We assume that \(F\) is holonomic near \(\bigcup _{j {\lt} i} K_j\). We need to build a smooth homotopy of formal solutions starting at \(F\) which coincide with \(F₀\) near \(A\), coincide with \(F\) outside \(U_i\), have base map at distance less than \(τ\) from \(\operatorname{bs}F₀\) and end at a formal solution which is holonomic near \(\bigcup _{j ≤ i} K_j\). In addition this homotopy must be time-independent for time near \((-∞, 0]\) and \([1, +∞)\).

Of course this homotopy comes from the local \(h\)-principle we proved in Lemma 2.15. The first key observation allowing to apply that lemma is that \(d(\operatorname{bs}F, \operatorname{bs}F₀) {\lt} τ ≤ ε\) hence \(\operatorname{bs}F\) sends sends \(φ_i(E)\) into \(ψ_{j(i)}(E')\).

Definition 3.18 then turns \(F\) into a section \(\mathcal{F}\) of \(J¹(E, E')\). According to Lemma 3.19, \(\mathcal{F}\) is a formal solution of the relation \(\mathcal{R}_i\) induced by \(\mathcal{R}\) in \(J¹(E, E')\) via \(φ_i\) and \(ψ_{j(i)}\), \(\mathcal{F}\) is relative to \(φ_i⁻¹(A)\) and \(\mathcal{F}\) is holonomic near \(φ_i⁻¹(A ∪ \bigcup _{j {\lt} i} φ_j(\bar B_E))\).

The homotopy \(H\) will be constructed by updating \(F\) using some homotopy \(\mathcal{H}\) of sections of \(J¹(E, E')\) with support in the closed ball \(2B_E\) and time independent for \(t\) near \((-∞, 0] ∪ [1, +∞)\) (here by support we mean the closure of the set of points where \(\mathcal{H}_t\) differs from \(\mathcal{F}\)). In order to ensure \(d(\operatorname{bs}F₀, \operatorname{bs}H_t) {\lt} τ\) for all \(t\), it suffices to ensure that, for each \(x ∈ φ_i(2\bar{B}_E)\) and \(t ∈ [0, 1]\), \(d(\operatorname{bs}H_t(x), \operatorname{bs}F(x)) {\lt} τ(x) - d(\operatorname{bs}F(x), \operatorname{bs}F₀(x))\). The latter will hold as soon as, for all \(e\) and \(t\), \(‖\operatorname{bs}\mathcal{H}_t(e) - \operatorname{bs}\mathcal{F}(e)‖ {\lt} η\) for some positive \(η\) given by Lemma 3.3 (applied to \(P = ℝ\), \(M\) and \(N\)).

There is a homotopy of immersions of \(𝕊^2\) into \(ℝ^3\) from the inclusion map to the antipodal map \(a : q ↦ -q\).

We denote by \(ι\) the inclusion of \(𝕊^2\) into \(ℝ^3\). We set \(j_t = (1-t)ι + ta\). This is a homotopy from \(ι\) to \(a\) (but not an immersion for \(t=1/2\)). Using the canonical trivialization of the tangent bundle of \(ℝ^3\), we can set, for \((q, v) ∈ T𝕊^2\), \(G_t(q, v) = \mathrm{Rot}_{Oq}^{πt}(v)\), the rotation around axis \(Oq\) with angle \(πt\). The family \(σ : t ↦ (j_t, G_t)\) is a homotopy of formal immersions relating \(j^1ι\) to \(j^1a\). It is homotopic by reparametrization to a homotopy of formal immersions relating \(j^1ι\) to \(j^1a\) which are holonomic for \(t\) near the \(0\) and \(1\).

The above theorem ensures this family is homotopic, relative to \(t = 0\) and \(t = 1\), to a family of holonomic formal immersions, ie a family \(t ↦ j^1f_t\) with \(f_0 = ι\), \(f_1 = a\), and each \(f_t\) is an immersion.