Prove2Me

A Möbius map with antidiagonal matrix acts on the whole sphere as z↦λ/zz\mapsto\lambda/z with λ≠0\lambda\ne0

Proved
CurveSymmetry.mobius_antidiagonal_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. A matrix g∈GL2(C)g\in\mathrm{GL}_2(\mathbb C) with rows (a,b)(a,b) and (c,d)(c,d) acts on C^\widehat{\mathbb C} by the Möbius transformation Mg(z)=az+bcz+dM_g(z)=\dfrac{az+b}{cz+d}, with the usual conventions: if c≠0c\ne0 then Mg(−d/c)=∞M_g(-d/c)=\infty and Mg(∞)=a/cM_g(\infty)=a/c, and if c=0c=0 then Mg(∞)=∞M_g(\infty)=\infty. For γ∈C\gamma\in\mathbb C let sγ:C^→C^s_\gamma:\widehat{\mathbb C}\to\widehat{\mathbb C} be the map with sγ(0)=∞s_\gamma(0)=\infty, sγ(∞)=0s_\gamma(\infty)=0 and sγ(z)=γ/zs_\gamma(z)=\gamma/z for z∈C∖{0}z\in\mathbb C\setminus\{0\}.

Suppose that a=0a=0 and d=0d=0. Then:

  1. b/c≠0b/c\ne0;
  2. MgM_g agrees with sb/cs_{b/c} at every point of the sphere:
Mg(p)=sb/c(p)for all p∈C^.M_g(p)=s_{b/c}(p)\qquad\text{for all }p\in\widehat{\mathbb C}.

Theorem 2 of the note lists the ambient symmetries of C^m,α\widehat C_{m,\alpha} as maps z↦λzz\mapsto\lambda z and z↦λ/zz\mapsto\lambda/z with constant λ\lambda, equation (3). This lemma identifies the Möbius maps with antidiagonal matrices with maps of the second kind, including their values at 00 and ∞\infty; the formalization uses it to bring Möbius maps that exchange 00 and ∞\infty into this form.

Formalization Note: C^\widehat{\mathbb C} is OnePoint ℂ and MgM_g is Mathlib's action of GL (Fin 2) ℂ on it; a,b,c,da,b,c,d are the entries g 0 0, g 0 1, g 1 0, g 1 1.

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 OnePoint
Formal statement
theorem CurveSymmetry.mobius_antidiagonal_action (g : MobiusMatrix) (ha : g 0 0 = 0) (hd : g 1 1 = 0) :
    g 0 1 / g 1 0 ≠ 0 ∧ ∀ p : Sphere, g • p = sphereInversion (g 0 1 / g 1 0) 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/MobiusPair.lean (C. Perassi)

View graph