# Zulip Chat Archive

## Stream: maths

### Topic: manifolds

#### Hoang Le Truong (May 11 2019 at 05:41):

I have the definition of manifold over a normed field in Lean. You can see it in the following link

https://github.com/truonghoangle/manifolds

If you do not mind, please can you give me advice about it, special name of function or section and approach way to the definition of tangent bundle.

#### Johan Commelin (May 11 2019 at 05:47):

Are you aware of the fact that @Sebastien Gouezel is also working on manifolds? Did you coordinate with him?

#### Hoang Le Truong (May 11 2019 at 05:54):

When I began with manifold, I did not known @Sebastien Gouezel is also working on manifolds. Now I will contact him.

#### Johan Commelin (May 11 2019 at 05:56):

Here is one discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Multiple.20differentiability

#### Johan Commelin (May 11 2019 at 05:57):

Here is another one that might be relevant: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/out_param

#### Johan Commelin (May 11 2019 at 06:00):

@Hoang Le Truong Here is another attempt by Patrick: https://github.com/PatrickMassot/lean-differential-topology

#### Hoang Le Truong (May 11 2019 at 06:00):

Thank @Johan Commelin for your information

#### Sebastien Gouezel (May 11 2019 at 07:33):

The current state of thingsI have done on manifolds is in https://github.com/sgouezel/mathlib/blob/manifold4/src/geometry/manifolds/basic.lean. I am going for a more general approach, that would also encompass manifolds with boundaries, or manifolds with corners, or Thurston's (G,X) structures, but essentially the basic definitions are the same as yours, i.e., an atlas such that the changes of charts belong to some class of maps (called a groupoid, as in the fundamental textbook of Kobayashi and Nomizu). What I have done so far:

