Prove2Me

The parameters eiθe^{i\theta}, 0<θ<π0<\theta<\pi, give pairwise fully Möbius-inequivalent curves C^m,α\widehat{C}_{m,\alpha}

Proved
CurveSymmetry.family_arc_equivalence_iff

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

algebraic-geometrycurve-symmetry-leanzariski-topology

Let m≥2m\ge 2 be an integer. For α∈C\alpha\in\mathbb{C} let Cm,α={z∈C:Re⁡(zm(∣z∣2+α))=0}C_{m,\alpha}=\{z\in\mathbb{C} : \operatorname{Re}\bigl(z^m(|z|^2+\alpha)\bigr)=0\} and let C^m,α\widehat{C}_{m,\alpha} be its closure in the Riemann sphere C^=C∪{∞}\widehat{\mathbb{C}}=\mathbb{C}\cup\{\infty\}. A matrix g=(gjk)∈GL2(C)g=(g_{jk})\in\mathrm{GL}_2(\mathbb{C}) acts on C^\widehat{\mathbb{C}} by the Möbius transformation p↦(g11p+g12)/(g21p+g22)p\mapsto(g_{11}p+g_{12})/(g_{21}p+g_{22}), and κ:C^→C^\kappa:\widehat{\mathbb{C}}\to\widehat{\mathbb{C}} denotes complex conjugation, κ(z)=zˉ\kappa(z)=\bar z for z∈Cz\in\mathbb{C} and κ(∞)=∞\kappa(\infty)=\infty. Let θ,φ∈(0,π)\theta,\varphi\in(0,\pi).

Then C^m,eiθ\widehat{C}_{m,e^{i\theta}} is carried onto C^m,eiφ\widehat{C}_{m,e^{i\varphi}} by a Möbius transformation gg or by an anti-Möbius transformation g∘κg\circ\kappa if and only if θ=φ\theta=\varphi:

∃ g∈GL2(C):  g(C^m,eiθ)=C^m,eiφ  or  g(κ(C^m,eiθ))=C^m,eiφ⟺θ=φ.\exists\,g\in\mathrm{GL}_2(\mathbb{C}):\ \ g\bigl(\widehat{C}_{m,e^{i\theta}}\bigr)=\widehat{C}_{m,e^{i\varphi}}\ \ \text{or}\ \ g\bigl(\kappa(\widehat{C}_{m,e^{i\theta}})\bigr)=\widehat{C}_{m,e^{i\varphi}}\qquad\Longleftrightarrow\qquad\theta=\varphi.

This is the claim of Remark 5 of the note that, for fixed m≥2m\ge2, the parameters α=eiθ\alpha=e^{i\theta} with 0<θ<π0<\theta<\pi give pairwise fully Möbius-inequivalent curves, a full Möbius equivalence being a holomorphic Möbius map or such a map composed with complex conjugation.

Formalization Note: The sphere is OnePoint ℂ, C^m,α\widehat{C}_{m,\alpha} is the topological closure of the image of Cm,αC_{m,\alpha}, and the equalities are equalities of images of subsets of the sphere.

Preamble
import Definitions.Def_CurveSymmetry_01_RealLoci
import Definitions.Def_CurveSymmetry_02_FamilyBasics
import Definitions.Def_CurveSymmetry_03_IsometriesAndCharts
import Definitions.Def_CurveSymmetry_04_ProjectiveClosure
import Mathlib.Algebra.MvPolynomial.Nilpotent
import Mathlib.Algebra.MvPolynomial.NoZeroDivisors
import Mathlib.Algebra.MvPolynomial.PDeriv
import Mathlib.Algebra.Polynomial.FieldDivision
import Mathlib.Algebra.Polynomial.Reverse
import Mathlib.Analysis.Calculus.FDeriv.Analytic
import Mathlib.Analysis.Calculus.FDeriv.Equiv
import Mathlib.Analysis.Calculus.FDeriv.Mul
import Mathlib.Analysis.Calculus.FDeriv.Pi
import Mathlib.Analysis.Complex.Isometry
import Mathlib.Analysis.Complex.OperatorNorm
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Analysis.Normed.Affine.MazurUlam
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.FieldTheory.Separable
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.Algebra.Module.FiniteDimension
import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

open CurveSymmetry
set_option autoImplicit false
Formal statement
theorem CurveSymmetry.family_arc_equivalence_iff {m : ℕ} (hm : 2 ≤ m) {θ φ : ℝ}
    (hθ : θ ∈ Set.Ioo 0 Real.pi) (hφ : φ ∈ Set.Ioo 0 Real.pi) :
    ((∃ g : MobiusMatrix, (fun p : Sphere => g • p) ''
        sphericalFamily m (arcParameter θ) = sphericalFamily m (arcParameter φ)) ∨
     (∃ g : MobiusMatrix, (fun p : Sphere => g • OnePoint.map (star : ℂ → ℂ) p) ''
        sphericalFamily m (arcParameter θ) = sphericalFamily m (arcParameter φ))) ↔ θ = φ := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note), Remark 5, p. 4, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/FamilyParameterArc.lean (C. Perassi)
Human review

  • Endorsed by Shuze Chen · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by carlok · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph