Möbius transformations of the projective line are analytic

Mathlib identifies the projective line OnePoint 𝕜 with the projectivization ℙ 𝕜 (Fin 2 → 𝕜) (OnePoint.equivProjectivization) and lets GL (Fin 2) 𝕜 act on it through this identification (OnePoint.instGLAction), by the Möbius transformations z ↦ (a * z + b) / (c * z + d). This file relates that description to the two charts of the analytic manifold OnePoint 𝕜, and shows that every Möbius transformation is analytic.

In homogeneous coordinates, the affine chart reads the point [v₀ : v₁] as v₀ / v₁ where v₁ ≠ 0, and the inverted chart reads it as v₁ / v₀ where v₀ ≠ 0. The inverse of the inverted chart is itself the Möbius transformation of the matrix !![0, 1; 1, 0], restricted to 𝕜.

Analyticity is checked on 𝕜 first: near a point z₀ where c * z₀ + d ≠ 0 the transformation is the analytic function (a * z + b) / (c * z + d) followed by the inclusion 𝕜 → OnePoint 𝕜, and near a pole it is (c * z + d) / (a * z + b) followed by the inverse of the inverted chart, the numerator a * z₀ + b being nonzero there because the matrix is invertible. Near ∞, a Möbius transformation precomposed with the inverse of the inverted chart is again a Möbius transformation restricted to 𝕜.

Hence GL (Fin 2) 𝕜 acts on OnePoint 𝕜 by analytic maps (OnePoint.instContMDiffConstSMul), and so does PSL(2, 𝕜), which acts through representatives (OnePoint.instContMDiffConstSMulPSL). For 𝕜 = ℂ, each Möbius transformation is therefore a biholomorphism of the Riemann sphere, with inverse the transformation of the inverse matrix: this is Diffeomorph.constSmul 𝓘(ℂ) ω g. Restricting scalars, the Möbius transformations are also smooth maps of the underlying real surface, and in the affine coordinate the transformation of !![a, b; c, d] has derivative det / (c * z + d) ^ 2.

Main results

• OnePoint.affineChart_equivProjectivization_symm_mk and OnePoint.invChart_equivProjectivization_symm_mk: the two charts in homogeneous coordinates.
• OnePoint.invChart_symm_eq_smul: the inverse of the inverted chart is a Möbius transformation.
• Matrix.GeneralLinearGroup.contMDiff_smul_coe: a Möbius transformation restricted to 𝕜 is analytic.
• OnePoint.instContMDiffConstSMul: GL (Fin 2) 𝕜 acts on OnePoint 𝕜 by analytic maps.
• OnePoint.instContMDiffConstSMulPGL: so does PGL(2, 𝕜).
• OnePoint.instContinuousConstSMul: in particular it acts by homeomorphisms.
• OnePoint.instContMDiffConstSMulPSL: PSL(2, 𝕜) acts on OnePoint 𝕜 by analytic maps.
• OnePoint.instContMDiffConstSMulGLReal, OnePoint.instContMDiffConstSMulPSLReal: GL(2, ℂ) and PSL(2, ℂ) act on the Riemann sphere by smooth maps of the underlying real surface.
• OnePoint.mfderiv_smul_coe_apply: the derivative of a Möbius transformation in the affine coordinate.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §§1–2.

The charts in homogeneous coordinates

These lemmas are simp↓ (pre-simp) lemmas: as ordinary simp lemmas they would never fire, since simp first rewrites the inner point with Mathlib's equivProjectivization_symm_apply_mk.

@[simp]

theorem OnePoint.equivProjectivization_symm_mk_mem_affineChart_source_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] {v : Fin 2 → 𝕜} (hv : v ≠ 0) : (equivProjectivization 𝕜).symm (Projectivization.mk 𝕜 v hv) ∈ affineChart.source ↔ v 1 ≠ 0

The point [v₀ : v₁] of the projective line lies in the source of the affine chart exactly when v₁ ≠ 0.

@[simp]

theorem OnePoint.affineChart_equivProjectivization_symm_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] {v : Fin 2 → 𝕜} (hv : v ≠ 0) : ↑affineChart ((equivProjectivization 𝕜).symm (Projectivization.mk 𝕜 v hv)) = v 0 / v 1

The affine chart reads the point [v₀ : v₁] of the projective line as v₀ / v₁. Off its source, where v₁ = 0, both sides are 0.

@[simp]

theorem OnePoint.equivProjectivization_symm_mk_mem_invChart_source_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] [ProperSpace 𝕜] {v : Fin 2 → 𝕜} (hv : v ≠ 0) : (equivProjectivization 𝕜).symm (Projectivization.mk 𝕜 v hv) ∈ invChart.source ↔ v 0 ≠ 0

