Riemann-surface chart conventions

X is the eval problem's Riemann surface: [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (connectedness is only needed at the very end). This file sets up the chart-level toolkit:

• transition maps between maximal-atlas charts are analytic (C¹ over ℂ means complex-differentiable on an open set, hence analytic by DifferentiableOn.analyticOnNhd);
• Rado.HolomorphicOn F s: chartwise holomorphy of F : X → ℂ, with chart independence;
• the identity theorem on connected open subsets of X;
• stability of the maximal atlas under affine post-composition (used to normalize a chart so that its target contains the standard configuration of Rado/Complex/PlanarConnected.lean);
• point-set instances: local compactness, local (path-)connectedness, local second countability.

@[reducible, inline]

abbrev Rado.riemannAtlas (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] : Set (OpenPartialHomeomorph X ℂ)

The maximal C¹ (equivalently, holomorphic) atlas of a Riemann surface.

Equations

• Rado.riemannAtlas X = IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X

theorem Rado.transition_analyticAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ riemannAtlas X) (he' : e' ∈ riemannAtlas X) {x : X} (hx : x ∈ e.source ∩ e'.source) : AnalyticAt ℂ (↑e' ∘ ↑e.symm) (↑e x)

Transition maps between maximal-atlas charts are analytic.

theorem Rado.chartAt_mem_riemannAtlas {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] (x : X) : chartAt ℂ x ∈ riemannAtlas X

The preferred chart at a point belongs to the maximal atlas.

def Rado.HolomorphicOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (F : X → ℂ) (s : Set X) : Prop

Chartwise holomorphy of a map X → ℂ on a set, via the preferred charts.

Equations

• Rado.HolomorphicOn F s = ∀ x ∈ s, AnalyticAt ℂ (F ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

theorem Rado.HolomorphicOn.continuousOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {F : X → ℂ} {s : Set X} (hF : HolomorphicOn F s) : ContinuousOn F s

theorem Rado.HolomorphicOn.mono {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {F : X → ℂ} {s : Set X} (hF : HolomorphicOn F s) {t : Set X} (hts : t ⊆ s) : HolomorphicOn F t

theorem Rado.HolomorphicOn.analyticAt_comp_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {F : X → ℂ} {s : Set X} (hF : HolomorphicOn F s) {e : OpenPartialHomeomorph X ℂ} (he : e ∈ riemannAtlas X) {x : X} (hx : x ∈ s ∩ e.source) : AnalyticAt ℂ (F ∘ ↑e.symm) (↑e x)

Chart independence: a chartwise-holomorphic map reads as analytic through every maximal-atlas chart.

theorem Rado.HolomorphicOn.congr_of_eventuallyEq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {F G : X → ℂ} {s : Set X} (hG : HolomorphicOn G s) (h : ∀ x ∈ s, F =ᶠ[nhds x] G) : HolomorphicOn F s

If F agrees with a holomorphic map near each point of s, it is holomorphic on s.

theorem Rado.HolomorphicOn.eqOn_of_eventuallyEq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {F G : X → ℂ} {s : Set X} (hF : HolomorphicOn F s) (hG : HolomorphicOn G s) (hs : IsOpen s) (hsc : IsPreconnected s) {x : X} (hx : x ∈ s) (hFG : F =ᶠ[nhds x] G) : Set.EqOn F G s

Identity theorem on a Riemann surface: two maps holomorphic on a connected open set that agree near one of its points agree everywhere on it.

theorem Rado.affine_trans_mem_riemannAtlas {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ riemannAtlas X) {a b : ℂ} (ha : a ≠ 0) : ∃ e' ∈ riemannAtlas X, e'.source = e.source ∧ ∀ x ∈ e.source, ↑e' x = a * ↑e x + b

Post-composing a maximal-atlas chart with a complex affine map z ↦ a z + b (a ≠ 0) stays in the maximal atlas.

theorem Rado.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] : LocallyCompactSpace X

Riemann surfaces are locally compact.

theorem Rado.locallyConnectedSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] : LocallyConnectedSpace X

Riemann surfaces are locally connected.

theorem Rado.locally_secondCountable {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) : ∃ (U : Set X), x ∈ U ∧ IsOpen U ∧ SecondCountableTopology ↑U

Riemann surfaces are locally second countable.