Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

An anti-Möbius map sending C^m,α\widehat C_{m,\alpha}Cm,α​ into C^m,β\widehat C_{m,\beta}Cm,β​ carries VαV_\alphaVα​ onto VβV_\betaVβ​

Proved
CurveSymmetry.family_anti_mobius_complex_transport

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

algebraic-geometrycurve-symmetry-leaneuclidean-geometry

Let m≥1m\ge1m≥1 be an integer and let α,β∈C\alpha,\beta\in\mathbb Cα,β∈C with α≠αˉ\alpha\ne\bar\alphaα=αˉ and β≠βˉ\beta\ne\bar\betaβ=βˉ​; no condition on their moduli is imposed. For γ∈{α,β}\gamma\in\{\alpha,\beta\}γ∈{α,β} let C^m,γ\widehat C_{m,\gamma}Cm,γ​ be the closure in the Riemann sphere C^=C∪{∞}\widehat{\mathbb C}=\mathbb C\cup\{\infty\}C=C∪{∞} of Cm,γ={z∈C:Re⁡(zm(∣z∣2+γ))=0}C_{m,\gamma}=\{z\in\mathbb C:\operatorname{Re}\bigl(z^m(|z|^2+\gamma)\bigr)=0\}Cm,γ​={z∈C:Re(zm(∣z∣2+γ))=0}; complex conjugation p↦pˉp\mapsto\bar pp↦pˉ​ acts on C^\widehat{\mathbb C}C, with ∞ˉ=∞\bar\infty=\infty∞ˉ=∞. For x=(x0,x1)x=(x_0,x_1)x=(x0​,x1​) and y=(y0,y1)y=(y_0,y_1)y=(y0​,y1​) in C2\mathbb C^2C2 let

Fγ(x,y)=γ x0mx1 y1m+1+x0m+1y0 y1m+γˉ x1m+1y0m y1+x0 x1m y0m+1,F_\gamma(x,y)=\gamma\,x_0^m x_1\,y_1^{m+1}+x_0^{m+1}y_0\,y_1^m+\bar\gamma\,x_1^{m+1}y_0^m\,y_1+x_0\,x_1^m\,y_0^{m+1},Fγ​(x,y)=γx0m​x1​y1m+1​+x0m+1​y0​y1m​+γˉ​x1m+1​y0m​y1​+x0​x1m​y0m+1​,

the bihomogenization of Pγ(X,Y)=Xm(γ+XY)+Ym(γˉ+XY)P_\gamma(X,Y)=X^m(\gamma+XY)+Y^m(\bar\gamma+XY)Pγ​(X,Y)=Xm(γ+XY)+Ym(γˉ​+XY), and let Vγ={([x],[y])∈P1×P1:Fγ(x,y)=0}V_\gamma=\{([x],[y])\in\mathbb P^1\times\mathbb P^1:F_\gamma(x,y)=0\}Vγ​={([x],[y])∈P1×P1:Fγ​(x,y)=0}.

Let g∈GL2(C)g\in\mathrm{GL}_2(\mathbb C)g∈GL2​(C) with rows (a,b)(a,b)(a,b) and (c,d)(c,d)(c,d) be any invertible matrix, Mg(z)=az+bcz+dM_g(z)=\frac{az+b}{cz+d}Mg​(z)=cz+daz+b​ the Möbius transformation of C^\widehat{\mathbb C}C it defines, and gˉ\bar ggˉ​ the matrix with conjugated entries; GL2(C)\mathrm{GL}_2(\mathbb C)GL2​(C) acts on P1\mathbb P^1P1 by h [x]=[hx]h\,[x]=[hx]h[x]=[hx]. Assume that the anti-Möbius map p↦Mg(pˉ)p\mapsto M_g(\bar p)p↦Mg​(pˉ​) sends C^m,α\widehat C_{m,\alpha}Cm,α​ into C^m,β\widehat C_{m,\beta}Cm,β​, that is, Mg(pˉ)∈C^m,βM_g(\bar p)\in\widehat C_{m,\beta}Mg​(pˉ​)∈Cm,β​ for every p∈C^m,αp\in\widehat C_{m,\alpha}p∈Cm,α​. Then for every (p1,p2)∈P1×P1(p_1,p_2)\in\mathbb P^1\times\mathbb P^1(p1​,p2​)∈P1×P1

(g p2, gˉ p1)∈Vβ  ⟺  (p1,p2)∈Vα.(g\,p_2,\ \bar g\,p_1)\in V_\beta\iff(p_1,p_2)\in V_\alpha.(gp2​, gˉ​p1​)∈Vβ​⟺(p1​,p2​)∈Vα​.

In the proof of Theorem 2 an anti-Möbius map M∘conjM\circ\mathrm{conj}M∘conj acts on the complexification by (X,Y)↦(M(Y),M‾(X))(X,Y)\mapsto(M(Y),\overline M(X))(X,Y)↦(M(Y),M(X)): complex conjugation on the sphere becomes the exchange of the two factors of P1×P1\mathbb P^1\times\mathbb P^1P1×P1. This is the antiholomorphic case of the step showing that an equivalence of the spherical real loci carries VαV_\alphaVα​ onto VβV_\betaVβ​; only an inclusion is assumed.

Formalization Note: the anti-Möbius map is p↦g⋅pˉp\mapsto g\cdot\bar pp↦g⋅pˉ​, with OnePoint.map star as the conjugation of OnePoint ℂ and an arbitrary ggg in GL (Fin 2) ℂ; membership in VγV_\gammaVγ​ is tested on chosen representatives.

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
Formal statement
theorem CurveSymmetry.family_anti_mobius_complex_transport {m : ℕ} (hm : 0 < m) {α β : ℂ}
    (ha : α ≠ star α) (hb : β ≠ star β) (g : MobiusMatrix)
    (hmap : ∀ p ∈ sphericalFamily m α,
      g • OnePoint.map (star : ℂ → ℂ) p ∈ sphericalFamily m β)
    (p : ProjectiveLine × ProjectiveLine) :
    complexifiedAntiMobius g p ∈ familyProjectiveCurve m β ↔ p ∈ familyProjectiveCurve m α := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note), proof of Theorem 2, 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/FamilyGlobalTransport.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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me