- extended the material on derivatives, to get access to a convenient API (PRed in #966)
- defined local equivalences, just like you do except I use genuine functions instead of pfuns, to avoid defining yet another notion of derivatives (and I don't care what the functions do outside of their domains and codomains), and defined a basic interface for them (in https://github.com/sgouezel/mathlib/blob/manifold4/src/geometry/manifolds/local_equiv.lean). The fact that this is a good choice has been questioned by several people on Zulip, who encouraged me to use pfuns as you do, but for now it seems to go rather smoothly -- I need to develop the library further to see what the advantages and drawbacks are.
- defined C^n functions, and proved basic properties (invariance under addition, composition, and so on), in https://github.com/sgouezel/mathlib/blob/manifold4/src/geometry/manifolds/times_cont_diff.lean
- defined general manifolds based on groupoids. As well as diffeomorphisms (for the groupoid structure), and proved that the inverse or the composition of two diffeomorphisms is a diffeomorphism (this is not so obvious) in https://github.com/sgouezel/mathlib/blob/manifold4/src/geometry/manifolds/basic.lean. Specialized to smooth manifolds, for which I am now defining the tangent space.

My goal would be to go up to the Whitney embedding theorem (any smooth real manifold embeds in R^N for large enough N), which is a non-trivial theorem, to stress-test the definitions and the interface.

#### Sebastien Gouezel (May 11 2019 at 07:44):

One important point in library-building, I think, is that writing down definitions is not enough: you need to prove theorems, to see how definitions work out well or not, and what interface you need for the proofs. For instance, the first statement I settled to prove is that the composition of diffeomorphisms is a diffeomorphism. This showed me that I needed to implement a serious interface to local equivs, that now takes over 800 lines. And now defining the tangent space shows me gaps in this interface, that I will have to fill.

#### Hoang Le Truong (May 11 2019 at 08:11):

My goal would be to go up to the Hodge theorem. I also think that the definition is right through the proof of the theorems. For instance about tangent bundle, we have three ways to give the definition. Moreover, for complex manifold, we have three tangent bundle. I am struggling between approachable approach on complex, real number and general ways.

#### Johan Commelin (May 11 2019 at 08:17):

Do you want to state the Hodge theorem or also prove it?

#### Johan Commelin (May 11 2019 at 08:17):

Either of them would be fantastic!

#### Sebastien Gouezel (May 11 2019 at 08:30):

I am going for a general way (over any field), as follows: let `charts x`

be the set of all charts around `x`

. If `e`

and `e'`

are such charts, they yield a linear map from `E`

to `E`

, the derivative of `e' o e^{-1}`

. Take the quotient of `(charts x) × E`

under these identifications, this gives the tangent space. Hopefully, this should be easily generalizable to define exterior or symmetric products of the tangent bundle, opening the way to Riemannian metrics and to differential forms. But before doing the general case, I will stick to tangent spaces for now.

#### Sebastien Gouezel (May 11 2019 at 08:32):

Another definition would be to choose one chart around each point, and only use this one to define the tangent space. This avoid taking a quotient, but it is less canonical. I will have to do it at some point, though, because I will want the derivative of a map to be a bounded linear map between tangent spaces, and for this I need a normed space structure on the tangent space, for which there is no canonical choice.

#### Patrick Massot (May 11 2019 at 08:33):

I think there will be painful points in any case, the only question is whether the API will be able to hide them

#### Sebastien Gouezel (May 11 2019 at 08:40):

Yes, it is definitely going to be nontrivial.

#### Hoang Le Truong (May 11 2019 at 09:47):

@Johan Commelin I want to prove it but first step is to give the statement of the Hodge theorem

#### Hoang Le Truong (May 11 2019 at 09:56):

@Sebastien Gouezel are you think how definition of tangent space via derivations is good

#### Hoang Le Truong (May 11 2019 at 09:59):

@Patrick Massot can you explain detaily about whether the API will be able to hide them

#### Sebastien Gouezel (May 11 2019 at 10:03):

Definition of tangent space via derivations is very nice, but as far as I remember proofs that it behaves well require localizing functions around the point, and while this works well over R this creates problems over C where you don't have partitions of unity. And this construction is really specific to tangent spaces, while the stupid approach using equivalence classes of vectors should be generalizable to other vector bundles.

#### Kevin Buzzard (May 11 2019 at 10:15):

One important point in library-building, I think, is that writing down definitions is not enough: you need to prove theorems, to see how definitions work out well or not, and what interface you need for the proofs.

Tom Hales' project does not need proofs, so for this project one *might* find that writing down definitions is in many cases enough. If the goal is just to formalise statements of theorems then this might provide far fewer demands on the definition-builder.

#### Hoang Le Truong (May 11 2019 at 10:26):

With complex maifold we have real tangent bundle, complexified tangent bundle and holomorphic tangent bundle. In fact, we begin with real tangent bundle. So I don't understand what the problems over C is.

#### Sebastien Gouezel (May 11 2019 at 11:22):

You don't need to separate the real case and the complex case: there is a definition which works for both at the same time. So, to minimize work, it is probably better to use this one.

#### Hoang Le Truong (May 17 2019 at 09:02):

@Sebastien Gouezel I read carefully the definition of very general manifold. It is very nice. I have question:What is the definition of submanifold? Is the definition of submanifold dependent on model space?

#### Neil Strickland (May 22 2019 at 08:17):

Can you comment on why your `local_equiv α β`

actually involves maps defined on all of `α`

and `β`

, rather than just the indicated subsets? This seems to be asking for trouble later. Among other things, it means that an empty type cannot have a local equivalence with a nonempty one, which is a problem if `α`

and `β`

arise naturally as subtypes of something else. Can you not use maps `α → roption β`

and `β → roption α`

or something like that? That way, the `eq_on_source`

thing would become unnecessary.

#### Sebastien Gouezel (May 22 2019 at 11:35):

There are pros and cons to both approaches, i.e. (1): functions defined everywhere, but you don't care about the values outside of the source, and (2): roption, i.e., really kill the values outside of source.

In (1), if functions are equal on the source but different outside, then they are not equal, while you want to think of them as the same function. That's the role of `eq_on_source`

, which is definitely an annoyance.

In (2), your function does not take values in the right space, and this calls for trouble. For instance, if you want to define the derivative of a function `f : M -> M' `

where `M`

and `M'`

are manifolds, what you do is write `f`

in charts, i.e., consider `e' o f o e^{-1}`

where `e`

and `e'`

are charts around `x`

and `f x`

, and then you differentiate. With the roption approach, what you get is a function from `E`

to `roption E'`

, so you can not define the derivative as the limit of `(f(x+hv)-f(x))/h`

when `h`

tends to `0`

(or an equivalent definition using small o) as it does not make sense to subtract elements of `roption E'`

, or to divide them by a scalar. So, you would need to extend many algebraic definitions to `roption`

, or to restrict your function to some suitable set and play some nontrivial dance there.

I have the feeling that (2) will create many more concrete problems than (1). Most of the time, we don't care at all about equality of charts, we just use one given chart and that's it. While having to reproject your function back to `E`

to do some algebraic manipulation happens all the time. That's why I went for (1). But you are not the first person to voice concerns about this choice.

#### Mario Carneiro (May 22 2019 at 11:53):

You can define the derivative when the function is defined on an open set around the target point

#### Mario Carneiro (May 22 2019 at 11:54):

the little o definition with a filter for roption functions actually makes this pretty painless

#### Mario Carneiro (May 22 2019 at 11:54):

Jeremy and I worked it out a while ago

#### Sebastien Gouezel (May 22 2019 at 12:04):

You can definitely work it out. The same for continuity: there is already an API for continuity of partial functions, crafted by Jeremy. Except that it is some amount of work. Then when you want to talk about C^k functions, or analytic functions, or Besov functions, or whatever, and even if you have already done it for functions you will need to spend some time to define again the same notions for partial functions (with a well developed API if you want these notions to be usable). This is completely avoided by the approach (1), at the expense of the mild annoyance that equality between charts (which is essentially never used) is not the right notion.

#### Mario Carneiro (May 22 2019 at 12:04):

You don't want to lift every algebraic operation to roption exactly; you use the monad structure for that

#### Mario Carneiro (May 22 2019 at 12:05):

I'm not sure it's true to say it's completely avoided; instead you have to build an API for `eq_on_bla`

and `local_equiv`

and such. It's moving the work elsewhere

#### Sebastien Gouezel (May 22 2019 at 12:08):

I think in any case you will need to build an API for `local_equiv`

. Even with partial functions, you will need to bundle two partial functions which are inverse to each other on their respective domains, and see how they compose and so on.

#### Mario Carneiro (May 22 2019 at 12:10):

no, that's equiv of subtypes

#### Sebastien Gouezel (May 22 2019 at 12:16):

Not really, because you want to be able to compose them even when when the target of the first one is not the source of the second one, by automatically taking the intersection of the domains. Composition of roption-valued functions does that automatically, but composition of equivs of subtypes does not.

#### Mario Carneiro (May 22 2019 at 12:18):

that's true. I guess you need to forget about the domains in the types in your case

#### Mario Carneiro (May 22 2019 at 12:19):

still I like the fact that using subtypes gives you topology for free... can roption do the same?

#### Hoang Le Truong (May 22 2019 at 12:24):

2) With the roption approach, I change a function `E → roption E`

to function ` E → E`

by

```
def ext_by_zero(f : β →. α) (z:β) : α :=
if h:z ∈ f.dom then f.fn z h else 0
```

When we only work on `x ∈ f.dom`

#### Hoang Le Truong (May 22 2019 at 12:25):

Fisrt I work only with complex field and definition of `manifold ℂ β`

`local_equiv α β`

also work only funtions `α → β`

. But we can change ℂ to any field `k`

. When we work on field `𝔽₁`

then empty function joint theory as absorbing element. Therefore I choose `local_equiv α β`

include empty function

#### Mario Carneiro (May 22 2019 at 12:25):

I think the natural topology on roption A is the one-point compactification

#### Mario Carneiro (May 22 2019 at 12:28):

@Johannes Hölzl Do you know a way to do the topology of `roption A`

with filters?

#### Sebastien Gouezel (May 22 2019 at 14:07):

I am still puzzled by my question that started this thread: how come a `simp`

invocation can create a ghost duplication of some objects, that disappears if one adds a `rw`

just before, in https://github.com/sgouezel/mathlib/blob/f6d6492e7a8b892b4a22fb010fb12d1a4695d38a/src/geometry/manifolds/mderiv.lean#L604. Any hint on what is going on would be welcome.

#### Reid Barton (May 23 2019 at 15:02):

I wonder whether it would be useful to introduce germs of functions here (a "germ of a function f : X -> Y at x : X" is a neighborhood N of x together with a function N -> Y, modulo the relation that two germs agree if they have a common restriction to a smaller neighborhood). Notions like continuity, derivatives and all higher-order information is local--meaning it only depends on the germ.

#### Reid Barton (May 23 2019 at 15:11):

I guess it's better to only allow continuous functions, so that you can compose germs.

#### Neil Strickland (May 23 2019 at 15:14):

I think that it would be best if the foundations of manifolds used sheaves explicitly. If you don't do it explicitly then I think you end up duplicating a lot of the ideas anyway. Many of the most popular manifolds are algebraic varieties, and you make the interface with algebraic geometry much smoother if you use similar foundations. In that context, germs become very natural.

#### Johan Commelin (May 23 2019 at 15:22):

This has been discussed, but Patrick and Sebastien both said that this is not a good strategy for the general theory of manifolds. I trust their judgment.

#### Kevin Buzzard (May 23 2019 at 16:48):

Maybe for them, many of the most popular manifolds are not algebraic varieties.

#### Sebastien Gouezel (May 23 2019 at 18:28):

For me, elliptic curves are surfaces, and they are all the same :)

