help with mfderiv

Stream: maths

[Koundinya Vajjha]

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

[Koundinya Vajjha]

Does anyone have any pointers?

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

In fact, this question is very much math-subtle: for $p = (x,v) \in TM$, you are writing a vector $W$ in $T_p (TM)$ as a pair $(w, w')$ where $w$ and $w'$ are vectors in $T_x M$, so you are using an identification of $T_p(TM)$ with $T_x M \times T_x M$. In general, there is no such canonical identification, so saying that $W$ is $(w, w')$ does not really make sense (although by the irrelevant details of the construction, $W$ is a member of some version of $E \times E$, so Lean understands the question). The reason is that you have a canonical subspace of $T_p(TM)$, the kernel of the derivative of the projection from $TM$ to $M$, 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)}M$ as $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?

[Koundinya Vajjha]

@Sebastien Gouezel , I was trying to access the local coordinates on $TTM$ induced by $M$.
The term tangent_bundle.pure is the zero section which is the "return" natural transformation of the monad structure of $T$. 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

[Koundinya Vajjha]

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.

[Sebastien Gouezel]

You say "access the local coordinates on $TTM$ induced by $M$", 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 $p$ in the tangent bundle (that you denote with $(x, x')$ -- this is a little bit misleading as $x'$ is a tangent vector), and then you have a tangent vector to this point, that you denote with $(v, v')$ but here you are abusing coordinates. Instead, let's just denote it with $W$. Then, you have the map $proj : TM \to M$. You can consider its differential at $p$, which is a map $T_p proj : T_p (TM) \to T_x M$. You can take the image of $W$ under this map, and you get canonically a well defined vector in $T_x M$. If I understand correctly, your map is therefore $(p, W) \mapsto (x, (v + T_p proj (W)))$ where $p = (x, v)$. If you try to work with this expression, things should go much more smoothly.

[Sebastien Gouezel]

Still, your formula is true, by the way!

[Koundinya Vajjha]

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)⟩

[Koundinya Vajjha]

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

[Koundinya Vajjha]

I'm still stuck on the second one but.

[Koundinya Vajjha]

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⟩⟩ :=

[Sebastien Gouezel]

Yes

[Koundinya Vajjha]

Is the proof simple?

[Sebastien Gouezel]

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

[Koundinya Vajjha]

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

[Sebastien Gouezel]

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.

[Koundinya Vajjha]

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?

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

Proof done in #4292

[Koundinya Vajjha]

Great! Thanks for your quick response!