upper half plane topology

Stream: mathlib4

[Johan Commelin]

See https://leanprover-community.github.io/mathlib-port-status/file/analysis/complex/upper_half_plane/topology

To what extent is the dependency on the manifold library essential? This file is what connects the zeta function to the manifold library.

[Johan Commelin]

Aha, https://tqft.net/mathlib4/2023-06-22/all suggests that a refactor could solve this.

[Yury G. Kudryashov]

This file didn't depend on manifolds when I wrote it.

[Yury G. Kudryashov]

(AFAIR)

[Yury G. Kudryashov]

Indeed, the dependency was added by @David Loeffler in !3#18631

[Yury G. Kudryashov]

I think that the lines added in that commit should be moved to a new file (say, upper_half_plane.manifold) with 'Authors: David Loeffler'

[Ruben Van de Velde]

I mentioned this a while back, but there was little appetite for a split then. Can't find it now on mobile

[David Loeffler]

I didn't write those lines, I just moved them (they were originally somewhere in the modular_forms directory). It hardly seems worth doing a split for ease of porting when the port is so close to completion anyway.

[Yury G. Kudryashov]

I think that topology on the upper half-plane should not depend on advanced topics like derivatives.

[Yury G. Kudryashov]

In fact, I would split the code about action from basic but now it should wait till after the port.

[Kevin Buzzard]

I'm not sure I see the logic (but I'm not arguing against it). Our original proof of quadratic reciprocity did not depend on advanced topics like Gauss sums and the complex numbers (it was just counting integer points in a rectangle in a clever way), but our current proof does. Does this also bother you? I'm not sure I care at all.

[David Loeffler]

I'm not sure I see the logic either, and I am going to argue against it, on the following grounds: if you split upper_half_plane.topology in half, then how many files are going to import just the first half?

As far as I'm aware there are basically no mathematically interesting structures you can build around the upper half-plane without knowing it's a manifold. (There aren't that many files in mathlib right now which use the differentiable structure on H, but that's not because it isn't important, it's because modular forms in mathlib are still at a very early stage of development.)

[David Loeffler]

For example, if you fork off the differentiable structure into upper_half_plane.manifold, then that file is still going to have to be imported by jacobi_theta, because otherwise it's impossible to state the fact that the theta function is differentiable (which is part of what makes it a modular form).

[Kevin Buzzard]

So basically the observation is that the file can be split (which would make the topology not depend on calculus) but it's not going to make the port any easier.

[Patrick Massot]

David Loeffler said:

As far as I'm aware there are basically no mathematically interesting structures you can build around the upper half-plane without knowing it's a manifold.

Did you try saying this out loud?

[Patrick Massot]

Hint: I heard Gauss and Jacobi died almost one century before differentiable manifolds were actually defined.

[David Loeffler]

@Patrick Massot Two comments:

• Firstly, this historical analogy makes no sense, because the ordering of topics in mathlib does not follow historical evolution of the subject. One of Gauss's most famous discoveries was the divergence theorem; yet the versions of the divergence theorem we have in mathlib require Lebesgue integrals, despite the fact that Gauss died long before Lebesgue was born. So what's your point?

• Secondly, I don't appreciate the jeering tone of your reply. If you follow your own advice to read your message out loud, perhaps you'll realise that it falls well below the standard of civility normally expected on this forum.

[Yury G. Kudryashov]

About importing topology without manifolds: e.g., you can define metric and do "basic" Lobachevsky geometry without the manifold structure.

[Yury G. Kudryashov]

E.g., Mathlib.Algebra.Group is not a single file.

[Yury G. Kudryashov]

(it used to be)

[Yury G. Kudryashov]

And you can have jacobi_theta.basic and jacobi_theta.manifold.

[Yury G. Kudryashov]

One more example: you can prove the Riemann mapping theorem (for the unit disc or for the upper half-plane) without ever saying the word "manifold".

[Yury G. Kudryashov]

One more reason to split: if this file appears on the longest import chain, then splitting it will slightly speed up every CI run on a commit that modifies a file deep down the import hierarchy.

[Johan Commelin]

Kevin Buzzard said:

I'm not sure I see the logic (but I'm not arguing against it). Our original proof of quadratic reciprocity did not depend on advanced topics like Gauss sums and the complex numbers (it was just counting integer points in a rectangle in a clever way), but our current proof does. Does this also bother you? I'm not sure I care at all.

I don't really care either. But I do notice that porting the manifold stuff is probably going to be 1 of the two rough patches left for the port, the other being AG. I wouldn't mind if the files regarding zeta could be ported independently of that.

I know that the port is close to being finished. But it isn't finished yet. I still think this split could be helpful, even if only temporarily.

[Yury G. Kudryashov]

Kevin Buzzard said:

I'm not sure I see the logic (but I'm not arguing against it). Our original proof of quadratic reciprocity did not depend on advanced topics like Gauss sums and the complex numbers (it was just counting integer points in a rectangle in a clever way), but our current proof does. Does this also bother you? I'm not sure I care at all.

I do not suggest to change any proof, just to move the code around.

[David Loeffler]

FWIW, the entire modular-forms library could have been developed without mentioning manifolds (and this is the way that elementary modular forms texts do it; I'm pretty sure the word "manifold" does not appear anywhere in Serre's "Course in arithmetic"). Given a function f on H (which is by definition a subtype of C), you can define "differentiability" by equipping H with a manifold structure (as we do), or you can extend f arbitrarily to C and ask that it be differentiable_on the subset of C underlying H. As it happens we've gone with the first option, but the second would also have worked.

[Yury G. Kudryashov]

Again, splitting the file doesn't mean that we'll change any definition or a proof.

[Patrick Massot]

David, my comment was not meant to be taken too seriously, just as I assumed your claim wasn't meant to be read too seriously. As you noted, one can define differentiable functions on the upper half-space without manifold theory (both in the real world and in mathlib).

[David Loeffler]

David, my comment was not meant to be taken too seriously, just as I assumed your claim wasn't meant to be read too seriously

The difference is that my comment was not insulting.

[Johan Commelin]

I think it is possible to read Patrick's comment in a joking tone, in which it wouldn't come across as insulting to me.

[Jireh Loreaux]

FWIW, I initially read it with David's interpretation, but then thought about Patrick's disposition, realized that's not the way he intended it, and then reread it with the intended tone. Hence I didn't add a :butterfly:

[Yury G. Kudryashov]

As a person who had a big argument over e-mail, then found out the only reason was misunderstanding of the tone (by both side) and what each side thought was (un)important in the messages, I suggest that you try to avoid deeping the conflict without talking face to face.

[Patrick Massot]

I swear I really laughed when reading that "As far as I'm aware there are basically no mathematically interesting structures you can build around the upper half-plane without knowing it's a manifold." and indeed I was still smiling while writing me comment, not insulting anyone. I was assuming, and still assume, that David knows there are mathematically interesting structures on the upper half plane that do not require manifold theory. So for me the whole context of that discussion was indeed a joke.

[David Loeffler]

Again, splitting the file doesn't mean that we'll change any definition or a proof.

I initially didn't think this would work, but I've rechecked the code and realised it probably would. I had forgotten that the differentiability statement for jacobi_theta is given in two distinct formulations (one elementary and one using manifolds), and it is only the elementary formulation which is used in zeta_function, so it can indeed be factored off. I can make a mathlib3 PR for this tomorrow, unless someone else wants to do the honours first.

[Yury G. Kudryashov]

Just to clarify: I think that we should split this file even if all files about modular forms will import the manifold one.

[Yury G. Kudryashov]

I'm trying to split it now.

[Yury G. Kudryashov]

BTW, why didn't the "repeated namespace" linter report docs#upper_half_plane.upper_half_plane.charted_space ?

[Johan Commelin]

@David Loeffler Just a random bit of info to help you for this specific instance of spelunking: https://tqft.net/mathlib4/2023-06-23/all tells us that no decleration in the zeta file depends on anything in the manifold files. Hence all the - in front of those files.

[Ruben Van de Velde]

Ruben Van de Velde said:

port-progress bot said:

mathlib port progress	number_theory.zeta_function
Unported files:	53/1252	(95.8% of total)
Unported lines:	29183/557043	(94.8% of total)
Longest unported chain:	11/116	(90.5% progress)

Hmm, seems like number_theory.modular_forms.jacobi_theta pulls in a bunch of manifold stuff for the one lemma mdifferentiable_jacobi_theta. Not sure if that's worth changing

fwiw, this was the previous (much shorter) conversation

[Yury G. Kudryashov]

!3#19212

[Yury G. Kudryashov]

BTW, the "manifold" files are small because they are not yet used by anybody.

[Yury G. Kudryashov]

Once you will use them, you will add lemmas like "if a function is differentiable on {z | 0 < im z}, then it is mdifferentiable on the upper_half_plane etc.

[Yury G. Kudryashov]

Also, you will want lemmas about mfderiv of functions to/from the upper_half_plane in terms of fderiv/deriv.

[Yury G. Kudryashov]

Many of these lemmas will be rfl.

[Yury G. Kudryashov]

I made 1 change besides moving the code around: used =O notation instead of is_O.

[Alex J. Best]

Yury G. Kudryashov said:

BTW, why didn't the "repeated namespace" linter report docs#upper_half_plane.upper_half_plane.charted_space ?

because it skips instances, I'm not sure why, perhaps too many annoying autogenerated names to fix