An anti-Möbius map sending into carries onto
ProvedCurveSymmetry.family_anti_mobius_complex_transportLet be an integer and let with and ; no condition on their moduli is imposed. For let be the closure in the Riemann sphere of ; complex conjugation acts on , with . For and in let
the bihomogenization of , and let .
Let with rows and be any invertible matrix, the Möbius transformation of it defines, and the matrix with conjugated entries; acts on by . Assume that the anti-Möbius map sends into , that is, for every . Then for every
In the proof of Theorem 2 an anti-Möbius map acts on the complexification by : complex conjugation on the sphere becomes the exchange of the two factors of . This is the antiholomorphic case of the step showing that an equivalence of the spherical real loci carries onto ; only an inclusion is assumed.
Formalization Note: the anti-Möbius map is , with OnePoint.map star as the conjugation of OnePoint ℂ and an arbitrary in GL (Fin 2) ℂ; membership in is tested on chosen representatives.
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
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 sorryConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.