Holomorphy transfer kit for `ℙ¹` (CC5) #

Unit: projective-line (docs/design/projective-line.md §3.3). For a Riemann surface Z (ChartedSpace ℂ Z + IsManifold 𝓘(ℂ) ω Z, no compactness/connectedness needed anywhere) this file converts holomorphy of maps Z → OnePoint ℂ into planar AnalyticAt/MeromorphicAt statements read in coeChart/invChart:

contMDiff_coe: the coercion ℂ → ℙ¹ is holomorphic;
ContMDiffAt.onePointCoe/ContMDiff.onePointCoe: the "no poles" lift constructor;
contMDiffAt_iff_analyticAt_of_ne_infty/_of_eq_infty: chart-iff lemmas at a finite value resp. at ∞;
contMDiffAt_of_pole: the pole constructor (planar; pre-ℳ X layer) — a function agreeing near z₀ with a meromorphic g having a genuine pole, sent to ∞ at z₀, is holomorphic into ℙ¹;
meromorphicAt_coeChart_comp: the converse atom — a holomorphic map into ℙ¹ is chart-locally meromorphic;
contMDiff_inversion/inversionDiffeomorph: inversion is a biholomorphic involution.

source

theorem RS.P1.contMDiff_coe :

ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ OnePoint.some

The coercion ℂ → ℙ¹ is holomorphic.

source

theorem RS.P1.ContMDiffAt.onePointCoe {Z : Type u_1} [TopologicalSpace Z] [ChartedSpace ℂ Z] {g : Z → ℂ} {x : Z} (hg : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g x) :

ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (fun (z : Z) => ↑(g z)) x

Holomorphic lift of a holomorphic function (the "no poles" constructor).

source

theorem RS.P1.ContMDiff.onePointCoe {Z : Type u_1} [TopologicalSpace Z] [ChartedSpace ℂ Z] {g : Z → ℂ} (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) :

ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ fun (z : Z) => ↑(g z)

source

theorem RS.P1.contMDiffAt_iff_analyticAt_of_ne_infty {Z : Type u_1} [TopologicalSpace Z] [ChartedSpace ℂ Z] {f : Z → OnePoint ℂ} {x : Z} (h : f x ≠ OnePoint.infty) :

ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x ↔ ContinuousAt f x ∧ AnalyticAt ℂ (↑coeChart ∘ f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

Holomorphy at a finite value, read in the coeChart.

source

theorem RS.P1.contMDiffAt_iff_analyticAt_of_eq_infty {Z : Type u_1} [TopologicalSpace Z] [ChartedSpace ℂ Z] {f : Z → OnePoint ℂ} {x : Z} (h : f x = OnePoint.infty) :

ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f x ↔ ContinuousAt f x ∧ AnalyticAt ℂ (↑invChart ∘ f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)

Holomorphy at ∞, read in the invChart ("1/f is analytic").

source

theorem RS.P1.tendsto_coe_cobounded :

Filter.Tendsto OnePoint.some (Bornology.cobounded ℂ) (nhds OnePoint.infty)

(↑) sends cobounded ℂ to 𝓝 ∞.

source

theorem RS.P1.contMDiffAt_of_pole {g : ℂ → ℂ} {z₀ : ℂ} (_hg : MeromorphicAt g z₀) (hord : meromorphicOrderAt g z₀ < 0) {F : ℂ → OnePoint ℂ} (hFinf : F z₀ = OnePoint.infty) (hF : ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, F z = ↑(g z)) :

ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F z₀

Pole constructor (planar; the pre-ℳ X layer). A function agreeing near z₀ with a meromorphic g having a genuine pole, and sent to ∞ at z₀, is holomorphic into ℙ¹.

source