#### Kevin Buzzard (May 23 2019 at 18:28):

yeah that's not a good sign

#### Kevin Buzzard (May 23 2019 at 18:28):

I spent many years studying their moduli spaces!

#### Kevin Buzzard (May 23 2019 at 18:29):

For you it's the one point set.

#### Johan Commelin (May 23 2019 at 18:32):

@Sebastien Gouezel Aren't you interested in varying an almost complex structure on that unique elliptic curve?

#### Sebastien Gouezel (May 23 2019 at 18:33):

Of course I am joking. Teichmüller space is one of my favorite playgrounds.

#### Sebastien Gouezel (May 23 2019 at 18:49):

I wonder whether it would be useful to introduce germs of functions here (a "germ of a function f : X -> Y at x : X" is a neighborhood N of x together with a function N -> Y, modulo the relation that two germs agree if they have a common restriction to a smaller neighborhood). Notions like continuity, derivatives and all higher-order information is local--meaning it only depends on the germ.

I considered this, or at least introducting predicates `locally_equal_at`

and `locally_equal_within_at`

. Finally, I decided that it does not help much to simplify other arguments, so I haven't introduced the definition, but I am still using it implicitely at some places, see for instance https://github.com/sgouezel/mathlib/blob/6d693c310ab036171dabadcf8924e5bc15ec8054/src/geometry/manifolds/mderiv.lean#L552

