This is file proves the existence of a sphere eversion from the local verson of the h-principle.

We define the relation of immersions R = immersion_sphere_rel ⊆ J¹(E, F) which consist of all (x, y, ϕ) such that if x is outside a ball around the origin with chosen radius R < 1 then ϕ must be injective on (ℝ ∙ x)ᗮ (the orthogonal complement of the span of x). We show that R is open and ample.

Furthermore, we define a formal solution of sphere eversion that is holonomic near 0 and 1. We have to be careful since we're not actually working on the sphere, but in the ambient space E ≃ ℝ³. See loc_formal_eversion for the choice and constaints of the solution.

Finally, we obtain the existence of sphere eversion from the parametric local h-principle, proven in Local/ParametricHPrinciple.

def SphereImmersion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : E → F) : Prop

A map between vector spaces is a immersion viewed as a map on the sphere, when its derivative at x ∈ 𝕊² is injective on the orthogonal complement of x (the tangent space to the sphere). Note that this implies f is differentiable at every point x ∈ 𝕊² since otherwise D f x = 0.

Equations

• SphereImmersion f = ∀ x ∈ Metric.sphere 0 1, Set.InjOn ⇑(D f x) ↑(Submodule.span ℝ {x})ᗮ

def immersionSphereRel (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F : Type u_2) [NormedAddCommGroup F] [InnerProductSpace ℝ F] : RelLoc E F

The relation of immersionsof a two-sphere into its ambient Euclidean space.

Equations

• immersionSphereRel E F = {w : OneJet E F | w.1 ∉ Metric.ball 0 0.9 → Set.InjOn ⇑w.2.2 ↑(Submodule.span ℝ {w.1})ᗮ}

@[simp]

theorem mem_loc_immersion_rel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : E} {y : F} {φ : E →L[ℝ] F} : (x, y, φ) ∈ immersionSphereRel E F ↔ x ∉ Metric.ball 0 0.9 → Set.InjOn ⇑φ ↑(Submodule.span ℝ {x})ᗮ

theorem sphereImmersion_of_sol {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : E → F) : (∀ x ∈ Metric.sphere 0 1, (x, f x, D f x) ∈ immersionSphereRel E F) → SphereImmersion f

theorem mem_slice_iff_of_not_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : E} {w : F} {φ : E →L[ℝ] F} {p : DualPair E} (hx : x ∉ Metric.ball 0 0.9) (y : F) : w ∈ (immersionSphereRel E F).slice p (x, y, φ) ↔ Set.InjOn ⇑(p.update φ w) ↑(Submodule.span ℝ {x})ᗮ

theorem loc_immersion_rel_open_aux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ E] {x₀ : E} {y₀ : F} {φ₀ : E →L[ℝ] F} (hx₀ : x₀ ∉ Metric.ball 0 0.9) (H : Set.InjOn ⇑φ₀ ↑(Submodule.span ℝ {x₀})ᗮ) : ∀ᶠ (p : OneJet E F) in nhds (x₀, y₀, φ₀), inner x₀ p.1 ≠ 0 ∧ Function.Injective ⇑((p.2.2.comp ((Submodule.span ℝ {p.1})ᗮ.subtypeL.comp (projSpanOrthogonal p.1))).comp (Submodule.span ℝ {x₀})ᗮ.subtypeL)

theorem loc_immersion_rel_open {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ E] : IsOpen (immersionSphereRel E F)

theorem loc_immersion_rel_ample {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (n : ℕ) [Fact (Module.finrank ℝ E = n + 1)] (h : Module.finrank ℝ E ≤ Module.finrank ℝ F) : (immersionSphereRel E F).IsAmple

def locFormalEversionAuxφ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) (x : E) : E →L[ℝ] E

The main ingredient of the linear map in the formal eversion of the sphere.

Equations

• locFormalEversionAuxφ ω t x = ω.rot (t, x) - (2 * t) • (Submodule.span ℝ {x}).subtypeL.comp (orthogonalProjection (Submodule.span ℝ {x}))

theorem smooth_at_locFormalEversionAuxφ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) {p : ℝ × E} (hx : p.2 ≠ 0) {n : WithTop ℕ∞} : ContDiffAt ℝ n (Function.uncurry (locFormalEversionAuxφ ω)) p

def locFormalEversionAux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) : HtpyJetSec E E

A formal eversion of 𝕊², viewed as a homotopy.

Equations

• One or more equations did not get rendered due to their size.

def locFormalEversion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) : (immersionSphereRel E E).HtpyFormalSol

A formal eversion of 𝕊² into its ambient Euclidean space. The corresponding map E → E is roughly a linear homotopy from id at t = 0 to - id at t = 1. The continuous linear maps are roughly rotations with angle t * π. However, we have to keep track of a few complications:

• We need the formal solution to be holonomic near 0 and 1. Therefore, we compose the above maps with a smooth step function that is constant 0 near t = 0 and constant 1 near t = 1.
• We need to modify the derivative of ω.rot to also have the right behavior on (ℝ ∙ x) at t = 1 (it is the identity, but it should be -id). Therefore, we subtract (2 * t) • (submodule.subtypeL (ℝ ∙ x) ∘L orthogonal_projection (ℝ ∙ x)), which is 2t times the identity on (ℝ ∙ x).
• We have to make sure the family of continuous linear map is smooth at x = 0. Therefore, we multiply the family with a factor of smooth_step (‖x‖ ^ 2).

Equations

• locFormalEversion ω = { toFamilyJetSec := locFormalEversionAux ω, is_sol := ⋯ }

@[simp]

theorem locFormalEversion_f {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) : ((locFormalEversion ω) t).f = fun (x : E) => (1 - 2 * smoothStep t) • x

theorem locFormalEversion_φ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) (t : ℝ) (x v : E) : (((locFormalEversion ω) t).φ x) v = smoothStep (‖x‖ ^ 2) • ((ω.rot (smoothStep t, x)) v - (2 * smoothStep t) • ↑((orthogonalProjection (Submodule.span ℝ {x})) v))

theorem locFormalEversion_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) (x : E) : ((locFormalEversion ω) 0).f x = x

theorem locFormalEversion_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) (x : E) : ((locFormalEversion ω) 1).f x = -x

theorem locFormalEversionHolAtZero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) {t : ℝ} (ht : t < 1 / 4) {x : E} (hx : smoothStep (‖x‖ ^ 2) = 1) : ((locFormalEversion ω) t).IsHolonomicAt x

theorem locFormalEversionHolAtOne {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) {t : ℝ} (ht : 3 / 4 < t) {x : E} (hx : smoothStep (‖x‖ ^ 2) = 1) : ((locFormalEversion ω) t).IsHolonomicAt x

theorem locFormalEversion_hol {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] [FiniteDimensional ℝ E] (ω : Orientation ℝ E (Fin 3)) : ∀ᶠ (p : ℝ × E) in nhdsSet ({0, 1} ×ˢ Metric.sphere 0 1), ((locFormalEversion ω) p.1).IsHolonomicAt p.2

theorem sphere_eversion_of_loc {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (Module.finrank ℝ E = 3)] : ∃ (f : ℝ → E → E), 𝒞 ↑⊤ ↿f ∧ (∀ x ∈ Metric.sphere 0 1, f 0 x = x) ∧ (∀ x ∈ Metric.sphere 0 1, f 1 x = -x) ∧ ∀ t ∈ unitInterval, SphereImmersion (f t)