10.3. ProjectiveLine🔗

Jacobians.ProjectiveLine — source

RiemannSphere

The Riemann sphere ℂℙ¹, modelled as the one-point compactification OnePoint ℂ = ℂ ∪ {∞}.

abbrev RiemannSphere : Type

invMap

The underlying point map of the inversion: ∞ ↦ 0, 0 ↦ ∞, and z ↦ z⁻¹ otherwise.

def invMap : RiemannSphere → RiemannSphere

invMap_infty

@[simp] lemma invMap_infty : invMap OnePoint.infty = (((0 : ℂ)) : RiemannSphere)

invMap_coe

lemma invMap_coe (z : ℂ) :
    invMap (z : RiemannSphere) =
      if z = 0 then (OnePoint.infty) else ((z⁻¹ : ℂ) : RiemannSphere)

invMap_coe_zero

@[simp] lemma invMap_coe_zero : invMap ((0 : ℂ) : RiemannSphere) = OnePoint.infty

invMap_coe_of_ne

lemma invMap_coe_of_ne {z : ℂ} (hz : z ≠ 0) :
    invMap (z : RiemannSphere) = ((z⁻¹ : ℂ) : RiemannSphere)

involutive_invMap

lemma involutive_invMap : Function.Involutive invMap

tendsto_coe_cobounded_infty

The coercion ℂ → OnePoint ℂ tends to ∞ along cobounded ℂ (i.e. as |z| → ∞).

lemma tendsto_coe_cobounded_infty :
    Tendsto ((↑) : ℂ → RiemannSphere) (cobounded ℂ) (𝓝 OnePoint.infty)

tendsto_invMap_infty

lemma tendsto_invMap_infty :
    Tendsto (fun z : ℂ => invMap (z : RiemannSphere)) (coclosedCompact ℂ)
      (𝓝 (invMap OnePoint.infty))

continuous_invMap_coe

The affine restriction z ↦ invMap z : ℂ → OnePoint ℂ is continuous.

lemma continuous_invMap_coe : Continuous (fun z : ℂ => invMap (z : RiemannSphere))

continuous_invMap

lemma continuous_invMap : Continuous invMap

inversionHomeomorph

Inversion z ↦ z⁻¹ as a self-homeomorphism of the Riemann sphere, swapping 0 ↔ ∞. This is the change of coordinates between the two standard charts.

def inversionHomeomorph : RiemannSphere ≃ₜ RiemannSphere where

inversionHomeomorph_apply

@[simp] lemma inversionHomeomorph_apply (p : RiemannSphere) :
    inversionHomeomorph p = invMap p

inversionHomeomorph_symm_apply

@[simp] lemma inversionHomeomorph_symm_apply (p : RiemannSphere) :
    inversionHomeomorph.symm p = invMap p

chartCoe

The affine chart ℂℙ¹ ⊇ {∞}ᶜ ≃ ℂ: the inverse of the open embedding ℂ ↪ OnePoint ℂ.

def chartCoe : OpenPartialHomeomorph RiemannSphere ℂ

chartCoe_source

@[simp] lemma chartCoe_source : chartCoe.source = {OnePoint.infty}ᶜ

chartCoe_target

@[simp] lemma chartCoe_target : chartCoe.target = Set.univ

chartCoe_apply_coe

lemma chartCoe_apply_coe (z : ℂ) : chartCoe (z : RiemannSphere) = z

chartCoe_symm_apply

@[simp] lemma chartCoe_symm_apply (z : ℂ) : chartCoe.symm z = (z : RiemannSphere)

chartInfty

The chart at ∞: pre-compose the affine chart with the inversion z ↦ z⁻¹.

def chartInfty : OpenPartialHomeomorph RiemannSphere ℂ

chartInfty_source

@[simp] lemma chartInfty_source : chartInfty.source = {((0 : ℂ) : RiemannSphere)}ᶜ

chartInfty_apply_infty

