Zulip Chat Archive

Stream: maths

Topic: help with mfderiv


view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 03:55):

I'm having a lot of difficulty working with the tangent bundle construction -- in particular with mfderiv. The goal is simple, but I couldn't find an results on mfderiv I could apply to this goal.
Here's a mwe:

import geometry.manifold.basic_smooth_bundle
import geometry.manifold.mfderiv

noncomputable theory

section tangent

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E  : Type*} [normed_group E]  [normed_space 𝕜 E]
{H  : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
(M : Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]


def tangent_bundle.pure : M  tangent_bundle I M  :=
λ x, x,0


lemma tangent_map_tangent_bundle_pure :
   x v,
  tangent_map I I.tangent (tangent_bundle.pure I M) x,v = ⟨⟨x,0⟩,⟨v,0⟩⟩ :=
begin
  intros x v,
  simp [tangent_bundle.pure,tangent_map],
  dsimp,
  sorry,
end

end tangent

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 03:56):

Does anyone have any pointers?

view this post on Zulip Sebastien Gouezel (Sep 26 2020 at 07:41):

You won't have pointers for this one, because it has not been considered yet, and because it's not completely math-obvious (I mean, statements involving the tangent bundle to the tangent bundle always need thinking twice). Let me have a look.

view this post on Zulip Sebastien Gouezel (Sep 26 2020 at 09:11):