#### Patrick Massot (May 23 2019 at 19:37):

I think that it would be best if the foundations of manifolds used sheaves explicitly. If you don't do it explicitly then I think you end up duplicating a lot of the ideas anyway. Many of the most popular manifolds are algebraic varieties, and you make the interface with algebraic geometry much smoother if you use similar foundations. In that context, germs become very natural.

We should have a FAQ dedicated only to this question. This is an old algebraic geometry people fantasy relying on no mathematical content as far as we've seen. Pretending to define smooth manifold as ringed spaces only adds definitions without buying anything, and then the idea stops completely as soon as you want extra structure on your manifold.

#### Neil Strickland (May 23 2019 at 20:17):

What extra structure do you have in mind? You can certainly do vector bundles, tangent bundles, metrics, symplectic structures, connections, curvature, exterior derivatives, almost complex structures very naturally from the ringed space viewpoint.

#### Sebastien Gouezel (May 23 2019 at 21:02):

Triangulations. Flows. Much of Riemannian geometry (for instance geodesic flow or Jacobi fields). Connected sums. Knots and surgery. Open book structure in contact manifolds. Thurston's `(G,X)`

structures. PDEs. Perelman's geometrization theorem (yes, we're aiming high :). And many other things that a true differential geometer would know much better than me (I am more into dynamical systems and probability theory).

