Formalization of Riemann Mapping Theorem

Stream: mathlib4

[Dattabhasvant Ghadiyaram]

I hope this is the right channel to post.
As a course project, I am planning to work on the formalization of some important theorems in complex analysis. The Riemann Mapping Theorem was my first idea. Could I get some guidance on how to get started and how to contribute this to mathlib?

[Junyan Xu]

It's done by @Vincent Beffara in https://github.com/vbeffara/RMT4 (apparently no sorry remains in the repo)

[Dattabhasvant Ghadiyaram]

Thank you! Do you have suggestions for what else I could work on?

[Kevin Buzzard]

That work hasn't been contributed to mathlib so will become unusable over time. It's on lean v4.7.0 so already ten versions behind. I bet it doesn't even compile with today's mathlib. One way of helping the community would be by helping to PR the results to mathlib.

If this doesn't appeal then a couple of things on my list are: compact Riemann surfaces and the fact that any nonconstant map between them has a degree, and the Weierstrass P-function (which I need for FLT; the details of what exactly I need are here ). I was taught both of these things as an undergraduate but they're not in mathlib.

[Ruben Van de Velde]

I might look at updating RMT4 to a more recent mathlib later

[Dattabhasvant Ghadiyaram]

Thanks @Kevin Buzzard ! I will check out both of them!

[Ruben Van de Velde]

Wasn't too bad: https://github.com/vbeffara/RMT4/pull/1

[Kevin Buzzard]

@Vincent Beffara do you have any plans to get this stuff into mathlib? I think RMT would be a great result to have! Stuff which doesn't make it into mathlib just rots. Ruben said "wasn't too bad" but it's 14 files changed and 161 lines of fixes, and if people don't keep keeping it alive then eventually it will just sink.

[Michael Rothgang]

Ruben Van de Velde said:

Wasn't too bad: https://github.com/vbeffara/RMT4/pull/1

I looked through the diff: looks good to me. (I don't have merge right, of course.)

[Junyan Xu]

do you have any plans to get this stuff into mathlib?

I think #20873 is supposed to be one of those PRs and I reviewed it, but there's a stronger version of a result in the PR that I've proven previously but the PR's approach can't (yet) prove, so it's currently stuck. I should take some time to understand why it's difficult with this approach ...

[Ruben Van de Velde]

I don't have an opinion on what's a good approach here, but I'm not sure a WIP PR that hasn't been touched for over a year should block landing other work

[Kim Morrison]

I'm sure a WIP PR that hasn't been touched for less than a year should not block landing other work. :-)

[Kim Morrison]

It's really important that we don't let work sitting in other repos inhibit people from getting it into Mathlib or other maintained repos, even if it is at the cost of duplicating work.

[Ruben Van de Velde]

Sure, but the fastest path to getting a proof into mathlib is likely "submit the existing proof", not "start from scratch"

[Junyan Xu]

I've extracted the part of the WIP PR #10084 that is ready into #22649

[Johan Commelin]

Great! But it needs a shake and some docstrings.

[Junyan Xu]

I added IsCoveringMap.existsUnique_continuousMap_lifts to #22649 which allows to lift a continuous map from an arbitrary simply-connected, locally path-connected space through a covering map. (Taking the space to be the unit interval, we recover path lifting.) This can be directly used to define a branch of the square root of a nowhere vanishing function on a simply-connected domain, but maybe @Vincent Beffara's proof of RMT requires more.

[Johan Commelin]

This is very nice!