Prove2Me

The identification of the Riemann sphere with P1(C)\mathbb P^1(\mathbb C) is GL2(C)\mathrm{GL}_2(\mathbb C)-equivariant

Proved
CurveSymmetry.sphereProjectiveEquiv_action

by carlok · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrycurve-symmetry-leaneuclidean-geometry

Let C^=C∪{∞}\widehat{\mathbb C}=\mathbb C\cup\{\infty\} be the Riemann sphere, let P1(C)\mathbb P^1(\mathbb C) be the projective line of one-dimensional subspaces of C2\mathbb C^2, and let Φ:C^→P1(C)\Phi:\widehat{\mathbb C}\to\mathbb P^1(\mathbb C) be the standard bijection, Φ(z)=[z:1]\Phi(z)=[z:1] for z∈Cz\in\mathbb C and Φ(∞)=[1:0]\Phi(\infty)=[1:0]. An invertible matrix g∈GL2(C)g\in\mathrm{GL}_2(\mathbb C) with rows (a,b)(a,b) and (c,d)(c,d) acts on P1(C)\mathbb P^1(\mathbb C) by g⋅[v]=[gv]g\cdot[v]=[gv], and on C^\widehat{\mathbb C} as a Möbius transformation: g⋅z=az+bcz+dg\cdot z=\frac{az+b}{cz+d} if cz+d≠0cz+d\ne0 and g⋅z=∞g\cdot z=\infty if cz+d=0cz+d=0, while g⋅∞=a/cg\cdot\infty=a/c if c≠0c\ne0 and g⋅∞=∞g\cdot\infty=\infty if c=0c=0.

Then for every g∈GL2(C)g\in\mathrm{GL}_2(\mathbb C) and every p∈C^p\in\widehat{\mathbb C},

Φ(g⋅p)=g⋅Φ(p).\Phi(g\cdot p)=g\cdot\Phi(p).

This lets the ambient Möbius maps of Theorem 2, which act on the Riemann sphere containing C^m,α\widehat C_{m,\alpha}, be treated as projective linear maps of P1\mathbb P^1, the factor of the surface P1×P1\mathbb P^1\times\mathbb P^1 in which the compactification VαV_\alpha of Lemma 4 lies. Every invertible matrix is allowed, not only the forms singled out in Theorem 2.

Formalization Note: the Riemann sphere is Mathlib's one-point compactification OnePoint ℂ, P1(C)\mathbb P^1(\mathbb C) is the projectivization of C2\mathbb C^2, and Φ\Phi is Mathlib's standard bijection between them, used as a bijection of sets (no topological statement is made); both actions are Mathlib's actions of GL2(C)\mathrm{GL}_2(\mathbb C).

Preamble
import Definitions.Def_CurveSymmetry_01_RealLoci
import Definitions.Def_CurveSymmetry_02_FamilyBasics
import Definitions.Def_CurveSymmetry_03_IsometriesAndCharts
import Mathlib.Algebra.MvPolynomial.Nilpotent
import Mathlib.Algebra.MvPolynomial.NoZeroDivisors
import Mathlib.Algebra.Polynomial.FieldDivision
import Mathlib.Algebra.Polynomial.Reverse
import Mathlib.Analysis.Complex.Isometry
import Mathlib.Analysis.Complex.OperatorNorm
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Analysis.Normed.Affine.MazurUlam
import Mathlib.Data.Complex.Basic
import Mathlib.RingTheory.MvPolynomial.Homogeneous
import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
import Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
import Mathlib.RingTheory.Polynomial.GaussLemma
import Mathlib.RingTheory.RootsOfUnity.Complex
import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
import Mathlib.Tactic
import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

open CurveSymmetry
set_option autoImplicit false
open scoped LinearAlgebra.Projectivization
open OnePoint
Formal statement
theorem CurveSymmetry.sphereProjectiveEquiv_action (g : MobiusMatrix) (p : Sphere) :
    sphereProjectiveEquiv (g • p) = g • sphereProjectiveEquiv p := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, used for Theorem 1 (p. 1), Theorem 2 (p. 2), Lemma 4 (p. 3), https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/SphereGeometry.lean (C. Perassi)

View graph