Manifolds

Stream: PR reviews

[Sebastien Gouezel]

I am currently submitting my work on manifolds to mathlib. The first PR is #1359, but other ones are coming along the way. The current final state of things can be seen in https://github.com/sgouezel/mathlib/tree/manifold9. In the summary of #1359, I have added a list of what is coming next, but let me copy it here. Any comment or advice on design decisions or API is welcome in this stream.

Here is the summary of what is coming next:

• src/topology/local_homeomorph: local homeomorphisms (just like local equivs, but with open source and target, and continuous functions between them).
• geometry/manifold/fiber_bundle: fiber bundles (where the fiber is a topological space, the base is a topological space, and local trivializations are formulated using local homeos). Useful to define the tangent bundle later on.
• geometry/manifold/manifold: define a manifold modelled on a general topological space (where the charts are given by local homeos). Define groupoids of local homeos, and specify what it means for a manifold to have this groupoid as structure groupoid.
  *geometry/manifold/smooth_manifold_with_boundary: as a particular case of manifolds, define smooth manifolds with boundary, where the model space is a normed vector space (or a nice subset of such a vector space, for instance a half space), where the coordinate changes are smooth.
  *geometry/manifold/basic_smooth_bundle: define a specific kind of smooth vector bundles over a smooth manifold (the bundle should be trivial in the charts of the manifold), and use this machinery to define the tangent bundle (applications to differential forms or riemannian metrics should be easy, but are not done yet), as a smooth manifold.
  *geometry/manifold/mderiv.lean: the differential of a map between manifolds, as a map between tangent spaces. Follows the API for derivatives (and is defeq to the standard derivative when the manifold is a vector space, as it should be -- to get this was an important guidance in the choice of definitions).

[Patrick Massot]

This is glorious. Actual maths are about to enter the world of proof assistants!

[Patrick Massot]

About names (which are important for navigation):

• don't you want to rename fiber_bundle to topological_fiber_bundle?
• In smooth_manifold_with_boundary, do I understand correct that you include corners? If yes then the name is a bit misleading. You could either make it longer (including "corners") or shorter (dropping "with_boundary")

[Patrick Massot]

In mderiv, it's a bit sad to see continuity as requirement for differentiability. Can't you check differentiability in nicely related charts (with the image of the source chart contained in the target chart)? Is this related to your defeq constraint?

[Sebastien Gouezel]

I guess I will get some complaints here on Zulip about definitions such as

class smooth_manifold_with_boundary (𝕂 : Type*) [nondiscrete_normed_field 𝕂]
  (E : out_param $ Type*) [out_param $ normed_group E] [out_param $ normed_space 𝕂 E]
  (H : out_param $ Type*) [out_param $ topological_space H] [I : out_param $ model_with_boundary 𝕂 E H]
  (M : Type*) [topological_space M] [out_param $ manifold H M] extends
  has_groupoid H M (times_cont_diff_groupoid ⊤ 𝕂 E H)

If there are tricks to get a better API or a better use of typeclasses, I will be happy to hear about them!

[Sebastien Gouezel]

All the out_param are here so that you can just talk about the k-derivative of f : M -> M' and Lean will find all by itself the smooth manifold structures on M and M'...

[Patrick Massot]

This looks like a very general class that could have less hairy specializations making people happier

[Patrick Massot]

out_param magic is a difficult dark art where success can be asserted only after a lot of API usage

[Sebastien Gouezel]

In mderiv, it's a bit sad to see continuity as requirement for differentiability. Can't you check differentiability in nicely related charts (with the image of the source chart contained in the target chart)? Is this related to your defeq constraint?

There is really something tricky going on here: if your function is not continuous, then its image will typically not be contained in a chart. So you really need continuity if you want to be able to define differentiability. In the Isabelle paper on manifolds, they face the same issue, and they also have to include continuity in the definition of differentiability. And I guess any precise enough mathbook should also do it!

[Patrick Massot]

The definition I had in mind was: f is differentiable at x if there is a chart domain U containing x and a chart domain V containing the image of U such that the obvious composition is differentiable at the chart image of x. Is it junk?

[Sebastien Gouezel]

This looks like a very general class that could have less hairy specializations making people happier

Yes, there should be a specialization smooth_manifold k E M where H = E. With a notation, everything is fine. With a class extending the previous one, I don't know how to get instances right.

