Rotation around a vector by an angle

Stream: sphere eversion

[Heather Macbeth]

@Patrick Massot I was able to construct the rotation around a vector by an angle as an element of $O(3)$, in the following form (using the constructions unit_quaternions and unit_quaternions.to_matrix_hom from my polyrith tutorial):

local notation `ℛ²` := euclidean_space ℝ (fin 2)
local notation `ℛ³` := euclidean_space ℝ (fin 3)

local notation `𝕊¹` := metric.sphere (0 : ℛ²) 1
local notation `𝕊²` := metric.sphere (0 : ℛ³) 1

def rotate_around (x : 𝕊²) (y : 𝕊¹) : unit_quaternions :=
⟨ (y : ℛ²) 0 + (y : ℛ²) 1 • (quaternion_algebra.mk 0 ((x : ℛ³) 0) ((x : ℛ³) 1) ((x : ℛ³) 2)), sorry ⟩

local notation `↑ₘ` := @coe (matrix.orthogonal_group (fin 3) ℝ) (matrix (fin 3) (fin 3) ℝ) _

example (x : 𝕊²) (y : 𝕊¹) :
  matrix.mul_vec (↑ₘ(unit_quaternions.to_matrix_hom (rotate_around x y))) (x : ℛ³) = (x : ℛ³) :=
sorry

I can go up or down in level of generality, let me know -- just wanted to run the first version past you.

[Heather Macbeth]

@Patrick Massot I have a co-ordinate-free version now, but I didn't try to Lean it yet :). Let $V$ be a three-dimensional oriented inner product space, with the inner product denoted $\langle \cdot,\cdot\rangle$ and the volume form denoted $\Omega$.

We have the Hodge isomorphism between $V$ and $\Lambda^2(V^*)$, and the further isomorphism between $\Lambda^2(V^*)$ and
$\mathfrak{so}(V)=\{A\in\operatorname{End}(V) : A^t+A=0\}.$

The composition of these two isomorphisms can be written explicitly as sending $v\in V$ to the element $A_v\in\operatorname{End}(V)$ defined as follows: for $w\in V$, $A_v(w)$ is the unique element of $V$ such that for all $u\in V$,
$\langle A_v(w),u\rangle=\Omega(v,w,u).$
One needs to check that in fact $A_v^t+A_v=0$, so that $A_v\in\mathfrak{so}(V)$.

Now denote by $S^2(v)$ the 2-sphere in $V$, and define a map from $S^2(V)\times \mathbb{R}$ to $SO(V)$ by the endomorphism exponential
$(v,t)\mapsto \exp(tA_v).$
It can be checked that this is $2\pi$-periodic, so descends to a map
$S^2(V)\times S^1 \to SO(V).$

[Patrick Massot]

Thanks Heather! I answer late because I took a break after coming back from Providence. Of course the coordinate-free version looks nice but, as I told you in Providence, the test case for us is to make you can easily prove that the map sending $(v, t, w)$ to $\exp(tA_v)w$ is smooth.

[Patrick Massot]

Note that I don't really need that the version where $t$ is in $\mathbb{S}^1$$ is smooth. Our $t$ will naturally be a real number.

[Heather Macbeth]

Patrick Massot said:

Of course the coordinate-free version looks nice but, as I told you in Providence, the test case for us is to make you can easily prove that the map sending $(v, t, w)$ to $\exp(tA_v)w$ is smooth.

OK, this sounds like a challenge :). For the quaternion version the smoothness looks pretty doable, for the co-ordinate-free version the hard part (modulo current mathlib) seems to be the smoothness of the endomorphism exponential.

Do you have written down somewhere the other properties you need it confirmed to satisfy? E.g. I imagine you need that $t=0$ gives the identity and that for all $v$ it fixes $v$? What else?

[Heather Macbeth]

Heather Macbeth said:

for the co-ordinate-free version the hard part (modulo current mathlib) seems to be the smoothness of the endomorphism exponential.

I think there's also a bit of a trick available, some formula like
$\exp(tA_v)=\operatorname{Proj}_v+\cos(t)\operatorname{Proj}_{v^\perp}+\sin(t)A_v$
should hold and it is likely easier to prove smoothness in this representation.

[Patrick Massot]

I also need that for $t=\pi$ you get -id on $v^\perp$.

[Patrick Massot]

I also found https://en.m.wikipedia.org/wiki/Euler%E2%80%93Rodrigues_formula which a more elementary version of the quaternion story.

[Joseph Myers]

