topology and analysis

Stream: general

[Patrick Massot]

This is a mathlib organization question. I had in mind that the analysis folder import topology but not the other way around. However I just noticed that topology.metric_space.isometry import normed group. Is that intentional? Actually there are other examples. Should we try to fix that? @Sebastien Gouezel

[Heather Macbeth]

There are some other examples, for example topology.continuous_function.bounded imports normed_group.

[Heather Macbeth]

Like Patrick, I would be mildly in favour of changing it so that it only went topology -> analysis.

[Heather Macbeth]

Another example: topology.metric_space.pi_Lp.

[Heather Macbeth]

That actually indirectly imports much of measure theory!

[Patrick Massot]

The case of pi_Lp is extremely easy to settle. This file is never used by any other file in the topology folder, it can move straight to the analysis folder.
piLp.pdf

[Kevin Buzzard]

A genuine question from a non-computing-expert: why does it matter if files in one directory do or don't import files in another directory?

[Patrick Massot]

The file continuous_function.bounded could rather easy because it seems already cleanly split between a first half which is about metric spaces and a second half about normed spaces. We can simply move the second half to a new file in the analysis folder. But the real question is files depending on that one, and there are a lot : bounded.pdf. If we are lucky then those file that are in the topology folder use only the first part.

[Patrick Massot]

Kevin, there are two separate issue. The first one is users searching mathlib. The second one is compilation time. If the import structure of mathlib is completely random then any modification triggers recompilation of a huge part of mathlib.

[Patrick Massot]

Maybe I'll try to fix all this tonight. A much more ambitious fix would be to get the measure theory folder to be independent of topology and analysis, and again move everything from measure theory that depends on topology or analysis to analysis. But this is maybe more debatable from a mathematical point of view, and the measure theory folder is a giant mess anyway.

[Mario Carneiro]

Patrick Massot said:

Kevin, there are two separate issue. The first one is users searching mathlib. The second one is compilation time. If the import structure of mathlib is completely random then any modification triggers recompilation of a huge part of mathlib.

The compilation time issue is only a problem for unnecessary imports at the file level. Moving a file from one folder to another should not affect compilation time.

[Patrick Massot]

Sure, I was talking about the splitting case.

[Patrick Massot]

If you split continuous_function.bounded into a metric space part and a normed space part then modifying normed_space.basic won't recompile half of the topology folder.

[Sebastien Gouezel]

I'm definitely on board with splitting files to get more fine-grained recompilation. I don't see how we could make sure that topology never imports analysis, though: there will be topological results whose proofs will use analytic tools.

As for measure theory, the integral uses L^1, which is a particular case of L^p, which requires real powers and convexity inequalities, which requires a good deal of analysis. And conversely many results in analysis will use integration (I have in the works a proof that the second derivative is symmetric, which requires nonintrivial integration results). So disentangling things when it is reasonable is absolutely a good idea, but we have to know that this won't always be possible.

[Patrick Massot]

What do you have in mind as a topological result using analysis? For integration I agree it's much more tricky (as I already wrote before). The extreme view would be to put all of integration into analysis, leaving only measure theory in measure_theory, but I agree I wouldn't expect to see this.

[Sebastien Gouezel]

To take an extreme example: the classification of compact (oritentable, boundaryless) surfaces through the genus, which is a purely topological statement but whose proof could use de Rham cohomology or Morse functions or whatever, deeply rooted in analysis.

[Heather Macbeth]

Sebastien Gouezel said:

To take an extreme example: the classification of compact (oritentable, boundaryless) surfaces through the genus, which is a purely topological statement but whose proof could use de Rham cohomology or Morse functions or whatever, deeply rooted in analysis.

I would maybe make a separate "differential topology" folder for such results -- at least, I think that's how it's organized in my head. But I don't feel very strongly about it.

[Adam Topaz]

Just wait until we want to calculate the etale fundamental group of $\mathbb{P}^1 - \{0,1,\infty\}$

[Kevin Buzzard]

I would really like a big push on this sort of thing but I always have this July 2022 ICM deadline in mind and I think the top priority should really be finishing the Scholze job. However that will force us to have a usable sheaves on sites setup so perhaps at least the definition of etale fundamental groups will also follow

[Adam Topaz]

I mentioned the etale fundamental group of P^1 - {0,1,infty} in this thread because the usual proof is to use the Riemann existence theorem. It's really a nontrivial combination of analysis, topology, algebraic geometry and category theory to prove that this fundamental group is the free profinite group on 2 letters. I have no idea what folder of mathlib that would go in ;)

[Adam Topaz]

Also to my knowledge there is no known purely algebraic proof of this fact.

[Kevin Buzzard]

It would be a great long term project and it would emphasize the importance of the monorepo approach

[Patrick Massot]

Sebastien Gouezel said:

To take an extreme example: the classification of compact (oritentable, boundaryless) surfaces through the genus, which is a purely topological statement but whose proof could use de Rham cohomology or Morse functions or whatever, deeply rooted in analysis.

This is not a serious objection. Such a proof would clearly be in a differential topology folder, even if you somehow manage to state it in elementary terms (which is not so easy because you need to describe models).

