Construction of the Riemann Sphere

Stream: maths

[Jeremy Feusi]

Hi!
So I recently got into Lean and decided to provide a construction of the Riemann sphere (as a smooth complex manifold) using quotient types (and finished doing so about 5 min ago!). Is this something you would be interested in incorporating into mathlib? I just thought I'd ask b.c. then I'd clean up my code a bit (at least I'll try my best, this is my first ever Lean project, so the code looks exactly like what happens when you give a random undergrad an IDE and tell him to type until it compiles :sweat_smile: ) and try to create a sensible PR.

[Kevin Buzzard]

We have rather few examples of mathematical objects in mathlib but we certainly need the sphere!

[Eric Wieser]

How different is with_top ℂ from the Riemann sphere?

[Alex J. Best]

Its equiv as a type, but with_top doesn't carry a topology, much less a complex manifold structure at present. docs#alexandroff is the one point compactification as a topological space at least

[Eric Wieser]

Are you suggesting alexandroff ℂ has the correct topology?

[Eric Wieser]

In which case that's a much better suggestion

[Jeremy Feusi]

@Kevin Buzzard Nice, sounds good! Well my original goal was actually to use it to define meromorphic functions since my kind of long term idea is to formalize the theory of branched covers of Riemann surfaces (with emphasis on "long term", Idk if you remember but I just asked you something like a week ago after you talk at ETH where I can find Riemann surfaces, so this is all still at the very beginning :sweat_smile: ). But I've changed plans and I currently think that the best way to define a function meromorphic at a point is a holomorphic function $f$ on a dotted neighbourhood together with an integer $e$ such that $z^e*f$ is bounded. This would play nicely with the removable singularity theorem and it becomes trivial to add and multiply meromorphic functions. But what do you guys think?

[Jeremy Feusi]

@Eric Wieser That's true, I didn't think of that! One benefit of doing it with quotient types is that it allows you to define a function out of the Riemann sphere by specifying it on the complement of 0 and on the complement of infinity and then showing that it agrees on the complement of both points which one doesn't have with alexandroff ℂ. Or is the gluing lemma formalized in such a way that we would get this from the charts?

[Kalle Kytölä]

Note that @Vincent Beffara constructed the Riemann sphere as the projective line $P^1 \mathbb{C}$ in this conversation.

[Kalle Kytölä]

I tend to think the topology is not the most tricky issue, the complex manifold structure already should be a better test of the design choice. But to me it seems the real test is whether the automorphism group of the Riemann sphere are the Möbius transformations (fractional linear transformations) $PSL(2,\mathbb{C})$. For this the projective line looks the most promising.

[Kalle Kytölä]

I didn't see the code of @Jeremy Feusi yet... What approach did you take?

[Kalle Kytölä]

Obviously constructing the Riemann sphere as a complex manifold is a great achievement, especially for someone who "recently got into Lean"! :speechless:

Congratulations @Jeremy Feusi! :tada:

[Jeremy Feusi]

Thanks! Yes, the topology in most cases will be the correct one. I was actually thinking about determining the automorphism group too, though as of right now I'm not sure what the best way to proceed is in my approach. So I didn't upload the code anywhere since it's rather a mess but if you'd like to see I could do so. The approach I took is to take the disjoint union of 2 copies of the complex plane and then glue them together like one does for $spec(k[X])$ in the general case.

[Jeremy Feusi]

I took a look at the conversation you mentioned and they seem to mention there, that that approach is obviously not the right one? Anyone have an idea what the problems are explicitly? Ah or wait, I think the discussion there was about projectivising vector spaces, right?

[Vincent Beffara]

Hi @Jeremy Feusi :wave:

[Vincent Beffara]

I chose to define the Riemann sphere from the projective line precisely because defining functions on it would be easier (since the projective line is defined as a quotient and we can use quotient.lift and friends for it).

[Vincent Beffara]

E.g. you can define projective coordinates,

local notation `[`x`:`y`, `h`]` := (mk _ (x,y) h)
local notation `[`x`:`y`]` := [x:y, by simp]

(where h is supposed to prove that (x,y) \ne (0,0)) and you can define

def lift_on {K V α : Type*} [field K] [add_comm_group V] [module K V]
  (z : ℙ K V) (f : {w : V // w ≠ 0} → α)
  (hf : ∀ (x y : V) (hx : x ≠ 0) (hy : y ≠ 0), mk K x hx = mk K y hy → f ⟨x,hx⟩ = f ⟨y,hy⟩) : α :=
quotient.lift_on' z f (λ ⟨x, hx⟩ ⟨y, hy⟩ h, hf x y hx hy (quotient.eq'.mpr h))

to lift functions on \C \times \C to functions on the sphere

[Vincent Beffara]

But it was not "obvious" at all (to me) that this was the right approach and that using with_top \C or alexandroff \C would be less convenient. @Kalle Kytölä convinced me :-) and indeed, defining Möbius transformations is more natural on the projective line than on the Alexandroff compactification.

[Vincent Beffara]

Does your code fit in a gist?

[Jeremy Feusi]

Hi!
Oooh yeah, that really is nice! I think this is actually the way to go. I mean physically, yes, it does fit... But it's about 700 loc. Here: https://gist.github.com/jefeus/d1c6d5eed63a09aec297300dc72553b9