[Sebastien Gouezel]

The definition I had in mind was: f is differentiable at x if there is a chart domain U containing x and a chart domain V containing the image of U such that the obvious composition is differentiable at the chart image of x. Is it junk?

It's clearly equivalent, but this definition is more complicated to work with (you need to construct your V when you check differentiability, at least when you build the API)

[Sebastien Gouezel]

• don't you want to rename fiber_bundle to topological_fiber_bundle?

No strong opinion on this. According to wikipedia, a fiber bundle is by default a topological one, but I agree that most often we think of a smooth one.

[Patrick Massot]

Anyway, this definition is clearly part of the private API. What matters is that the definition matches the classical definition on open subsets of the model space and that a function on a submanifold is differentiable iff it extends as a differentiable function on a neighborhood (this covers in particular smooth functions on submanifolds of the model space).

[Patrick Massot]

About fiber bundle, I think adding "topological" avoids confusion for very little cost

[Patrick Massot]

At least in the file name

[Sebastien Gouezel]

• In smooth_manifold_with_boundary, do I understand correct that you include corners? If yes then the name is a bit misleading. You could either make it longer (including "corners") or shorter (dropping "with_boundary")

Yes, I include corners. In the beginning, I had the shorter version, but then I decided I wanted to keep it for the boundaryless version. I agree that smooth_manifold_with_corners is better, but it might look frightening. Or extended_smooth_manifold (less scary, but less precise as one doesn't know what the extension refers to). I guess I'll go for smooth_manifold_with_corners, less ambiguity is better.

[Patrick Massot]

https://github.com/sgouezel/mathlib/blob/manifold9/src/geometry/manifold/mderiv.lean#L709-L710 may be the first statement that I can recognize, but I like it.

[Sebastien Gouezel]

Functoriality is beautiful, especially when it hides all the mess of the definitions.

[Patrick Massot]

Funny you say that, I was thinking about the tangent functor. It's a big weird that the construction of the tangent bundle and mderiv are in separate file. A file tangent_functor.lean would be easier to find (but may be 2000 lines long...)

[Patrick Massot]

the differential of a map between manifolds, as a map between tangent spaces. Follows the API for derivatives (and is defeq to the standard derivative when the manifold is a vector space, as it should be -- to get this was an important guidance in the choice of definitions).

Why do the last few lemmas of mderiv.lean suggest this is not a defeq?

[Sebastien Gouezel]

Funny you say that: at the beginning, it was the other way around, with first the construction of mderivand then deriving the tangent bundle from it. But the construction was a little bit ad hoc, and I would have needed to redo everything to construct differential forms or riemannian metrics. I decided that to get a general machinery would be more efficient (and indeed the general machinery is not really longer than the direct construction using mderiv, surprisingly).

[Patrick Massot]

I meant you could end the first file at https://github.com/sgouezel/mathlib/blob/manifold9/src/geometry/manifold/basic_smooth_bundle.lean#L255

[Patrick Massot]

and move the end to mderiv.lean, renamed tangent_functor.lean

[Sebastien Gouezel]

the differential of a map between manifolds, as a map between tangent spaces. Follows the API for derivatives (and is defeq to the standard derivative when the manifold is a vector space, as it should be -- to get this was an important guidance in the choice of definitions).

Why do the last few lemmas of mderiv.lean suggest this is not a defeq?

You are right, it's not a defeq. But it's the same map, and in particular the domain of definition of the linear map is the same space (i.e., not the vector space for the first one and a crazy quotient or a crazy space of derivations for the second one).

[Patrick Massot]

The crazy space of derivation is crazy algebraic geometry bullshit anyway. And you didn't restrict to $C^\infty$ anyway, right?

[Sebastien Gouezel]

I meant you could end the first file at https://github.com/sgouezel/mathlib/blob/manifold9/src/geometry/manifold/basic_smooth_bundle.lean#L255

Yes I could, but the file would become super-long. I was more planning of including the other constructions (differential forms, metrics) also in basic_smooth_bundle .

[Patrick Massot]

I guess crazy quotient refer to space of smooth curves modulo the same speed relation? This is a nice relation but indeed you only get a isomorphism in the vector space case

[Patrick Massot]

You'll need to split off tensor bundles in all cases

[Patrick Massot]

I'd like to read more about how you avoided those definitions of the tangent bundle but still remained functorial

[Sebastien Gouezel]

The crazy space of derivation is crazy algebraic geometry bullshit anyway. And you didn't restrict to $C^\infty$ anyway, right?

Well, it works perfectly well in any smoothness, but typeclass inference doesn't like it when there is an additional unspecified parameter of smoothness. And if you want to talk about C^k functions on a C^r manifold, then you would need to infer automatically inequalities like k <= r, which looks like a daunting task. So I only give the definition for C^oo manifolds for simplicity.

[Sebastien Gouezel]

I guess crazy quotient refer to space of smooth curves modulo the same speed relation? This is a nice relation but indeed you only get a isomorphism in the vector space case

Yes, that's the most intuitive definition but not the easiest to work with in a formal way.

[Patrick Massot]

I'm confused about the smoothness answer. I think there are different discussions. Defining the tangent space using derivations does not work in finite regularity, you get infinite dimensional tangent space in all cases. Then you say you used a definition that could work in the finite differentiability case, except that Lean would make it harder?

[Sebastien Gouezel]

I'd like to read more about how you avoided those definitions of the tangent bundle but still remained functorial

It's just a hack, that should make both computer scientists and mathematicians crazy. It's explained in the docstring of https://github.com/sgouezel/mathlib/blob/manifold9/src/geometry/manifold/fiber_bundle.lean

[Sebastien Gouezel]

Then you say you used a definition that could work in the finite differentiability case, except that Lean would make it harder?

Yes, that's it. My definition works in any smoothness, but it's easier to use for Lean in infinite smoothness.

[Patrick Massot]

This fiber bundle hack is really shocking. I'll need time to stomach it

[Johan Commelin]

So, if I have a map p : E → B, I cannot tell Lean that it is a fibre bundle. Do I understand that correctly?

[Jeremy Avigad]

I guess it is not too hard to construct the relevant fibre bundle and characterize its relation to p? Anyhow, it looks like a nice solution to me.

[Johan Commelin]

Probably yes, but I imagine that it would be nice to have good API for this. Otherwise it will become frustrating rather soon.

[Johan Commelin]

For example, I would like prod.fst and prod.snd to both be fibre bundles

[Sebastien Gouezel]

Indeed, I have only implemented the bundled version of fiber bundles, but one could also need the unbundled version is_fiber_bundle p, where p : E -> B is a map between topological spaces and all the standard properties hold. For what I wanted to do, the bundled version is more efficient (in particular since it builds the total space of the bundle and its topology for me).

[Sebastien Gouezel]

Many things with fiber bundles seem easier to do with the bundled version, by the way (fibered products, pullbacks, K-theory, characteristic classes...).

[Kevin Buzzard]

Just to say that this sort of technical conversation involving expert mathematicians trying to formalise serious stuff in mathlib is such a joy to see -- it is something we were so far from 2 years ago and it's very exciting to see it happening in Lean. Thank you Sebastien and thank you also Patrick for keeping a very close eye on what he is doing.

[Johan Commelin]

@Sebastien Gouezel But in this case the bundled version is not (close to being defeq to) {p // is_fiber_bundle p}.

[Johan Commelin]

So it might be even harder to apply a "bundled fact" to an unbundled fibre bundle than the usual (un)bundling dance

[Sebastien Gouezel]

From the unbundled version you can construct a bundled version (using all the possible trivializations), from which you can get an unbundled version which will be isomorphic to the original one, but definitely not defeq, I agree.

[Scott Morrison]

It's explained in the docstring of https://github.com/sgouezel/mathlib/blob/manifold9/src/geometry/manifold/fiber_bundle.lean

This seems to have disappeared? I get a 404.

[Floris van Doorn]

new link: https://github.com/sgouezel/mathlib/blob/manifold9/src/geometry/manifold/topological_fiber_bundle.lean

[Sebastien Gouezel]

Yes, sorry for the inconvenience but the name change was a request of the referee here on Zulip :)

[Patrick Massot]

Sébastien, I thought a bit more about your topological fiber bundle hack, and I think this is a pretty serious issue, and such a decision should be given really serious consideration. Having a trustworthy type checker is wonderful, but formalization will always involve human deciding whether the bit of formalized math they are looking at has anything to do with what is in their head and has the same name.

For people who don't know about manifolds, let me try an analogy. An elementary version of what Sébastien did would be to start rat.lean with def ℚ : Type := ℕ, then write 500 lines defining algebraic operations on ℚ (secretly using your favorite enumeration of ℚ to import the usual operations), and then write 1000 lines proving that ℚ, endowed with these operation is a field of characteristic zero, and it uniquely embeds into every field of characteristic zero, or some other property aiming to convince the reader that ℚ is the field there are thinking of, and provide an API to manipulate its elements.

This is not to be confused with the divide by zero or the rooster and butterflies scandals. Those shock mathematicians, but are only extensions of what we would do. Here there is no intersection with real world.

I think the goal of having the tangent bundle to a vector space E equal (not even definitionaly) to E × E is not worth this. Even in sloppy real world math we write an isomorphism sign here. When I dream of manifolds in a proof assistant, I rather see to_manifold, a variation on the to_additive tactic that would turn lemmas about open subsets of vector spaces (or, better, of affine spaces) into lemmas about manifolds. This I think would have been a much nicer guide.

[Sebastien Gouezel]

Some more context. A fiber bundle above a space B with fiber E is a space Z with a projection on the base, such that all its fibers are homeomorphic to E (plus a local triviality condition that I will omit in the discussion). The usual way to construct a fiber bundle is to have local trivializations, and to say what happens when one changes trivialization. I.e., one has a space I of local trivializations, and open sets O_i, and for each i and j and each x ∈ O_i ∩ O j one has homeomorphisms \phi_{ij}(x) of E, that satisfy a (compatibility) cocycle condition. Then the space of the fiber bundle is constructed by gluing above each x copies of E indexed by those i where x ∈ O_i, where the gluing is made using the \phi_{ij}. So the fiber above x is isomorphic to E, but not canonically (each choice of some i gives an isomorphism between the fiber and E).

What I do is that I avoid the gluing completely and use choice instead, choosing one specific isomorphism above x to identify the fiber above x with E -- this amounts to choosing one preferred trivialization at each point. Which means that in practice the total space of my bundle is just B × E (this definitely makes sense mathematically, the total space of the fiber bundle is in bijection with B × E, although non-canonically).

The claim is that the construction is much shorter this way (no need to define all the identifications, to show that the fiber defined as a quotient has a vector space structure, a topological space structure, and so on). And also it avoids a lot of DTT hell further on, as all fibers are the same to Lean (although this is completely hidden from the user by the API).

I knew that this would make mathematicians scream (because the definition I use is certainly not "the right one"), and computer scientists also because I use choice where it is not needed. (In fact, choice is not apparent in my development, as the very definition of fiber bundle takes a preferred trivialization at each point -- this is a way to express that the O_i cover the base). But I have really thought this through, and in the end if you don't like the definition you just need to use the API (just like I don't even know how rationals are defined in Lean, as a type of coprime pairs of integers or as a quotient).