Understand me well: I am not saying that none of this can be formalized in terms of ringed spaces. However, when doing anything about these concepts I think it would only come in the way and make things more complicated to state and prove.

#### Scott Morrison (May 23 2019 at 22:04):

There's also the pragmatic point that there are no written sources for anything on Sebastien's list written using the "locally ringed space foundations".

#### Reid Barton (May 23 2019 at 22:07):

I mean, ideally one's foundations should become irrelevant at some stage of the development, though I don't know whether this is going to be the case for everything on Sebastien's list.

#### Reid Barton (May 23 2019 at 22:11):

Well, I guess the main point is that eventually one will want to have the description in terms of atlases regardless of whether it is chosen as the definition or not.

#### Kevin Buzzard (May 24 2019 at 06:10):

This post is beginning to read like my Langlands brain dump from earlier this week. Can we get it into an issue somehow? That would rely on fleshing some of the ideas out

#### Patrick Massot (May 24 2019 at 06:46):

What extra structure do you have in mind? You can certainly do vector bundles, tangent bundles, metrics, symplectic structures, connections, curvature, exterior derivatives, almost complex structures very naturally from the ringed space viewpoint.

Do you mean: you can define manifolds as ringed space then derive existence of atlases and do everything naturally from there? If not then could you elaborate? Let's go for simpler stuff. What is your ringed definition of manifolds with boundary for instance?

#### Johan Commelin (May 24 2019 at 06:55):

I've never used manifolds with boundary, so I don't know exactly how functions on them are supposed to behave. But I'll take a stab:

A manifold with boundary of dimension $n$ is a locally ringed space $(X, \mathcal{O})$, such that: there exists an open set $U$ with the properties

- for every point $x \in U$ there is an open neighbourhood $U_x$ such that the induced LRS $(U_x, \mathcal{O}|_{U_x})$ is isomorphic (as LRS) to the standard open $n$-ball with the sheaf of $C^k$ functions on it;
- for every point $x \notin U$, there is an open neighbourhood $U_x$ such that the induced LRS $(U_x, \mathcal{O}|_{U_x})$ is isomorphic (as LRS) to the standard half $n$-ball with the sheaf of $C^k$ functions on it.

#### Patrick Massot (May 24 2019 at 06:58):

And what is the boundary then?

#### Johan Commelin (May 24 2019 at 06:59):

The interior consists of all points that have an open neighbourhood isomorphic to the standard open $n$-ball. The boundary is the complement of the interior.

#### Johan Commelin (May 24 2019 at 06:59):

Or do you mean that you want the boundary as LRS?

#### Johan Commelin (May 24 2019 at 07:01):

I guess you can take the induced reduced LRS structure on the closed subset.

#### Patrick Massot (May 24 2019 at 07:03):

I mean how do you recognize the interior using only the sheaf?

#### Johan Commelin (May 24 2019 at 07:04):

What I just said: it's the subspace of points that have a neighbourhood isomorphic to the standard open $n$-ball.

#### Patrick Massot (May 24 2019 at 07:05):

Hint: a function $f$ on the half $n$-ball is $C^k$ at $x$ is there is an open neighborhood $U$ of $x$ in $\mathbb{R}^n$ and a function from $U$ to $\mathbb{R}$ which restricts to $f$

#### Patrick Massot (May 24 2019 at 07:06):

What you define is everything