In fact, this question is very much math-subtle: for p=(x,v)TMp = (x,v) \in TM, you are writing a vector WW in Tp(TM)T_p (TM) as a pair (w,w)(w, w') where ww and ww' are vectors in TxMT_x M, so you are using an identification of Tp(TM)T_p(TM) with TxM×TxMT_x M \times T_x M. In general, there is no such canonical identification, so saying that WW is (w,w)(w, w') does not really make sense (although by the irrelevant details of the construction, WW is a member of some version of E×EE \times E, so Lean understands the question). The reason is that you have a canonical subspace of Tp(TM)T_p(TM), the kernel of the derivative of the projection from TMTM to MM, but you don't have a canonical complementary subspace (such a complementary subspace is usually called a horizontal subspace, and requires the choice of a connection).

There is one place where there is a canonical decomposition, though: at the zero section, you have a canonical horizontal space, which is the tangent space to the zero section, so you have a canonical decomposition of T(x,0)MT_{(x,0)}M as TxMkerT(x,0)πT_x M \oplus ker T_{(x,0)}\pi. That's why your question can make sense. However, it is not at all obvious that the Lean implementation really respects this canonical decomposition (and if it does it is more a coincidence that a deliberate design choice).

So, I have a question: are you sure this is a statement you want to prove and to use?

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 13:16):

@Sebastien Gouezel , I was trying to access the local coordinates on TTMTTM induced by MM.
The term tangent_bundle.pure is the zero section which is the "return" natural transformation of the monad structure of TT. In any case, here is my attempt so far:

import geometry.manifold.basic_smooth_bundle
import geometry.manifold.mfderiv

noncomputable theory

universes u v w


section tangent_bundle_monad

variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E E' : Type*} [normed_group E] [normed_group E'] [normed_space 𝕜 E] [normed_space 𝕜 E']
{H H' : Type*} [topological_space H] [topological_space H'] (I : model_with_corners 𝕜 E H)
(I' : model_with_corners 𝕜 E' H')
(M M': Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M][topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']

/-- The zero section is the `pure` of the tangent bundle monad. -/
def tangent_bundle.pure : M  tangent_bundle I M  :=
λ x, x,0

lemma tangent_map_tangent_bundle_pure :
   x v,
  tangent_map I I.tangent (tangent_bundle.pure I M) x,v = ⟨⟨x,0⟩,⟨v,0⟩⟩ :=
begin
  intros x v,
  simp [tangent_bundle.pure,tangent_map],
  dsimp,
  sorry,
end

/-- The zero section is a retraction of the projection. -/
@[simp] lemma pure_section :
 x, (tangent_bundle.proj I M) (tangent_bundle.pure I M x) = x := λ _, rfl

/-- The `join` operation of the tangent bundle monad.
    ⟨x,x',v,v'⟩ ↦ ⟨x,x'⟩ and ⟨x,x',v,v'⟩ ↦ ⟨x,v⟩ satisfies one of the two unit laws. Their sum satisfies both.  -/
def tangent_bundle.join :
 tangent_bundle I.tangent (tangent_bundle I M)  tangent_bundle I M :=
λ ⟨⟨x, x'⟩, v, v'⟩, x, (v + x')⟩


def tangent_bundle.bind :
tangent_bundle I M  (M  tangent_bundle I' M')  tangent_bundle I' M' :=
λ m f, tangent_bundle.join I' M' (tangent_map I I'.tangent f m)

lemma tangent_bundle.join_pure_1 :
 x',
tangent_bundle.join I M (tangent_bundle.pure I.tangent (tangent_bundle I M) x') = x' :=
begin
  rintros x,v⟩,
  unfold tangent_bundle.pure,
  have : (0 : tangent_space I.tangent (sigma.mk x v)) = 0,0⟩, by refl,
  rw this,
  simp [tangent_bundle.join],
end

lemma tangent_bundle.join_pure_2 :
 x' : tangent_bundle I M,
tangent_bundle.join I M (tangent_map _ _ (tangent_bundle.pure I M) x') = x' :=
begin
  rintros x,v⟩,
  rw tangent_map_tangent_bundle_pure,
  dsimp [tangent_bundle.join],
  simp,
end

end tangent_bundle_monad

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 13:19):

I was able to prove one monad law, the second one tangent_bundle.join_pure_2 needs me to compute the action of the tangent functor on the zero section, which is what I tried to prove in the mwe above.

view this post on Zulip Sebastien Gouezel (Sep 26 2020 at 14:56):

You say "access the local coordinates on TTMTTM induced by MM", but the difficulty is that there are several such coordinates. So, a good definition should be independent of the choice of such coordinates. For instance, your definition

/-- The `join` operation of the tangent bundle monad.
    ⟨x,x',v,v'⟩ ↦ ⟨x,x'⟩ and ⟨x,x',v,v'⟩ ↦ ⟨x,v⟩ satisfies one of the two unit laws. Their sum satisfies both.  -/
def tangent_bundle.join :
 tangent_bundle I.tangent (tangent_bundle I M)  tangent_bundle I M :=
λ ⟨⟨x, x'⟩, v, v'⟩, x, (v + x')⟩

is not obviously coordinate-independent. A very good practice in differential geometry is to try to recast things in canonical terms (just using the projection from the tangent bundle to the manifold, and its derivative). Here, you have a point pp in the tangent bundle (that you denote with (x,x)(x, x') -- this is a little bit misleading as xx' is a tangent vector), and then you have a tangent vector to this point, that you denote with (v,v)(v, v') but here you are abusing coordinates. Instead, let's just denote it with WW. Then, you have the map proj:TMMproj : TM \to M. You can consider its differential at pp, which is a map Tpproj:Tp(TM)TxMT_p proj : T_p (TM) \to T_x M. You can take the image of WW under this map, and you get canonically a well defined vector in TxMT_x M. If I understand correctly, your map is therefore (p,W)(x,(v+Tpproj(W)))(p, W) \mapsto (x, (v + T_p proj (W))) where p=(x,v)p = (x, v). If you try to work with this expression, things should go much more smoothly.

view this post on Zulip Sebastien Gouezel (Sep 26 2020 at 15:29):

Still, your formula is true, by the way!

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 15:33):

Actually yes, according to your suggested refactor, I now have:

def tangent_bundle.join :
 tangent_bundle I.tangent (tangent_bundle I M)  tangent_bundle I M :=
λ ⟨⟨x, v⟩, W⟩, x, v + (mfderiv I.tangent I (tangent_bundle.proj I M) x,v W)⟩

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 15:34):

And it made the proof of the first unit law simpler, indeed.

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 15:34):

I'm still stuck on the second one but.

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 15:35):

Sebastien Gouezel said:

Still, your formula is true, by the way!

do you mean this?

lemma tangent_map_tangent_bundle_pure :
   x v,
  tangent_map I I.tangent (tangent_bundle.pure I M) x,v = ⟨⟨x,0⟩,⟨v,0⟩⟩ :=

view this post on Zulip Sebastien Gouezel (Sep 26 2020 at 15:39):

Yes

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 15:40):

Is the proof simple?

view this post on Zulip Sebastien Gouezel (Sep 26 2020 at 15:41):

No, one really needs to unfold everything, so it is rather painful.

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 15:41):

That's what I couldn't get through. :(

view this post on Zulip Sebastien Gouezel (Sep 26 2020 at 15:43):

Also, in definitions, you shouldn't use bracket notation because it makes a (hidden) mess behind the scene. Instead of ⟨⟨x, v⟩, W⟩, call it p, and refer to the different fields as p.1.1 and p.1.2 and p.2 in the definition.

view this post on Zulip Koundinya Vajjha (Sep 26 2020 at 15:44):

Isn't the maths proof simply "observe that the map λ (x : M), ⟨x, 0⟩ is linear, and so it's mfderiv is actually itself" or am I missing something?

view this post on Zulip Sebastien Gouezel (Sep 26 2020 at 15:45):

It's not linear because there is no linear structure on the basis. And indeed the formula is not true in general, it really depends on the choice of a coordinate system. It turns out that, with the one we use in Lean, the formula is true.

view this post on Zulip Sebastien Gouezel (Sep 27 2020 at 20:39):

Proof done in #4292

view this post on Zulip Koundinya Vajjha (Sep 28 2020 at 01:13):

Great! Thanks for your quick response!


Last updated: May 14 2021 at 17:42 UTC