Unit vector in tangentspace

Stream: new members

[Sam Lindauer]

Hey all, I am currently working on writing a lemma that tells us that a smooth loop that is an immersion has (with abuse of notation) a smooth derivative that is a smooth loop around zero. To do this, I think I need to use some sort of standard unit vector in the tangent space to help define this smooth loop

$$\gamma \colon \mathbb{S}^1 \to \mathbb{R}^2 \text{ smooth immersion loop, then } \\ t \in \mathbb{S}^1 \mapsto D\gamma(t)(e) \in \mathbb{R}^2-\{0\} \text{ smooth loop around zero}$$

In lean I use the following setup and have tried to make a start at defining this lemma, but I am not completely sure how to finish it (the dots indicate the space where I would want to essentially write 1 or e):

import Mathlib

open scoped Manifold

notation "ℝ²" => EuclideanSpace ℝ (Fin 2)
notation "𝕊¹" => Metric.sphere (0 : ℝ²) 1

-- Smooth loop around zero
structure MLoop (γ : 𝕊¹ → ℝ²) : Prop where
  smooth : Smooth (𝓡 1) 𝓘(ℝ, ℝ²) γ
  around_zero : ∀x : 𝕊¹, γ x ≠ 0

-- Immersion loop
structure ILoop (γ : 𝕊¹ → ℝ²) : Prop where
  smooth : Smooth (𝓡 1) 𝓘(ℝ, ℝ²) γ
  -- Injectivity of derivative in this case (dim(𝕊¹) = 1)
  imm :  ∀ t : 𝕊¹, mfderiv (𝓡 1) 𝓘(ℝ, ℝ²) γ t ≠ 0

-- Now, one can take the function `t ↦ Dγ(t)(e)`
-- where `e is the standard unit vector` to get a `MLoop 𝕊¹ → ℝ²`

lemma deriv_iloop_eq_mloop {γ : 𝕊¹ → ℝ²} (γ_iloop : ILoop γ) :
  MLoop (fun t : 𝕊¹ ↦ (mfderiv (𝓡 1) 𝓘(ℝ, ℝ²) γ t ...)) := by sorry

Thanks in advance! Sam

[Johan Commelin]

I think you can drop the SphereEversion import, right?

[Johan Commelin]

And really your goal is how to fill in the following sorry, if I understand you correctly:

def e {t : 𝕊¹} : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) t := sorry

[Sam Lindauer]

Johan Commelin said:

I think you can drop the SphereEversion import, right?

oh yeah that's totally right :+1:

[Sam Lindauer]

Johan Commelin said:

And really your goal is how to fill in the following sorry, if I understand you correctly:

def e {t : 𝕊¹} : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) t := sorry

Essentially yes. Thinking about it now, it might be better to be able to define it as a smooth 'unit' section of the tangent bundle above the circle, because in that way smoothness of the resulting loop is easier to show I would guess. Otherwise, I think one needs to really dig in to taking this unit vector in charts and patching it up.

[Johan Commelin]

@Sam Lindauer The following works.

def e {t : 𝕊¹} : TangentSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1)) t := fun _ ↦ 1

Explanation: the tangent space is not defeq to $\R$ itself, but to $\R^1$ aka Fin 1 → ℝ

[Johan Commelin]

Do you think you can fill in the proof obligations?

[Sam Lindauer]

Thanks! There is several proof obligations left and I am not entirely sure how to do some of them, but I will give it a solid try first.