lemma chartInfty_apply_infty : chartInfty OnePoint.infty = 0

chartInfty_apply_coe

lemma chartInfty_apply_coe {z : ℂ} (hz : z ≠ 0) :
    chartInfty (z : RiemannSphere) = z⁻¹

chartAtRS

chartAt for the Riemann sphere: the chart at ∞ for the point ∞, the affine chart on every finite point. Defined by the OnePoint eliminator to avoid a decidability instance.

def chartAtRS (p : RiemannSphere) : OpenPartialHomeomorph RiemannSphere ℂ

chartAtRS_infty

@[simp] lemma chartAtRS_infty : chartAtRS OnePoint.infty = chartInfty

chartAtRS_coe

@[simp] lemma chartAtRS_coe (z : ℂ) : chartAtRS (z : RiemannSphere) = chartCoe

mem_chartAtRS_source

lemma mem_chartAtRS_source (p : RiemannSphere) : p ∈ (chartAtRS p).source

chartInfty_symm_apply

chartInfty.symm z = invMap (z : RiemannSphere): on the affine part it is z ↦ z⁻¹, matching the inversion.

lemma chartInfty_symm_apply (z : ℂ) :
    chartInfty.symm z = invMap (z : RiemannSphere)

homeoSphere

The Riemann sphere is homeomorphic to the unit 2-sphere S² ⊆ ℝ³ (stereographic projection).

def homeoSphere : RiemannSphere ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1

affineCoeff

The affine coefficient f(z) of the form s: the dz-coefficient read in the affine chart chartCoe, i.e. the local representative based at the finite point 0, evaluated at the finite point z. By localRep_analyticOn_chartTarget (with chartCoe.target = univ) this is entire.

noncomputable def affineCoeff (z : ℂ) : ℂ

inftyCoeff

The coefficient at ∞, g(w): the local representative based at ∞, read in the ∞-chart chartInfty. Analytic on chartInfty.target (a neighbourhood of 0), in particular continuous at 0.

noncomputable def inftyCoeff (w : ℂ) : ℂ

chartAt_coe

lemma chartAt_coe (z : ℂ) : chartAt ℂ (z : RiemannSphere) = chartCoe

chartAt_infty

lemma chartAt_infty : chartAt ℂ (OnePoint.infty : RiemannSphere) = chartInfty

affineCoeff_analyticOnNhd

affineCoeff s is entire (analytic on all of ℂ).

lemma affineCoeff_analyticOnNhd : AnalyticOnNhd ℂ (affineCoeff s) Set.univ

affineCoeff_differentiable

lemma affineCoeff_differentiable : Differentiable ℂ (affineCoeff s)

inftyCoeff_continuousAt_zero

inftyCoeff s is analytic on chartInfty.target, hence continuous at 0 (since 0 = chartInfty ∞ ∈ chartInfty.target).

lemma inftyCoeff_continuousAt_zero : ContinuousAt (inftyCoeff s) 0

trivAt_zero_symmL_one

The affine-frame unit tangent at a finite point z is just 1 ∈ ℂ: the chart transition chartCoe ∘ chartCoe.symm is the identity, so its derivative is 1.

lemma trivAt_zero_symmL_one (z : ℂ) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := RiemannSphere)) ((0 : ℂ) : RiemannSphere)).symmL
        ℂ (z : RiemannSphere) (1 : ℂ) = (1 : ℂ)

trivAt_infty_symmL_one

The ∞-frame unit tangent at a finite point z ≠ 0 is -z²: the chart transition chartCoe ∘ chartInfty.symm is w ↦ w⁻¹ near chartInfty (z:RS) = z⁻¹, with derivative -(z⁻¹)⁻² = -z². This is the dz = -w⁻² dw Jacobian of the inversion.

lemma trivAt_infty_symmL_one {z : ℂ} (hz : z ≠ 0) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := RiemannSphere)) (OnePoint.infty)).symmL
        ℂ (z : RiemannSphere) (1 : ℂ) = -z ^ 2