In oriented two dimensions we already have docs#orientation.rotation - my inclination for how to go from two dimensions to higher (not just three) dimensions (with only the two-dimensional subspace needing to have an orientation specified) would be to define the operation that goes from a linear_isometry_equiv of a subspace of an inner product space to a subspace of a possibly different inner product space, and another linear_isometry_equiv of their orthogonal complements, to a linear_isometry_equiv of the whole space (and then apply that operation with one isometry being two-dimensional rotation and the other being the identity to produce a higher-dimensional rotation). I don't know how readily that would give whatever smoothness properties you need, but we do have docs#orientation.rotation_pi saying what rotation by pi does.

[Heather Macbeth]

@Patrick Massot I pushed the construction, the smoothness, and the three facts you identified.

(For the smoothness, so far I proved smoothness of the operation considered as of type

(E × ℝ) → (E →L[ℝ] E)

But it should be a one-liner to deduce the smoothness of the version

(E × ℝ × E) → E

if that's what you need.)

[Heather Macbeth]

But I'm a bit suspicious. So far I barely used anything -- I didn't even need that the space was three-dimensional, or that the "orientation" three-form was nonzero (let alone compatible with the metric). Maybe there are other properties you need which will require these facts?

[Patrick Massot]

Nice! The real test is to build the homotopy of formal immersion defined in the last proof of the blueprint.

[Heather Macbeth]

@Patrick Massot I've been looking at this. It seems to me that to make the homotopy of formal immersions, I need three ingredients:

1. for the unit sphere $S(E)$ in $E$, there is a canonical smooth section of the bundle whose fibre over $x$ is $\operatorname{Hom}(T_xS(E), E)$, which comes from thinking of the tangent spaces of the embedding as living in $E$
2. The discussion about rotations gives a smooth map from $S(E)\times \mathbb{R}$ to $\operatorname{Hom}(E, E)$
3. for a manifold $M$ and normed spaces $E$, $F$, and a smooth section of the bundle whose fibre over $x$ is $\operatorname{Hom}(T_xM, E)$, and a smooth map from $M\times\mathbb{R}$ to $\operatorname{Hom}(E, F)$, these can be composed to give a homotopy of 1-jet sections from $M$ to $F$.

Sound right? I have started thinking about building (1), so far just have the statement,

def hyperplane_map (v : sphere (0:E) 1) :
  ((tangent_bundle_core (𝓡 n) (sphere (0:E) 1)).hom
    (trivial_basic_smooth_vector_bundle_core (𝓡 n)
      (sphere (0:E) 1) E)).to_topological_vector_bundle_core.total_space :=
⟨v, (submodule.subtypeL _) ∘L
    ((orthonormal_basis.from_orthogonal_span_singleton n
    (ne_zero_of_mem_unit_sphere (-v))).repr.symm.to_continuous_linear_equiv
      : euclidean_space ℝ (fin n) →L[ℝ] (ℝ ∙ (↑(-v):E))ᗮ)⟩

example : smooth (𝓡 n) ((𝓡 n).prod 𝓘(ℝ, euclidean_space ℝ (fin n) →L[ℝ] E)) (hyperplane_map E n) :=
sorry

[Heather Macbeth]

Note: This is just to build it as a homotopy of 1-jet sections, not yet to make it a homotopy of formal immersions.

[Patrick Massot]

For 1, we are indeed punished for not having submanifolds in mathlib. However I think of this map as the derivative $T_v\iota : T_vS(E) \to T_{\iota(v)}E$ of the inclusion map $\iota$ composed with the canonical identification of $T_eE$ with $E$ for all $e$. There shouldn't be anything specific to spheres. Also I don't understand why -v enters your code here.

[Patrick Massot]

@Heather Macbeth do you have any update here?

[Heather Macbeth]

Hi, @Patrick Massot and all. After the helpful message of Patrick, I hit decision paralysis a few weeks ago when looking a little more closely at @Floris van Doorn's work on constructing the pullback as a smooth bundle in certain situations (when the charts line up properly).

I agree with Patrick's suggested approach here :light_bulb:
Patrick Massot said:

However I think of this map as the derivative $T_v\iota : T_vS(E) \to T_{\iota(v)}E$ of the inclusion map $\iota$ composed with the canonical identification of $T_eE$ with $E$ for all $e$.

but does that mean I should explicitly construct another special-case instance of the pullback, analogous to the ones for prod_fst and prod_snd, with my instance being (say) the one where the target of the map has a single chart? Or is there maybe a way of avoiding such a construction and instead re-using the prod_fst/prod_snd ones, by some other clever exploitation of the "product trick"?

Anyway, sorry it took so long for me to summarize my thoughts here; looking forward to hearing others' thoughts.

[Heather Macbeth]

Patrick Massot said:

Also I don't understand why -v enters your code here.

By the way, this was a consequence of working too specifically with the charts of the sphere, rather than charts of a general source manifold. The charts of the sphere are stereographic projections centred around the antipodes of the base point.

[Patrick Massot]

I don't know what is the best construction from a library building point of view, but I would welcome any hack that can get us this map as soon as possible.

[Floris van Doorn]

I tried to read up on what you're trying to do here, so I might be misunderstanding.
I'm not sure why you would need to construct another pullback of smooth vector bundles. For $T_v\iota$ you can write mfderiv _ _ subtype.val, and the corresponding section is just one_jet_ext or one_jet_ext_sec applied to subtype.val, or am I misunderstanding what you're trying to do?

[Heather Macbeth]

@Floris van Doorn Thanks for the quick reply, I tried to write out what I wanted more explicitly, see this branch:
https://github.com/leanprover-community/sphere-eversion/tree/naive-homotopy
Effectively, for maps with target in a normed space V, I am writing glue between your point of view (one-jet sections considered as sections of the product manifold etc. etc.) and an alternative point of view (sections of the smooth vector bundle of endomorphisms from the tangent space to V).

Are the three sorries in global/twist_one_jet_sec things you've thought about/already proved somewhere? Effectively these are stating the fact "tangent bundle of V is canonically trivialized" in convenient ways.

[Heather Macbeth]

note: everything is type-correct, but because of the exploitation of defeq for fibres of bundles throughout the manifolds library, I'm only about 75% sure that I have written what I mean ...

[Sebastien Gouezel]

Heather Macbeth said:

note: everything is type-correct, but because of the exploitation of defeq for fibres of bundles throughout the manifolds library, I'm only about 75% sure that I have written what I mean ...

That's a very interesting point! The library was written to avoid dependent type hell as much as possible, and now it's backfiring :-)