[Patrick Massot]

Some more context. A fiber bundle above a space B with fiber E is a space Z with a projection on the base, such that all its fibers are homeomorphic to E (plus a local triviality condition that I will omit in the discussion). The usual way to construct a fiber bundle

There is something crucial here. You are talking about constructing a fiber bundle. I'm talking about defining fiber bundles. There could be a nice mathematical definition and a crazy constructor. Then the constructor can be as crazy as you like it.

Which means that in practice the total space of my bundle is just B × E (this definitely makes sense mathematically, the total space of the fiber bundle is in bijection with B × E, although non-canonically).

This is why I took the example of ℚ defined as ℕ equipped with some weird operations. There are indeed bijections from ℚ to ℕ, but I wouldn't say it "makes sense mathematically".

[Sebastien Gouezel]

Well, there has to be a definition of ℚ in Lean. And it has to be some definition like that, and one should choose the definition that is the most convenient to prove things about it. That's what I tried to do for fiber bundles.

[Patrick Massot]

Did you at least prove that your "fiber bundles" are actual fiber bundles?

[Sebastien Gouezel]

Yes, I construct a family of local trivializations \psi_i, which are local homeomorphisms, and such that the initial phi_{ij}is the composition \psi_i o \psi_j^{-1}. This is all the point of the construction: to put a topology on the total space of the bundle and check that everything works out as it should.

