Chart transitions of a complex curve are analytic

On a one-dimensional complex manifold, a manifold charted by ℂ whose transition maps are complex differentiable, the transition maps are in fact analytic: a complex differentiable function of one complex variable on an open set is analytic there, by the Cauchy integral formula. Being moreover injective on an open set, a transition map has nowhere vanishing derivative. This is the form in which the holomorphy of the atlas of a Riemann surface enters constructions on it, such as the elementary symmetric atlas of its symmetric powers or the local multiplicity of a holomorphic map.

The same argument shows that a map between complex curves that is holomorphic near a point has an analytic representative in any charts of the maximal atlases at the point and its image. It follows that a holomorphic map between complex curves is C^n for every n. The complex inverse function theorem also shows that the inverse of a holomorphic homeomorphism of complex curves is holomorphic.

Main declarations

• TauCeti.analyticAt_symm_trans: on a complex curve, the transition between two charts of the maximal atlas is analytic at the coordinates of every point of both chart sources.
• TauCeti.deriv_symm_trans_ne_zero: the derivative of such a transition vanishes nowhere.
• TauCeti.analyticAt_chart_comp_comp_symm: a map holomorphic near x has an analytic representative in any charts of the maximal atlases at x and f x; TauCeti.analyticAt_chartAt_comp_comp_chartAt_symm is the case of the preferred charts.
• MDifferentiable.contMDiff: a holomorphic map between complex curves is C^n for every n.
• IsHomeomorph.mdifferentiable_symm: the inverse of a holomorphic homeomorphism between complex curves is holomorphic.

Transition maps

theorem TauCeti.differentiableOn_symm_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) : DifferentiableOn ℂ (↑e' ∘ ↑e.symm) (e.symm.trans e').source

The transition map between two charts of the maximal atlas of a complex curve is holomorphic on its domain.

theorem TauCeti.analyticAt_symm_trans {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (hx : x ∈ e.source) (hx' : x ∈ e'.source) : AnalyticAt ℂ (↑e' ∘ ↑e.symm) (↑e x)

The transition between two charts of a complex curve is analytic. The transition map between two charts of the maximal atlas is analytic at the image of a point common to both chart domains.

theorem TauCeti.deriv_symm_trans_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {x : X} {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (hx : x ∈ e.source) (hx' : x ∈ e'.source) : deriv (↑e' ∘ ↑e.symm) (↑e x) ≠ 0

The derivative of a transition map between two charts of the maximal atlas vanishes nowhere: a transition map is a holomorphic injection of an open set.

Chart representatives of a holomorphic map

theorem TauCeti.analyticAt_chart_comp_comp_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} {e : OpenPartialHomeomorph X ℂ} {e' : OpenPartialHomeomorph Y ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 Y) (hx : x ∈ e.source) (hfx : f x ∈ e'.source) (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) : AnalyticAt ℂ (fun (z : ℂ) => ↑e' (f (↑e.symm z))) (↑e x)

A map that is holomorphic near x has an analytic representative in any charts of the maximal atlases at x and f x.

theorem TauCeti.analyticAt_chartAt_comp_comp_chartAt_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) : AnalyticAt ℂ (fun (z : ℂ) => ↑(chartAt ℂ (f x)) (f (↑(chartAt ℂ x).symm z))) (↑(chartAt ℂ x) x)

A map that is holomorphic near x has an analytic representative in the preferred charts at x and f x.

Regularity consequences

theorem MDifferentiable.contMDiff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {n : WithTop ℕ∞} (hf : MDiff f) : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n f

A holomorphic map between complex curves is C^n for every n, including n = ω.

theorem IsHomeomorph.mdifferentiable_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hhomeo : IsHomeomorph f) (hf : MDiff f) : MDiff ⇑(homeomorph f hhomeo).symm

The inverse of a holomorphic homeomorphism between complex curves is holomorphic.