The projective line OnePoint 𝕜 as an analytic manifold

For a nontrivially normed field 𝕜 whose closed balls are compact (ProperSpace 𝕜, as for ℝ, ℂ and ℚ_[p]), the one-point compactification OnePoint 𝕜 = 𝕜 ∪ {∞} is the projective line over 𝕜. This file charts it by the two classical coordinates: the affine coordinate OnePoint.affineChart, which reads a finite point z as z and is defined off ∞, and the inverted coordinate OnePoint.invChart, which reads a point z as z⁻¹ and ∞ as 0 and is defined off 0. Their transition map is z ↦ z⁻¹ on 𝕜ˣ, which is analytic, so these two charts make OnePoint 𝕜 a one-dimensional analytic manifold over 𝕜 (OnePoint.instIsManifold). Properness is what makes the inverted chart continuous at ∞: neighbourhoods of ∞ are complements of compact sets, and these must contain the complements of balls.

For 𝕜 = ℂ this is the Riemann sphere. Mathlib already shows that OnePoint ℂ is compact, Hausdorff and connected, so it is a compact connected Riemann surface, the target of meromorphic functions regarded as holomorphic maps. Differentiability (for 𝕜 = ℂ, holomorphy) of a map into OnePoint 𝕜 is tested in the two charts. At a point sent to a finite value it is continuity together with differentiability in the affine chart (OnePoint.mdifferentiableAt_iff_of_ne_infty); for a map that only takes finite values this is differentiability of the 𝕜-valued map (OnePoint.mdifferentiableAt_coe_comp_iff). At a point sent to ∞ it is continuity together with differentiability of the reciprocal, read in the inverted chart (OnePoint.mdifferentiableAt_iff_of_eq_infty).

Main declarations

• OnePoint.affineChart and OnePoint.invChart: the two charts of OnePoint 𝕜.
• OnePoint.instChartedSpace: the charted space structure, with preferred charts OnePoint.chartAt_coe and OnePoint.chartAt_infty.
• OnePoint.instIsManifold: the analytic manifold structure.
• OnePoint.contMDiff_coe: the inclusion 𝕜 → OnePoint 𝕜 is analytic.
• OnePoint.mdifferentiableAt_iff_of_ne_infty, OnePoint.mdifferentiableAt_iff_of_eq_infty and OnePoint.mdifferentiableAt_coe_comp_iff: differentiability of maps into OnePoint 𝕜.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §1.5 (c).

The affine chart

def OnePoint.affineChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : OpenPartialHomeomorph (OnePoint 𝕜) 𝕜

The affine chart of the projective line OnePoint 𝕜: it reads a finite point z as z, and is defined on the complement of ∞, with target all of 𝕜. Its inverse is the inclusion 𝕜 → OnePoint 𝕜 (OnePoint.affineChart_symm_apply).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OnePoint.affineChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : affineChart.source = {infty}ᶜ

@[simp]

theorem OnePoint.affineChart_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : affineChart.target = Set.univ

@[simp]

theorem OnePoint.affineChart_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (z : 𝕜) : ↑affineChart ↑z = z

@[simp]

theorem OnePoint.affineChart_infty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] : ↑affineChart infty = 0

@[simp]

theorem OnePoint.affineChart_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (z : 𝕜) : ↑affineChart.symm z = ↑z

The inverted chart

noncomputable def OnePoint.invChart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : OpenPartialHomeomorph (OnePoint 𝕜) 𝕜

The inverted chart of the projective line OnePoint 𝕜: it reads a point z as z⁻¹ and ∞ as 0, and is defined on the complement of 0, with target all of 𝕜. Its inverse sends 0 to ∞ and w ≠ 0 to w⁻¹ (OnePoint.invChart_symm_zero and OnePoint.invChart_symm_of_ne_zero).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OnePoint.invChart_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : invChart.source = {↑0}ᶜ

@[simp]

theorem OnePoint.invChart_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : invChart.target = Set.univ

@[simp]

theorem OnePoint.invChart_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (z : 𝕜) : ↑invChart ↑z = z⁻¹

@[simp]

theorem OnePoint.invChart_infty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : ↑invChart infty = 0

@[simp]

theorem OnePoint.invChart_symm_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : ↑invChart.symm 0 = infty

@[simp]

theorem OnePoint.invChart_symm_of_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {w : 𝕜} (hw : w ≠ 0) : ↑invChart.symm w = ↑w⁻¹

The charted space

@[instance_reducible]

noncomputable instance OnePoint.instChartedSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : ChartedSpace 𝕜 (OnePoint 𝕜)

The projective line OnePoint 𝕜 as a charted space modelled on 𝕜: its atlas consists of the affine chart and the inverted chart, the preferred chart at a finite point being the affine chart (OnePoint.chartAt_coe) and the preferred chart at ∞ the inverted chart (OnePoint.chartAt_infty).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem OnePoint.chartAt_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (z : 𝕜) : chartAt 𝕜 ↑z = affineChart

@[simp]

theorem OnePoint.chartAt_infty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : chartAt 𝕜 infty = invChart

theorem OnePoint.mem_atlas_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {e : OpenPartialHomeomorph (OnePoint 𝕜) 𝕜} : e ∈ atlas 𝕜 (OnePoint 𝕜) ↔ e = affineChart ∨ e = invChart

The analytic structure

instance OnePoint.instIsManifold {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : IsManifold (modelWithCornersSelf 𝕜 𝕜) ⊤ (OnePoint 𝕜)

The projective line is an analytic manifold. The transition maps between the affine and inverted charts are z ↦ z⁻¹ on 𝕜ˣ, which is analytic. For 𝕜 = ℂ this makes the Riemann sphere OnePoint ℂ a Riemann surface.

Differentiable maps into the projective line

For 𝕜 = ℂ, differentiability of a map into OnePoint ℂ is holomorphy into the Riemann sphere.

theorem OnePoint.contMDiff_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] : ContMDiff (modelWithCornersSelf 𝕜 𝕜) (modelWithCornersSelf 𝕜 𝕜) ⊤ some

The inclusion 𝕜 → OnePoint 𝕜 is analytic: it is the inverse of the affine chart.

theorem OnePoint.mdifferentiableAt_coe_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {g : M → 𝕜} {x : M} : (MDiffAt fun (y : M) => ↑(g y)) x ↔ MDiffAt g x

A map into 𝕜, regarded as a map into the projective line OnePoint 𝕜, is differentiable at a point exactly when it is differentiable there as a 𝕜-valued map.

theorem OnePoint.mdifferentiableAt_iff_of_ne_infty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → OnePoint 𝕜} {x : M} (hx : f x ≠ infty) : MDiffAt f x ↔ ContinuousAt f x ∧ MDiffAt (↑affineChart ∘ f) x

A map into the projective line OnePoint 𝕜 is differentiable at a point sent to a finite value exactly when it is continuous there and differentiable there when read in the affine chart.

theorem OnePoint.mdifferentiableAt_iff_of_eq_infty {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {f : M → OnePoint 𝕜} {x : M} (hx : f x = infty) : MDiffAt f x ↔ ContinuousAt f x ∧ MDiffAt (↑invChart ∘ f) x

A map into the projective line OnePoint 𝕜 is differentiable at a point sent to ∞ exactly when it is continuous there and differentiable there when read in the inverted chart, that is, when its reciprocal is differentiable there.