The point [v₀ : v₁] of the projective line lies in the source of the inverted chart exactly when v₀ ≠ 0.

@[simp]

theorem OnePoint.invChart_equivProjectivization_symm_mk {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] [ProperSpace 𝕜] {v : Fin 2 → 𝕜} (hv : v ≠ 0) : ↑invChart ((equivProjectivization 𝕜).symm (Projectivization.mk 𝕜 v hv)) = v 1 / v 0

The inverted chart reads the point [v₀ : v₁] of the projective line as v₁ / v₀. Off its source, where v₀ = 0, both sides are 0.

Möbius transformations

theorem OnePoint.invChart_symm_eq_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] [ProperSpace 𝕜] (w : 𝕜) : ↑invChart.symm w = Matrix.GeneralLinearGroup.mkOfDetNeZero !![0, 1; 1, 0] ⋯ • ↑w

The inverse of the inverted chart, 0 ↦ ∞ and w ↦ w⁻¹ for w ≠ 0, is the Möbius transformation z ↦ 1 / z of the matrix !![0, 1; 1, 0], restricted to 𝕜.

theorem Matrix.GeneralLinearGroup.contMDiff_smul_coe {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] [ProperSpace 𝕜] (g : GL (Fin 2) 𝕜) : ContMDiff (modelWithCornersSelf 𝕜 𝕜) (modelWithCornersSelf 𝕜 𝕜) ⊤ fun (z : 𝕜) => g • ↑z

A Möbius transformation restricted to 𝕜 is analytic. For g = !![a, b; c, d], it is z ↦ (a * z + b) / (c * z + d) away from the pole and sends the pole to ∞.

instance OnePoint.instContMDiffConstSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] [ProperSpace 𝕜] : ContMDiffConstSMul (modelWithCornersSelf 𝕜 𝕜) ⊤ (GL (Fin 2) 𝕜) (OnePoint 𝕜)

Möbius transformations of the projective line are analytic. For 𝕜 = ℂ, every transformation z ↦ (a * z + b) / (c * z + d) of the Riemann sphere is holomorphic, and hence a biholomorphism Diffeomorph.constSmul 𝓘(ℂ) ω g with inverse the transformation of g⁻¹.

instance OnePoint.instContMDiffConstSMulPGL {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] [ProperSpace 𝕜] : ContMDiffConstSMul (modelWithCornersSelf 𝕜 𝕜) ⊤ (Matrix.ProjGenLinGroup (Fin 2) 𝕜) (OnePoint 𝕜)

The Möbius transformations of PGL(2, 𝕜) are analytic, since the class of a matrix acts as the matrix does.

instance OnePoint.instContinuousConstSMul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] [ProperSpace 𝕜] : ContinuousConstSMul (GL (Fin 2) 𝕜) (OnePoint 𝕜)

Möbius transformations are homeomorphisms of the projective line.

instance OnePoint.instContMDiffConstSMulPSL {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [DecidableEq 𝕜] [ProperSpace 𝕜] : ContMDiffConstSMul (modelWithCornersSelf 𝕜 𝕜) ⊤ (Matrix.ProjectiveSpecialLinearGroup (Fin 2) 𝕜) (OnePoint 𝕜)

PSL(2, 𝕜) acts on the projective line by analytic maps, through representatives.

Möbius transformations as smooth maps of the real surface

instance OnePoint.instContMDiffConstSMulGLReal {n : WithTop ℕ∞} : ContMDiffConstSMul (modelWithCornersSelf ℝ ℂ) n (GL (Fin 2) ℂ) (OnePoint ℂ)

GL(2, ℂ) acts on the Riemann sphere, regarded as a real surface, by smooth (indeed real-analytic) maps: each Möbius transformation is holomorphic.

instance OnePoint.instContMDiffConstSMulPSLReal {n : WithTop ℕ∞} : ContMDiffConstSMul (modelWithCornersSelf ℝ ℂ) n (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℂ) (OnePoint ℂ)

PSL(2, ℂ) acts on the Riemann sphere, regarded as a real surface, by smooth (indeed real-analytic) maps.

theorem OnePoint.mfderiv_smul_coe_apply (g : GL (Fin 2) ℂ) {z : ℂ} (hz : ↑g 1 0 * z + ↑g 1 1 ≠ 0) (v : ℂ) : ((mfderiv% fun (x : OnePoint ℂ) => g • x) ↑z) v = (↑g).det / (↑g 1 0 * z + ↑g 1 1) ^ 2 * v

The derivative of a Möbius transformation in the affine coordinate. At a finite point z which g = !![a, b; c, d] does not send to ∞, the derivative of g on the Riemann sphere, read in the affine charts, is multiplication by det g / (c * z + d) ^ 2.