[Patrick Massot]

Maybe I should insist again that I'm thrilled that manifolds are arriving to Lean, and I know you are a much better mathematician and formalizer than I am. But I really fear the hiatus between maths and formalizing math is too wide here.

[Patrick Massot]

Why not defining actual fiber bundles then? And provide a crazy constructor.

[Sebastien Gouezel]

Honestly, I don't think the hiatus is that big. In ergodic theory, it is very common to start from an arbitrary bundle and to trivialize it (measurably) on a set of full measure. Again, I am just choosing one isomorphism with E in each fiber, among all those that naturally exist. And this is all about the constructor, that you can forget about just like the specific definition of ℚ .

I did not define actual fiber bundles because the actual definition is terribly messy, and I didn't need it.

[Sebastien Gouezel]

Most constructions (pullback, fibered product, and so on) are also much easier to do in terms of the constructor, by the way.

[Sebastien Gouezel]

I have reworked a little bit the terminology, and I agree the new version looks much better. Now, I have a predicate is_topological_fiber_bundle, which corresponds to what you think (and I prove that the first and second projections in a direct product satisfy this predicate). And I have a structure topological_fiber_bundle_core (but I could rename it to topological_fiber_bundle_pkg or whatever you like), from which I can construct a total space and a projection, and I prove that these satisfy is_topological_fiber_bundle. In particular, I have made it clear that this trick I use with choice is only for constructing a fiber bundle from a topological_fiber_bunde_core. New version at https://github.com/sgouezel/mathlib/blob/manifold9/src/geometry/manifold/topological_fiber_bundle.lean . @Patrick Massot , does it look better like that, and do you still see possible improvements?

