Uniformization theorem for Riemann surfaces

uniformization

Submitter: Junyan Xu.

Notes: Unavailable.

Source: John Hamal Hubbard, *Teichmüller theory and applications to geometry, topology, and dynamics. Vol. 1*, Chapter 1.

Informal solution: Unavailable.

theorem declaration uses `sorry`uniformization {X : Type*} [TopologicalSpace X] [T2Space X] [ConnectedSpace X]
    [SecondCountableTopology X] [ChartedSpace ℂ X] [IsManifold mℂ 1 X]
    (hX : ¬ CompactSpace X) (x : X) [Subsingleton <| Additive (FundamentalGroup X x) →+ ℝ] :
    Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ ℂ) ∨ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ UpperHalfPlane) := byX:Type u_1inst✝⁶:TopologicalSpace Xinst✝⁵:T2Space Xinst✝⁴:ConnectedSpace Xinst✝³:SecondCountableTopology Xinst✝²:ChartedSpace ℂ Xinst✝¹:IsManifold mℂ 1 XhX:¬CompactSpace Xx:Xinst✝:Subsingleton (Additive (FundamentalGroup X x) →+ ℝ)⊢ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ ℂ) ∨ Nonempty (X ≃ₘ⟮mℂ, mℂ⟯ UpperHalfPlane)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.