[Sebastien Gouezel]

What about the Jordan curve theorem, then, which is a purely topological statement but that you will have a hard time proving without ever mentioning normed space?

[Kevin Buzzard]

Aah but this is clearly a theorem about analysis because it mentions $\R$ :-) Similarly for the proof that $\pi_4(S^3)=\Z/2$ :-)

[Sebastien Gouezel]

I mean, I don't really see the point in trying to separate completely stuff. Mathematics is interwoven in all directions (and that's part of what makes it so fun). These higher level directories seem useful to me when you want to say that a statement belongs mainly to some field, but it should be expected that proofs will borrow tools from everywhere else.

[Eric Rodriguez]

For sure, but if we can put it into little boxes it ends up being really useful programming-wise

[Sebastien Gouezel]

Note that I'm completely onboard with trying to minimize imports, and to break files into smaller files when it helps getting clear cut dependencies. So, putting things into little boxes when it can be done naturally, yes, sure. But trying to jump through weird hoops when it can't be done naturally and we want to force some artificial organization onto something which is naturally not tree-like, not so much.

[Patrick Massot]

I don't think this discussion has anything to do with "programming-wise". And I think Jordan's theorem will be in an algebraic topology folder anyway. But that's not a very fruitful discussion.

[Kevin Buzzard]

The big theorems and ideas in mathematics often draw completely different fields together. For example the Langlands program is an attempt to unify certain questions in harmonic analysis and the representation theory of algebraic groups with the representation theory of Galois groups of fields which number theorists study like the rationals. Maybe it will have to have its own folder :-)

[Patrick Massot]

#7908 is another example that feels very wrong to me. Why do we need to pull the full manifold library into analysis/complex/isometry.lean?

[Patrick Massot]

@Heather Macbeth are you using more than this part that could clearly be somewhere else?

[Patrick Massot]

I also think it's very weird that circle means the group of unit complex number rather than any geometric circle in a Euclidean plane.

[Yaël Dillies]

unit_circle would sound like a good name to me.

[Patrick Massot]

I think circle_group is even better if you want to keep the word circle. Here the emphasis is really on the group structure.

[Patrick Massot]

I understand it's not called $U(1)$ or $SO_2(\mathbb{R})$ because this would cause conflict with the general case.

[Patrick Massot]

Although you'd have a hard time convincing a mathematician there is any difference between $U(1)$ and this.

[Heather Macbeth]

@Patrick Massot Indeed, I was planning a follow-up PR to split the circle file.

[Heather Macbeth]

Sébastien and I discussed whether to split the circle file in several pieces when I first PR'd it (#6907). At the time it seemed less necessary, but now that there are a couple of other things depending on just the topological group structure (#6952, #7908) I was thinking it would be better to have the topological group structure in a separate file, say analysis.complex.circle.

[Heather Macbeth]

Patrick Massot said:

Although you'd have a hard time convincing a mathematician there is any difference between $U(1)$ and this.

The difference is that circle is constructed as a subtype and submonoid and topological subspace of ℂ, whereas $U(1)$ is ℂ ≃ᵢ[ℂ] ℂ. In Lean they should be isomorphic objects but not literally equal.

[Patrick Massot]

I understand this. When I try really hard I can even tell the difference between scalars and 1x1 matrices.

[Heather Macbeth]

Heather Macbeth said:

Patrick Massot Indeed, I was planning a follow-up PR to split the circle file.

#7951

[Sebastien Gouezel]

Patrick Massot said:

The case of pi_Lp is extremely easy to settle. This file is never used by any other file in the topology folder, it can move straight to the analysis folder.

There were two examples that clearly needed fixing to have a more reasonable import graph. See #7990 and #7991. (Of course this is just a small contribution to improving the state of the import graph!)

[Heather Macbeth]

Patrick Massot said:

This is a mathlib organization question. I had in mind that the analysis folder import topology but not the other way around. However I just noticed that topology.metric_space.isometry import normed group. Is that intentional? Actually there are other examples. Should we try to fix that? Sebastien Gouezel

@Patrick Massot I experimented with swapping this, so that analysis.normed_group.basic imports topology.metric_space.isometry.
https://github.com/leanprover-community/mathlib/compare/move-isometry

The beneficiaries are

• topology.algebra.normed_group (a short file about completions recently written by @Johan Commelin), which can be combined into analysis.normed_space.basic
• topology.metric_space.completion, topology.metric_space.gluing, which no longer import normed group

Is this worth implementing in mathlib?

[Johan Commelin]

The second point definitely seems like a good idea :thumbs_up:

[Johan Commelin]

(And the first one is a nice bonus :smiley:)

[Yaël Dillies]

I'm grabbing a book about locally convex spaces sometimes soon, so maybe leave some space for such a new file (which will be inserted just before analysis.normed_space.basic, I think).

[Matt Kempster]

Would it be worth it to expand the linter to flag warnings when wrong-directional imports are created within a PR? This sort of thing generally comes out during a PR review process, but reviewers might miss it, and it can save time regardless.

[Matt Kempster]

Of course, we'd have to define and maintain "wrong-directional" boundaries, while avoiding worrying about really obvious ones.