#### Patrick Massot (May 24 2019 at 07:06):

I think

#### Patrick Massot (May 24 2019 at 07:07):

Hmm, maybe you're saved by topology

#### Johan Commelin (May 24 2019 at 07:07):

Hmm, maybe you're saved by topology

Yup, that was my guess.

#### Patrick Massot (May 24 2019 at 07:08):

The sheaf is useless but the half ball is not homeomorphic to a full ball

#### Patrick Massot (May 24 2019 at 07:08):

That won't save you for manifolds with corners

#### Johan Commelin (May 24 2019 at 07:08):

What is a manifold with corners?

#### Patrick Massot (May 24 2019 at 07:08):

Locally modeled on a product of lines and closed half lines

#### Patrick Massot (May 24 2019 at 07:09):

Eg. $[0, 1]^2$

#### Johan Commelin (May 24 2019 at 07:09):

Locally modeled on a product of lines and closed half lines

This sounds suspiciously close to a LRS definition.

#### Patrick Massot (May 24 2019 at 07:10):

The corners are topologically impossible to distinguish from the codimension 1 strata of the boundary, and functions won't help you

#### Patrick Massot (May 24 2019 at 07:10):

This sounds suspiciously close to an atlas deifnition

#### Neil Strickland (May 24 2019 at 07:10):

I mean that:

1. Points of an open set `U`

biject with homomorphisms `C^∞(U,ℝ) → ℝ`

of `ℝ`

-algebras

2. Vector bundles are the same as locally free modules over the structure sheaf. Fibres can be recovered by tensoring with characters as in 1.

3. Vector fields are `ℝ`

-linear derivations, and individual tangent vectors are derivations with respect to a character as in 1.

4. The module of one-form fields is dual to the module of vector fields. The full de Rham complex is the exterior algebra of the one-form fields over the structure sheaf.

5. Connections on a vector bundle are actions of the Lie algebra of vector fields on the module of sections

And so on.

You can make all these definitions in a fairly straightforward and uniform way for any `ℝ`

-algebra, and thus for sheaves of `ℝ`

-algebras. You can prove properties for the sheaf of smooth functions on `ℝⁿ`

, and deduce that they also hold for any ringed space that is locally isomorphic to that, which is the definition of a manifold.

#### Johan Commelin (May 24 2019 at 07:11):

The corners are topologically impossible to distinguish from the codimension 1 strata of the boundary, and functions won't help you

So we define it as a stratified LRS...

#### Johan Commelin (May 24 2019 at 07:13):

It seems to me that the atlas definition also needs extra data. The strata are part of the data, right?

#### Patrick Massot (May 24 2019 at 07:13):

No they are not

#### Johan Commelin (May 24 2019 at 07:13):

Hmm, ok

#### Patrick Massot (May 24 2019 at 07:13):

A diffeomorphism won't send a half plane to a quarter of plane

#### Patrick Massot (May 24 2019 at 07:15):

And of course none of this will bring you $(G, X)$-structures (for instance manifolds equipped with an atlas whose coordinate changes are in a given subgroup of $GL(n, \mathbb{R})$)

#### Patrick Massot (May 24 2019 at 07:17):

Neil, I'm sure you know this is all a joke. How can you hope to prove anything without reducing to the usual definitions? For instance, how to you equip $TM$ with a manifold structure and prove $TM \to M$ is a submersion?

#### Patrick Massot (May 24 2019 at 07:19):

Anyway, I should go and mark exams instead of feeding trolls

#### Neil Strickland (May 24 2019 at 07:28):

You certainly need to reduce things to properties of smooth functions on `ℝⁿ`

. The only question is how to organise reduction to local properties. Standard books on differential geometry typically do not do this in a very thorough way that would be suitable for formalisation. If you try to fill in the details, you will end up recreating a lot of sheaf-theoretic stuff. In my opinion, it would be more efficient to build a decent library of sheaf theory, which will be needed for other reasons anyway, and use that explicitly.