[Patrick Massot]

I had a quick look, and it certainly looks better. I'm don't understand how you encode structure groups though. Will this come later?

[Sebastien Gouezel]

In a is_topological_fiber_bundle, there is no structure group. In a topological_fiber_bundle_core, it is already there as one can start from a structure in which the coordinate change live in a smaller group than all the homeos of F, and then this will be respected in the construction of the fiber bundle.

[Patrick Massot]

Maybe I should have written that I'd like to see how you can do is_bundle_with_group on top of that

[Patrick Massot]

It's so ironic that each time I explain dependent type to anyone, I always say: it's very simple, it's like a fiber bundle...

[Sebastien Gouezel]

Maybe I should have written that I'd like to see how you can do is_bundle_with_group on top of that

You could have a Prop defining this, requiring the existence of a family of local trivializations for which the change of coordinates in the fibers all belong to a given group. But I think I would rather go a different way, with more data, as follows: I would register a manifold structure on the total space of the bundle, with model space B \times F (this is the data), and then having some structure group means that the coordinate changes belong to some groupoid of B \times F (with the identity in the basis, and your preferred group in the fiber). In this way, this fits nicely with the existing infrastructure.

[Johan Commelin]

@Sebastien Gouezel Will this framework be general enough to also do complex holomorphic manifolds?

[Reid Barton]

I think so

[Reid Barton]

Take k = C, E = H = C^n, and use the groupoid of holomorphic functions (once you define those)

[Sebastien Gouezel]

Take k = C, E = H = C^n, and use the groupoid of holomorphic functions (once you define those)

Yes. And holomorphic functions are already defined in this setting, as they are just the C^1 functions :)

[Johan Commelin]

Fantastic!

[Scott Morrison]

It's so exciting seeing the manifolds PRs coming in. :-)

[Scott Morrison]

Can I ask, @Sebastien Gouezel, how you would anticipate modelling stratified spaces?

Will we just be able to say: a sequence of closed subsets S_0 < S_1 < ... < S_n = M, so that S_{k+1} \setminus S_k is a (k+1)-dimensional submanifold of M?

[Sebastien Gouezel]

I am not sure of what definition of stratified space you mean. In the definition I have in mind, the global space can be singular, and only the intermediate pieces are nice, so you can't say that you have submanifolds of an ambient manifold. But you could for instance say that you have a manifold structure on each S_{k+1} \setminus S_k as a subtype. Or a sequence of manifolds that embed in your space, with compatibility conditions. The only way to work out the most efficient definition would be to start proving theorems!