[Floris van Doorn]

Thanks Heather. These sorry's are not something I have proven, but they should be easily provable from tools I wrote for the 1-jet bundles. For 1-jet bundles I proved smooth_at_one_jet_bundle, which precisely characterizes the smooth functions into a 1-jet bundle (in_coordinates is an appropriate pre- and post-composition with coordinate changes)

[Floris van Doorn]

If you want, I can work on these tools and prove these sorry's. I think it will not be too hard.

[Floris van Doorn]

Heather Macbeth said:

note: everything is type-correct, but because of the exploitation of defeq for fibres of bundles throughout the manifolds library, I'm only about 75% sure that I have written what I mean ...

This is very normal. I've written a couple of lemma statements that I had to modify during the proof, and even the original definition of 1-jet bundle that Patrick wrote down was wrong (it missed a coordinate change function).

I don't think the solution is to make it harder to write down these non-sensical things, since I'm greatly enjoying the freedom that tangent spaces are definitionally equal to the underlying vector space. It allowsme to write down lemmas like this: mfderiv (I.prod I') I prod.fst x = continuous_linear_map.fst 𝕜 E E'. Sometimes Lean is still confused because it thinks tangent_space is a dependent type, and refused to rewrite subexpressions, which is all very frustrating.
I think your family_twist might be missing a coordinate change function in the condition i_smooth. I'm not sure, since the codomain has trivial coordinate changes, but the domain doesn't...

[Floris van Doorn]

You had the correct formulation of family_twist (there was a coordinate change that showed up in the proof, but that was exactly the coordinate change needed to use the fact that s is smooth).

[Floris van Doorn]

I proved all three sorry's. The file twist_one_jet_sec is now sorry-free.

[Floris van Doorn]

I pushed your and my commits to master.

[Patrick Massot]

What is the current status of the formal sphere eversion then?

[Patrick Massot]

It seems that right now it is holonomic only at time 0 and 1, which isn't quite enough, but this can easily (on paper) be arranged after the fact, simply precomposing it by a time cutoff function).

[Patrick Massot]

I mean we need to prove this lemma which doesn't seem to hold with the current definition.

[Floris van Doorn]

I hope that Heather can do the remaining part.
From looking over the file, it seems like we still need to
(1) add a cut-off-function, and prove that this is still smooth
(2) prove that rotations are immersions - and I guess that the cut-off function is also an immersion, which probably needs that the derivatives of a rotation at $v$ is orthogonal to $v$
(3) prove that the base map is smooth (which is easy)

[Patrick Massot]

What do you mean by "the cut-off function is also an immersion"?

[Patrick Massot]

Maybe I should clarify that cut-off thing.

[Floris van Doorn]

Oh, sorry, I meant "the cut-off function is also injective"

[Patrick Massot]

A formal eversion is $F : \R \times \mathbb{S}^2 \to J^1(\mathbb{S}^2, \R^3)$ where $F_t(x) = (x, f_t(x), \varphi_t(x))$ with each $\varphi_t(x) : T_x\mathbb{S}^2 \to T_{f_t(x)}\R^3$ is an injective linear map, for all $x$ $f_0(x) = x$ and $f_1(x) = -x$ and $\varphi_t(x) = T_xf_t$ when $t$ is zero or one. This is what we can do with a nice explicit formula involving rotations. But we want to ensure a slightly stronger last condition, going from "when $t$ is zero or one" to "when $t$ is close to zero or one". Given a formal sphere eversion $F$ we can get the stronger version by setting $F'(t, x) = F(\rho(t), x)$ where $\rho : \R \to \R$ is a smooth non-decreasing function which equals zero on a neighborhood of zero and one on a neighborhood of one.

[Floris van Doorn]

Ah, I see. That makes that part immediate, indeed.

[Patrick Massot]

This $\rho$ is what I call the cutoff function.

[Patrick Massot]

There is no injectivity condition on $\rho$

[Floris van Doorn]

I indeed had a different construction in mind (a smooth transition between $T_xf_t$ and rotations). Sorry for the confusion.

[Heather Macbeth]

@Floris van Doorn Awesome! Thanks! And I am gratified to hear that I stated the sorries right :)