#### Andrew Ashworth (Jul 25 2019 at 21:05):

@Kevin Buzzard I saw your MathOverflow post on manifolds did not have an answer, and coincidentally I was browsing through the archive of formal proof today and saw this: https://www.isa-afp.org/entries/Smooth_Manifolds.html. I have not had the time to read the paper so I do not know how much it overlaps with current efforts, but I thought I'd mention it.

#### Andrew Ashworth (Jul 25 2019 at 21:15):

Hah, in the paper the authors wrote (http://home.in.tum.de/~immler/documents/immler2018manifolds.pdf) they complain about simple type theory and ambiguous math textbooks.

#### Kevin Buzzard (Jul 25 2019 at 21:20):

Post a response!

#### Johan Commelin (Oct 24 2019 at 13:43):

@Sebastien Gouezel How far are we from defining a manifold structure on projective space?

- Define projective space as a type. (Can be done for any field. Should later be connected to rational points of a scheme.)
- Setup the coordinate charts
- In the case that the base field is
`ℝ`

or`ℂ`

, show that the coordinate changes belong to suitable groupoids. - Done?

#### Sebastien Gouezel (Oct 24 2019 at 14:39):

Yes, that's it. All of this should be pretty straightforward, at least if you use the naive version of projective space, i.e., quotient a finite dimensional vector space minus 0 by scalar multiplication. Even more straightforward would be to do it over the vector space `fin (n+1) -> K`

, where one could use the standard `n+1`

affine charts.

#### Johan Commelin (Oct 24 2019 at 14:41):

Yes, that's what I was thinking of.

#### Johan Commelin (Oct 24 2019 at 14:42):

Are you working on things like open submanifolds, submersions, closed submanifolds defined by a regular value of a structomorphism, etc...?

#### Johan Commelin (Oct 24 2019 at 14:44):

Basically, I think I'm asking: what's the table of contents for your future PRs?

#### Kenny Lau (Oct 24 2019 at 14:56):

KP^n is a special case of Gr(n,k)

#### Johan Commelin (Oct 24 2019 at 14:58):

There are too many special cases here...

#### Johan Commelin (Oct 24 2019 at 14:58):

It's also a special case of a weighted projective space

#### Kevin Buzzard (Oct 24 2019 at 15:19):

it's also a special case of a projective variety

#### Reid Barton (Oct 24 2019 at 15:20):

Come on! This is about manifolds. It's clearly a special case of a symmetric space

#### Johan Commelin (Oct 24 2019 at 15:24):

Exactly... and my reflex is therefore to not make any examples at all... They are always to specific

#### Johan Commelin (Oct 24 2019 at 15:24):

But I think we need examples at some point.

#### Kevin Buzzard (Oct 24 2019 at 17:10):

https://github.com/leanprover-community/lean-perfectoid-spaces/tree/master/src/examples

#### Kevin Buzzard (Oct 24 2019 at 17:11):

I think Kenny at some point tried to make projective n-space as a scheme and failed---maybe it was even projective 1-space? We had to glue schemes, which meant we had to glue sheaves, and then we started down some rabbithole...

#### Kenny Lau (Oct 24 2019 at 17:12):

yeah I became lost in definition unfolding

#### Sebastien Gouezel (Oct 24 2019 at 17:43):

I am a little bit tired of definitions, so I think I will start proving a theorem, and see along the way which definitions I need. I would like to prove that an `n`

-dimensional real manifold embeds into `R^{2n+1}`

. This requires a partition of unity to embed it first in `R^N`

for some large `N`

, and then Sard theorem to decrease progressively the dimension by projecting along a typical direction and keeping an embedding. Given the amount of prerequisites, I expect this to be a long-term project :)

#### Johan Commelin (Oct 24 2019 at 18:32):

Is the `2n+1`

"useful"? Of course it is nice to know. But isn't the `N`

-version good enough for all practical purposes? I am really quite ignorant about these things...

#### Johan Commelin (Oct 24 2019 at 18:33):

