Riemann Mapping Theorem

Stream: Is there code for X?

[Vincent Beffara]

Hi, is there work going on about proving some version of the Riemann Mapping Theorem? @Kalle Kytölä and myself are interested in giving it a try but it would be bad to duplicate existing effort...

[Sebastien Gouezel]

Not as far as I know. @Yury G. Kudryashov , are you working on this?
(And also, what version are you thinking of? Connected and simply connected one-dimensional complex manifolds are isomorphic to the sphere, the plane or the disk -- or just the version for subsets of the complex plane?)

[Vincent Beffara]

For the moment, proper domains of the complex plane in which non-vanishing holomorphic functions have a holomorphic square root, which is a way of bypassing homotopy theory while being equivalent to simple connectivity.

[Vincent Beffara]

Do we have the Riemann sphere somewhere btw?

[Sebastien Gouezel]

As a complex manifold, I doubt it.

[Yury G. Kudryashov]

I'm not working on this.

[Vincent Beffara]

Sebastien Gouezel said:

As a complex manifold, I doubt it.

One version here https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Working.20on.20the.20projective.20line/near/281612337 but there is a lot of work to be done on it still

[Junyan Xu]

Connected and simply connected one-dimensional complex manifolds are isomorphic to the sphere, the plane or the disk

This is called the uniformization theorem which was conjectured in 1882, while the Riemann mapping theorem was stated with a wrong proof by Riemann in 1851, according to Wikipedia. It's indeed a generalization of the latter though.

[Sebastien Gouezel]

Oh yes, I've never been good with names. But I know the theorems, for sure :-)

[Vincent Beffara]

That was also my understanding of the names. I also have the impression that many of the pieces are there to prove the RMT, but that the uniformization theorem is much further away...