Defining a formal solution to ImmRel Whitney-Graustein

Stream: new members

[Sam Lindauer]

Hey all,

I am working on proving the whitney graustein theorem using the sphere eversion project. An important note are that I have currently axiomized anything to do with turning numbers (existence of lift, equal turning number implies homotopy between derivatives etc.), as that would become a whole side project that I do not want to get into at the moment. At this point, I have proven the mathematically 'trivial' direction, i.e. given a homotopy between loops => turning number is equal, and I am working on the inverse direction. So far, I have managed to call upon the function immersionRel_satisfiresHPrincipleWith and am working on the part where I have to construct a family of formal solutions and prove that this family is holonomic near a closed set. This is where I am tripping, as I think I know mathematically what to do, but I manage to get lost in the code of the sphere eversion project each time I am backtracking definitions.

Here is a glimpse into my setup:

import SphereEversion.Global.Immersion

open Metric FiniteDimensional Set Function LinearMap Filter ContinuousLinearMap Complex NormedSpace
open scoped Manifold Topology

variable (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [ProperSpace E] [Fact (finrank ℝ E = 2)]
local notation "𝕊¹" => sphere (0 : E) 1
local notation "𝓡_imm" => immersionRel (𝓡 1) 𝕊¹ 𝓘(ℝ, E) E

-- Structure for a loop in E that is also an immersion.
structure LoopImmersion (γ : 𝕊¹ → E) : Prop where
  -- Smooth function
  cdiff : Smooth (𝓡 1) 𝓘(ℝ, E) γ
  -- Immersion condition (≠ 0, since Dim(𝕊¹) = 1)
  imm : ∀ t : 𝕊¹, mfderiv (𝓡 1) 𝓘(ℝ, E) γ t ≠ 0

-- Structure for homotopy between loops
structure LoopHomotopy (Γ : ℝ → 𝕊¹ → E) : Prop where
  -- Smooth as function ℝ × 𝕊¹ → ℂ
  cdiff : Smooth (𝓘(ℝ, ℝ).prod (𝓡 1)) 𝓘(ℝ, E) ↿Γ
  -- LoopImmersion at every point
  imm : ∀ t : ℝ, LoopImmersion E (Γ t)

and here is a look at what I have got so far. As far as code goes, I am not yet looking at ways to simplify what I have already written, as I will probably want to also have a look at that myself more in depth later.

def family_of_formal_sol {γ₀ γ₁ : 𝕊¹ → E} (γ₀_imm : LoopImmersion E γ₀) (γ₁_imm : LoopImmersion E γ₁) (turn_eq : γ₀_imm.turningNumber = γ₁_imm.turningNumber):
  HtpyFormalSol 𝓡_imm := sorry

-- Prove that the family of formal solutions is holonomic near C := {0,1} x 𝕊¹
theorem family_of_formal_sol_hol_near_zero_one {γ₀ γ₁ : 𝕊¹ → E} (γ₀_imm : LoopImmersion E γ₀) (γ₁_imm : LoopImmersion E γ₁) (turn_eq : γ₀_imm.turningNumber = γ₁_imm.turningNumber):
    ∀ᶠ s : ℝ × 𝕊¹ near {0, 1} ×ˢ univ, (family_of_formal_sol E γ₀_imm γ₁_imm turn_eq s.1).toOneJetSec.IsHolonomicAt s.2 := by
      sorry

-- first implication whitney graustein
-- Assuming turning number is equal => ∃ homotopy
theorem whitney_graustein_left {f₀ f₁ : 𝕊¹ → E} (f₀_imm : LoopImmersion E f₀) (f₁_imm : LoopImmersion E f₁)
  (eq_turn : f₀_imm.turningNumber = f₁_imm.turningNumber) :
    ∃F : ℝ → 𝕊¹ → E, LoopHomotopy E F ∧ (F 0 = f₀) ∧ (F 1 = f₁) := by
      -- First step is to get H-principle result
      have rankE : finrank ℝ E = 2 := Fact.out
      have ineq_rank : finrank ℝ (ℝ^1) < finrank ℝ E := by simp [rankE]
      let ε : 𝕊¹ → ℝ := fun _ ↦ 1
      have hε_pos : ∀ x, 0 < ε x := fun _ ↦ zero_lt_one
      have hε_cont : Continuous ε := continuous_const
      let C := ({0, 1} : Set ℝ).prod (univ : Set 𝕊¹)
      have C_closed : IsClosed C :=
        (Finite.isClosed (by simp : ({0, 1} : Set ℝ).Finite)).prod isClosed_univ
      haveI : Nontrivial E := nontrivial_of_finrank_eq_succ (Fact.out : finrank ℝ E = 2)
      haveI : FiniteDimensional ℝ E := FiniteDimensional.of_finrank_eq_succ rankE
      haveI : Nonempty 𝕊¹ := (NormedSpace.sphere_nonempty.mpr zero_le_one).to_subtype
      haveI : IsCompact 𝕊¹ := isCompact_sphere (0 : E) 1
      haveI : SigmaCompactSpace 𝕊¹ := sigmaCompactSpace_of_locally_compact_second_countable
      let turn_hom := eq_turn_hom E f₀_imm f₁_imm eq_turn
      rcases (immersionRel_satisfiesHPrincipleWith (𝓡 1) 𝕊¹ 𝓘(ℝ, E) E 𝓘(ℝ, ℝ) ℝ
        ineq_rank C_closed hε_pos hε_cont).bs (family_of_formal_sol E f₀_imm f₁_imm eq_turn)
          (family_of_formal_sol_hol_near_zero_one E f₀_imm f₁_imm eq_turn)
            with ⟨F, h₁, h₂, h₃, h₄⟩

      -- Remains to show that F is a Loophomotopy f₀ ~ f₁
      sorry

Now, mathematically at family_of_formal_sol, I would want to have a family as follows:

$$\sigma \colon \mathbb{R} \times \mathbb{S}^1 \to J^1(\mathbb{S}^1, E),\\ \sigma_t \colon s \mapsto (s, f_t, g_t) \text{ for all } t \in \mathbb{R},\\ \sigma_0 = (0, f_0, g_0) \text{ and } \sigma_1 = (1, f_1, g_1),\\ \text{ where } f \colon \mathbb{R} \times \mathbb{S}^1 \to E \text{ is a homotopy between the immersions } f_0 \text{ and } f_1 \text{ from the theorem above } \\ \text{ and } g \colon \mathbb{R} \times \mathbb{S}^1 \to E \text{ is a homotopy of nonvanishing maps between } f_0' \text{ and } f_1'.$$

I get stuck at how to formalise these statements to a "FamilyFormalSol" or "HtpyFormalSol" that the statement

(immersionRel_satisfiesHPrincipleWith (𝓡 1) 𝕊¹ 𝓘(ℝ, E) E 𝓘(ℝ, ℝ) ℝ ineq_rank C_closed hε_pos hε_cont).bs

asks for.

It's a bit of a long one, sorry for that. Any help is sincerely appreciated,
Sam

[Johan Commelin]

@Sam Lindauer Is the code available at some project? Then we can open a local copy, which will probably make it easier to help you out.

[Sam Lindauer]

Yes, it should be reachable using the following link: https://github.com/MetalCreator666/WhitneyGraustein