I'll take a stab now at proving it's a formal immersion. Moment of truth ...

[Heather Macbeth]

OK, done! I proved that the construction:

• gives a formal immersion at each $t\in\mathbb{R}$
• is holonomic at 0 and 1

[Heather Macbeth]

This is modulo some theory which ought to be in mathlib, which I've sorried for now:

1. the tangent space of the sphere considered in the ambient space
2. interaction of orientations and inner products
3. finrank lemmas

[Heather Macbeth]

I also didn't implement the "fiddle with the endpoints" argument.

[Heather Macbeth]

Heather Macbeth said:

This is modulo some theory which ought to be in mathlib, which I've sorried for now:

1. the tangent space of the sphere considered in the ambient space
2. interaction of orientations and inner products
3. finrank lemmas

Just pushed (1). This also gives as a corollary that the identity and antipodal embeddings of the sphere are immersions.

[Heather Macbeth]

Heather Macbeth said:

This is modulo some theory which ought to be in mathlib, which I've sorried for now:

1. the tangent space of the sphere considered in the ambient space
2. interaction of orientations and inner products
3. finrank lemmas

(2) is now done.

I've also extracted explicitly what was previously implicit, that I have built a basis-free construction of the cross product for an oriented real inner product space. (The rotation by angle $t$ about a vector $v$ is realized as the endomorphism exponential of the endomorphism $tv\times \cdot$.). We should figure out whether this should supersede or coexist with the co-ordinate cross product constructed in
https://leanprover-community.github.io/mathlib_docs/linear_algebra/cross_product.html

[Patrick Massot]

Great, thanks!

[Yaël Dillies]

Just wondering, did you construct the cross product the same way we define the dimension (namely, use trunc on bases)?

[Heather Macbeth]

I don't know what trunc is.

[Heather Macbeth]

I wrote a canonical definition of the cross-product: let $\omega$ be the unique "volume" 3-form compatible with the orientation and inner product; then we define $\times$ so that for all $u$, $v$, $w$ we have $\langle u \times v, w\rangle = \omega(u,v,w)$.

[Kevin Buzzard]

trunc is a way of saying "we define this by making an arbitrary choice (eg picking a basis and counting it) and then proving the answer is independent of the choice", without actually applying the axiom of choice to pick a basis. It's the quotient of a type by the "always true" equivalence relation, so assuming the original type is nonempty it's got one element, and you can define maps from it to other types (like nat) using quotient.lift. So I think Yael's question mathematically is "did you pick a basis and if so then how exactly?" and your answer is "I didn't need to pick a basis at all!"

[Heather Macbeth]

Heather Macbeth said:

This is modulo some theory which ought to be in mathlib, which I've sorried for now:

1. the tangent space of the sphere considered in the ambient space
2. interaction of orientations and inner products
3. finrank lemmas

The homotopy of formal immersions and its to_mathlib prerequisites are now finished. I found some lemmas to replace (3) in mathlib already.

[Patrick Massot]

Thank you very much for all this rotation work Heather!

[Heather Macbeth]

I opened #16466, #16474, #16475, #16476, #16477, #16478, #16479; more to come!

[Patrick Massot]

It's great to also take the trouble to immediately open mathlib PRs