Riemann Surfaces & Uniformization Theorem

Stream: Is there code for X?

[Maxime Lucas]

From what I undestand there is very little about Riemann Surfaces in mathlib so far.I am interested in proving some stuff, possibly with the goal of proving the Uniformization Theorem. I am looking for a bit of guidance from more experienced users.
1/ mathlib seems to go up to the definition of manifolds, but not much farther. Is the way manifolds are defined really the best one? Nothing is bundled together so you have to introduce a lot of stuff anytime you want to consider a manifold. See for example all the variables introduced at the beginning of SmoothMap.I've tried defining the category of smooth manifolds for example and end up with something like this (please disregard the names), which is a lot more boiler plate than the Bundled I see everywhere else:

variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]

structure NormedSpaceCat : Type (u+1) :=
  E : Type u
  normed_add_comm_group_E : NormedAddCommGroup E
  normed_space_E : NormedSpace 𝕜 E

instance : CoeSort (NormedSpaceCat.{u} (𝕜 := 𝕜)) (Type u) where
  coe E := E.E

instance NormedSpaceCat_is_normed_add_comm_group (E : NormedSpaceCat (𝕜 := 𝕜)): NormedAddCommGroup (E.E) :=
  E.normed_add_comm_group_E

instance NormedSpaceCat_is_normed_space (E : NormedSpaceCat (𝕜 := 𝕜)): NormedSpace 𝕜 (E.E) :=
  E.normed_space_E

structure SmoothManifoldCat : Type (u+2) :=
  E : NormedSpaceCat (𝕜 := 𝕜)
  H : TopCat.{u+1}
  I : ModelWithCorners 𝕜 E H
  M : Type (u+1)
  topo : TopologicalSpace M
  charted : ChartedSpace H M
  smooth : SmoothManifoldWithCorners I M

2\ As far as I can tell there is no requirement for a Manifold to be Hausdorff. Is this on purpose or an oversight?
3\ There are many proofs of the Uniformization Theorem. Does someone have a good idea of which one would be the more suitable for mathlib? Either the one which requires the less work or the one which requires stuff that would be useful elsewhere perhaps?

[Sébastien Gouëzel]

Yes, it's on purpose that things are unbundled. If you bundle things, then you will run in troubles when you want to talk about Lie groups, because on one side you will have bundled manifolds, on the other side you will have unbundled groups, and these won't interact well. The design should be all bundled or all unbundled, and mathlib goes the unbundled way.

Yes, it's on purpose that manifolds are not Hausdorff (nor second-countable or sigma-compact): with the unbundled design, you can just add that as an assumption when it's needed, in the form of a mixin (like [T2Space M] or the variant you need). This makes it possible to have the right assumption for each statement. For instance, statements about partitions of unity or the Whitney embedding theorem will have this assumption (see for instance docs#exists_embedding_euclidean_of_compact).

[Johan Commelin]

Also, the unbundled approach allows you to smoothly (pun intended) treat your Riemann surface as a complex mfld, a real mfld, a topological space, etc...
But it is very true that you need a massive amount of variables to introduce a Lie group to Lean. There have been some experiments to make this more user friendly, but nothing conclusive yet. We should work more on that.