## Stream: maths

### Topic: help with mfderiv

#### 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


#### Koundinya Vajjha (Sep 26 2020 at 03:56):

Does anyone have any pointers?

#### 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.

#### Sebastien Gouezel (Sep 26 2020 at 09:11):

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 (Sep 26 2020 at 13:16):

@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

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



#### 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.

#### Sebastien Gouezel (Sep 26 2020 at 14:56):

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 (Sep 26 2020 at 15:29):

Still, your formula is true, by the way!

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


#### Koundinya Vajjha (Sep 26 2020 at 15:34):

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

#### Koundinya Vajjha (Sep 26 2020 at 15:34):

I'm still stuck on the second one but.

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


Yes

#### Koundinya Vajjha (Sep 26 2020 at 15:40):

Is the proof simple?

#### Sebastien Gouezel (Sep 26 2020 at 15:41):

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

#### Koundinya Vajjha (Sep 26 2020 at 15:41):

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

#### 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.

#### 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?

#### 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.

#### Sebastien Gouezel (Sep 27 2020 at 20:39):

Proof done in #4292

#### Koundinya Vajjha (Sep 28 2020 at 01:13):

Great! Thanks for your quick response!

Last updated: May 14 2021 at 17:42 UTC