Another nice long term goal (from my POV) would be Chow's theorem (closed analytic in P^n => algebraic). But maybe we should do some complex analysis first :lol:

#### Sebastien Gouezel (Oct 24 2019 at 18:41):

The `2n+1`

is nice, although not optimal: one can do `2n`

, and even `2n-1`

when `n`

is not a power of two (but this is much more difficult). But what is really interesting is the proof, as it involves several tools that are really important.

#### Sebastien Gouezel (Oct 24 2019 at 19:35):

Just for the fun: do you know the smallest dimension `N(n)`

such that any `n`

-dimensional manifold can be immersed in `R^N`

?

#### Sebastien Gouezel (Oct 24 2019 at 19:36):

It is `N(n) = 2n-a(n)`

, where `a(n)`

is the number of ones in the base-2 expansion of `n`

...

#### Johan Commelin (Oct 24 2019 at 19:39):

... lol, nice.

#### Mario Carneiro (Oct 25 2019 at 00:12):

do you know a 3D manifold that doesn't fit in 4D?

#### Mario Carneiro (Oct 25 2019 at 00:13):

oh, I guess that's covered by your more precise statement about `2n-a(n)`

#### Kevin Buzzard (Oct 25 2019 at 07:21):

It is

`N(n) = 2n-a(n)`

, where`a(n)`

is the number of ones in the base-2 expansion of`n`

...

I don't see how you can immerse S^1 in R :P

#### Sebastien Gouezel (Oct 25 2019 at 09:25):

I could edit my message to add the assumption `n > 1`

(I wish we could also do that for published papers :), but it is more honest to add it just now. So, standing assumption: `n > 1`

. And I just checked the paper, there is also a compactness assumption by the way.

#### David Michael Roberts (Oct 27 2019 at 22:21):

A similar thing happens for proper holomorphic embedding of Stein manifolds (i.e. complex manifolds with sufficiently many nontrivial C-valued functions, more or less) into affine C^n. The case of open Riemann surfaces is a special case where we don't know if we can drop one more dimension in the target to match the uniform formula that works for all dimensions \geq 2. We know we can put them in C^3, the formula suggests C^2, though there are no counterexamples known.

#### Johan Commelin (Dec 11 2019 at 08:15):

I am a little bit tired of definitions, so I think I will start proving a theorem, and see along the way which definitions I need. I would like to prove that an

`n`

-dimensional real manifold embeds into`R^{2n+1}`

. This requires a partition of unity to embed it first in`R^N`

for some large`N`

, and then Sard theorem to decrease progressively the dimension by projecting along a typical direction and keeping an embedding. Given the amount of prerequisites, I expect this to be a long-term project :)

@Sebastien Gouezel It just occurred to me that we are also getting towards a situation where we can *state* some form of Stokes' theorem. Does anyone know of a formalization of Stokes' theorem? The best I could find was an MSc project in Edinburgh that started working on it: http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=E6816A068653DFB139039B8F47C180AC?doi=10.1.1.64.7036&rep=rep1&type=pdf But I don't think they actually managed to get to Stokes' theorem.

#### Sebastien Gouezel (Dec 11 2019 at 08:50):

You have https://www.isa-afp.org/entries/Green.html for the 2-dimensional version, but I don't know of a general version. I think we are still pretty far in Lean: first one would need material of linear algebra on alternating forms, and then define differential forms and their integrals. Once one can state the theorem, I think proving it will not be hard (it just boils down to: use a partition of unity to reduce it to the half-space in `R^d`

, and then integrate by parts in the vertical direction).

#### Johan Commelin (Dec 11 2019 at 08:55):

I agree that we aren't ready to do it right away. But it might be a nice goal to work towards

#### Johan Commelin (Dec 11 2019 at 08:55):

It seems that you are currently moving towards partition of unity

#### Sebastien Gouezel (Dec 11 2019 at 09:17):

It's definitely a nice middle-term goal, yes.

Last updated: May 10 2021 at 07:15 UTC