inftyCoeff_eq_transition

The transition law (dz ↦ -w⁻² dw). For a finite point z ≠ 0, the affine coefficient and the ∞-coefficient (read at the *same* sphere point z, i.e. at chart coordinate w = z⁻¹ in the ∞-chart) satisfy g(z⁻¹) = -z² · f(z). Equivalently f(z) = -z⁻² · g(z⁻¹).

lemma inftyCoeff_eq_transition {z : ℂ} (hz : z ≠ 0) :
    inftyCoeff s z⁻¹ = -z ^ 2 * affineCoeff s z

affineCoeff_tendsto_cobounded

O(z⁻²) decay at ∞. The affine coefficient tends to 0 along cobounded (|z| → ∞): f(z) = -z⁻² g(z⁻¹) with g(z⁻¹) → g(0) bounded and z⁻² → 0.

lemma affineCoeff_tendsto_cobounded :
    Filter.Tendsto (affineCoeff s) (Bornology.cobounded ℂ) (𝓝 0)

affineCoeff_eq_zero

The affine coefficient vanishes identically. f is entire and tends to 0 at ∞ (Liouville: a bounded entire function tending to a limit at infinity is that constant).

lemma affineCoeff_eq_zero : affineCoeff s = 0

affineCoeff_eq_toFun_one

At a finite point z, the affine coefficient is s.toFun (z:RS) applied to the affine-frame unit 1.

lemma affineCoeff_eq_toFun_one (z : ℂ) :
    affineCoeff s z = s.toFun (z : RiemannSphere) (1 : ℂ)

section_apply_eq_zero_coe

The section vanishes at every finite point: s.toFun (z:RS) = 0. The affine-frame unit 1 spans the 1-dimensional fibre ℂ, and s.toFun (z:RS) 1 = f(z) = 0.

lemma section_apply_eq_zero_coe (z : ℂ) : s.toFun (z : RiemannSphere) = 0

trivAt_infty_symmL_one_at_infty

The ∞-frame unit tangent at the point ∞ is 1 ∈ ℂ: the chart transition chartInfty ∘ chartInfty.symm is the identity, so its derivative is 1.

lemma trivAt_infty_symmL_one_at_infty :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ, ℂ) (M := RiemannSphere)) (OnePoint.infty)).symmL
        ℂ (OnePoint.infty : RiemannSphere) (1 : ℂ) = (1 : ℂ)

inftyCoeff_eq_zero_of_ne

inftyCoeff s vanishes on the punctured chart target: for w ≠ 0, chartInfty.symm w = (w⁻¹ : RS) is a finite point, where s.toFun is 0.

lemma inftyCoeff_eq_zero_of_ne {w : ℂ} (hw : w ≠ 0) : inftyCoeff s w = 0

inftyCoeff_zero_eq_zero

inftyCoeff s 0 = 0: continuity at 0 plus vanishing on the punctured neighbourhood.

lemma inftyCoeff_zero_eq_zero : inftyCoeff s 0 = 0

section_apply_eq_zero_infty

The section vanishes at ∞: s.toFun ∞ = 0. The ∞-frame unit at ∞ is 1, and s.toFun ∞ 1 = inftyCoeff s 0 = 0; then ext_ring.

lemma section_apply_eq_zero_infty : s.toFun (OnePoint.infty : RiemannSphere) = 0

holomorphicOneForm_eq_zero

Liouville vanishing. Every global holomorphic 1-form on ℂℙ¹ is zero.

See the section docstring for the proof outline (chart pull-back → entire coefficient → O(z⁻²) decay at ∞ → bounded → constant by Liouville → constant = 0).

theorem holomorphicOneForm_eq_zero (s : HolomorphicOneForms RiemannSphere) : s = 0

genus_eq_zero

The Riemann sphere ℂℙ¹ has genus 0.

theorem genus_eq_zero : genus RiemannSphere = 0