Prove2Me

For ∣α∣=1|\alpha|=1, the map z↦c/zz\mapsto c/z sends C^m,α\widehat C_{m,\alpha} into itself if and only if c2m=αˉ2c^{2m}=\bar\alpha^2

Proved
CurveSymmetry.family_sphere_inversion_filter

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

algebraic-geometrycurve-symmetry-leanzariski-topology

Let m≥1m\ge1 be an integer, let α∈C\alpha\in\mathbb C with ∣α∣=1|\alpha|=1 and α∉R\alpha\notin\mathbb R, and let c∈Cc\in\mathbb C with c≠0c\ne0. Let Cm,α={z∈C:Re⁡(zm(∣z∣2+α))=0}C_{m,\alpha}=\{z\in\mathbb C:\operatorname{Re}(z^m(|z|^2+\alpha))=0\}, let C^m,α\widehat C_{m,\alpha} be its closure in the Riemann sphere C^=C∪{∞}\widehat{\mathbb C}=\mathbb C\cup\{\infty\}, and let Jc ⁣:C^→C^J_c\colon\widehat{\mathbb C}\to\widehat{\mathbb C} be the inversion Jc(z)=c/zJ_c(z)=c/z for z∈C∖{0}z\in\mathbb C\setminus\{0\}, Jc(0)=∞J_c(0)=\infty, Jc(∞)=0J_c(\infty)=0. Then

Jc(C^m,α)⊆C^m,α  ⟺  c2m=αˉ2.J_c(\widehat C_{m,\alpha})\subseteq\widehat C_{m,\alpha}\iff c^{2m}=\bar\alpha^{2}.

This is the inversion half of the description (3) of the ambient Möbius symmetries of C^m,α\widehat C_{m,\alpha} in Theorem 2, tested on the whole sphere, where JcJ_c exchanges 00 and ∞\infty. It is also used for Remark 5.

Formalization Note: the Riemann sphere is the one-point compactification OnePoint ℂ, C^m,α\widehat C_{m,\alpha} is the topological closure in it, and JcJ_c is defined pointwise on the sphere.

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.MvPolynomial.PDeriv
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.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.Compactification.OnePoint.ProjectiveLine

open CurveSymmetry
set_option autoImplicit false
open MvPolynomial OnePoint
Formal statement
theorem CurveSymmetry.family_sphere_inversion_filter {m : ℕ} (hm : 0 < m) {α c : ℂ}
    (hα : ‖α‖ = 1) (ha : α ≠ star α) (hc : c ≠ 0) :
    (∀ p ∈ sphericalFamily m α, sphereInversion c p ∈ sphericalFamily m α) ↔
      c ^ (2 * m) = star α ^ 2 := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for Theorem 2, p. 2, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/FamilySphereInversion.lean (C. Perassi)

View graph