Product manifolds

Stream: maths

[Sebastien Gouezel]

@Nicolò Cavalleri has just told me about a problem he met when defining product manifolds, and I would like to hear opinions on this. Currently, a charted space M with model H is a set of local charts from M to H covering the space. Every space is registered as a charted space over itself, using the only chart id, in charted_space_self. You can also define a product of charted space M and M' (with model space H \times H') by taking the products of the charts. Now, on H \times H', you have two charted space structures with model space H \times H' itself, the one coming from charted_space_self, and the one coming from the product of the two charted_space_self on each component. They are equal, but not defeq (because the product of id and id is not defeq to id), which is bad as we know.

I don't see how to solve this cleanly: forgetful inheritance is not really relevant, and both instances are important (you definitely want to think of a vector space as a manifold over itself, and also you want to be able to talk of product manifolds). Thoughts welcome!

[Johan Commelin]

Would it help if we use a type synonym for the model?

[Johan Commelin]

So that a vector space V has model model V

[Johan Commelin]

And then V × V' is a manifold over (model V) × (model V') and over model (V × V').

[Johan Commelin]

Wait... I need type signatures.

[Johan Commelin]

The model is an explicit parameter, right?

[Sebastien Gouezel]

That's a good idea. It seems cheaper to do it for products, though: the model space for M \times M' could be model_prod H H'.

[Johan Commelin]

Aha, that's probably even better.

[Nicolò Cavalleri]

Sebastien Gouezel said:

That's a good idea. It seems cheaper to do it for products, though: the model space for M \times M' could be model_prod H H'.

Well renaming that for products seems to break this definition:

/-- The product of two smooth manifolds with corners is naturally a smooth manifold with corners. -/
instance prod_smooth_manifold_with_corners {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
  {E : Type*} [normed_group E] [normed_space 𝕜 E]
  {E' : Type*} [normed_group E'] [normed_space 𝕜 E']
  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
  {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]
  (M' : Type*) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] :
  smooth_manifold_with_corners (I.prod I') (M×M') :=
{
  compatible :=
  begin
    intros f g,
    rintros ⟨f1, hf1, f2, hf2, hf⟩ ⟨g1, hg1, g2, hg2, hg⟩,
    rw [hf, hg, local_homeomorph.prod_symm, local_homeomorph.prod_trans],
    have h1 := has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) hf1 hg1,
    have h2 := has_groupoid.compatible (times_cont_diff_groupoid ⊤ I') hf2 hg2,
    exact times_cont_diff_groupoid_prod h1 h2,
  end,
}

with this error:

failed to synthesize type class instance for
𝕜 : Type ?,
_inst_7 : nondiscrete_normed_field 𝕜,
E : Type ?,
_inst_8 : normed_group E,
_inst_9 : normed_space 𝕜 E,
E' : Type ?,
_inst_10 : normed_group E',
_inst_11 : normed_space 𝕜 E',
H : Type ?,
_inst_12 : topological_space H,
I : model_with_corners 𝕜 E H,
H' : Type ?,
_inst_13 : topological_space H',
I' : model_with_corners 𝕜 E' H',
M : Type ?,
_inst_14 : topological_space M,
_inst_15 : charted_space H M,
_inst_16 : smooth_manifold_with_corners I M,
M' : Type ?,
_inst_17 : topological_space M',
_inst_18 : charted_space H' M',
_inst_19 : smooth_manifold_with_corners I' M'
⊢ charted_space (H × H') (M × M')

that seems to require naturally the charted space built on the product of both the model spaces and the charts, even if I think I never mentioned H \times H' anywhere in the manifold file. (I am not too sure why as I did not look to closely into the details of models with corners).
In case we adjust it, just to know, is it cheaper for products in terms of amount of code to be rewritten or like computationally? The cool thing about the product is that notationally everything involved in the product is written as a product and a lot of symmetric lemmas like

@[simp] lemma chart_of_prod_eq_prod_of_charts_coe :
  (chart_at (H×H') x : M × M' → H × H') = (prod.map (chart_at H x.fst) (chart_at H' x.snd))

become notationally quite dirty!

[Johan Commelin]

I will defer to @Sebastien Gouezel ...
I haven't had time to dive into the details of this part of the library yet.

[Sebastien Gouezel]

Yes, things will need fixing after this change, but it's worth it. I can take care of it, if you give me access to your files.

[Nicolò Cavalleri]

@Sebastien Gouezel I am having some problems with this new definition of model_prod. The first problem is directly connected to it: it broke my definition of prod_Lie_group. I do not understand why the library keeps requiring instances built on H \times H'even after you replaced everything with model_prod. I uploaded everything on a branch of Mathlib if you want to have a look: https://github.com/leanprover-community/mathlib/tree/Lie_groups/src/geometry
The second problem is in the second point below.

In this light I am still wondering why was it a good idea to use the synonym for products instead that for charted_space_self. I am clearly a newbie here so I don't want to question your choice, but I'd be very curious just to know the reason behind it. To me (again, a complete newbie) there's two big cons:

• it looks to me that the theory of smooth manifolds over R^n is very common, in that the basics are taught in every undergraduate course in physics and maths worldwide, whereas the theory of general charted spaces is less common: I did Part III in geometry but if I have to be sincere it is the first time I hear the term "charted spaces". For this reason I believe that newbies who will start working with the library in the future will almost surely encounter and use the instance of product manifolds many times, whereas the instance charted_space_self that is much more technical might remain buried under the whole math build upon it and people might never encounter it and need to use it (I mean I don't know but I never used it in my definitions up to now). This means that, provided that in both cases things will require adjustments every time they are used, as it looks to be the case, people who will use the geometry section of the library will first of all need to know and learn these technicalities about the library in order to use it, whereas, again, in the other case they probably won't need to learn the details of the library too much as charted_space_self might not be needed again. Hence, people who are not Lean expert will need to rely on your help each time to ask you for adjustments as I am doing now (whereas before I was able to state these particular definitions without asking your help) therefore loosing independence and making you loose time.
• Secondly goals in results that use product manifolds become more technical and cryptic and it's harder, for who does not know Lean well, to understand if sometimes Lean does not recognize things because this model_prod is being used or if the problem is elsewhere. Take for example the lemma tangent_bundle_proj_smooth in the file constructions that I put in this branch Lie_groups the last simp does not simplify terms of the form

(λ (x_1 : E × E), ⇑((chart_at (model_prod H E) x).symm) (⇑(I.symm) x_1.fst, x_1.snd)

by breaking up (chart_at (model_prod H E) x) as the apposite simp lemma requires, and I do not understand if in this case it is because the normal simp lemmas do not imply that the coercions should get simplified (as it looks it should however be the case from what you told me in the last PR we made together), or if it is model_prod that is creating problems. Again, I guess this kind of problems would be there also with the other synonym, but again I guess people would encounter it much less frequently.

Let me know what you think

[Sebastien Gouezel]

We have to introduce a type synonym to avoid typeclass issues. The idea is to insert it where it is least annoying, i.e., where people will encounter it less often. I have the impression that product manifolds will appear way less often than charted_space_self, which is why I introduced the type synonym on product manifolds. Indeed, whenever you speak of a smooth function from a vector space to a manifold or conversely, you are using a manifold structure on the vector space, which is precisely charted_space_self. And this happens all the time! (for instance when saying that charts are smooth).

Of course, we should also make sure that working with product manifolds is as easy as possible. The library is just in its infancy in this direction (you have only introduced them in the last PR), so there are still a lot of rough edges, that we will hopefully be able to smoothen. I will have a look at tour branch.

[Nicolò Cavalleri]

Sorry where is charted_space_self introduced in the library? I cannot find it! (VScode tells me it does not exist)

[Sebastien Gouezel]

Woops, that's the name in the version on my computer, not yet PRed to mathlib. In current mathlib, it is still named manifold_model_space.