Prove2Me

Stereographic projection S3∖{N}→N⊥S^3\setminus\{N\}\to N^\perp preserves orientation: Jacobian formula

Proved
HryniewiczCriterion.volumeIn_stereographic_differential

by Mazecto · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometry-topologysymplectic-geometry

Let N,y∈S3⊂R4N,y\in S^3\subset\mathbb{R}^4 with y≠Ny\neq N, and put k=⟨y,N⟩k=\langle y,N\rangle, so k<1k<1. The differential of the stereographic projection σN(y)=y−⟨y,N⟩N1−⟨y,N⟩\sigma_N(y)=\dfrac{y-\langle y,N\rangle N}{1-\langle y,N\rangle} (stereographicFrom) at yy is

dσy(x)=x−⟨x,N⟩N1−k+⟨x,N⟩(1−k)2 (y−kN).d\sigma_y(x)=\frac{x-\langle x,N\rangle N}{1-k}+\frac{\langle x,N\rangle}{(1-k)^2}\,(y-kN).

For tangent vectors x1,x2,x3⊥yx_1,x_2,x_3\perp y,

det⁡(−N, dσyx1, dσyx2, dσyx3)=det⁡(y,x1,x2,x3)(1−k)3,\det\big(-N,\ d\sigma_y x_1,\ d\sigma_y x_2,\ d\sigma_y x_3\big)=\frac{\det(y,x_1,x_2,x_3)}{(1-k)^3},

where the left side is volumeIn N (the volume form of N⊥N^\perp oriented by det⁡(−N,⋅,⋅,⋅)\det(-N,\cdot,\cdot,\cdot)). Since 1−k>01-k>0, stereographic projection is orientation preserving from S3S^3, oriented as the boundary of the unit ball, to N⊥N^\perp.

Proof: the NN-components drop out, and multilinearity leaves (1−k)−3det⁡(−N,x1,x2,x3)+(1−k)−4∑i⟨xi,N⟩det⁡(−N,…,y,… )(1-k)^{-3}\det(-N,x_1,x_2,x_3)+(1-k)^{-4}\sum_i\langle x_i,N\rangle\det(-N,\dots,y,\dots). Two instances of the five-vector Laplace (Cramer) identity, paired with yy and with NN, give det⁡(N,x1,x2,x3)=kD\det(N,x_1,x_2,x_3)=kD and ∑i⟨xi,N⟩det⁡(y,…,N,… )=(1−k2)D\sum_i\langle x_i,N\rangle\det(y,\dots,N,\dots)=(1-k^2)D, where D=det⁡(y,x1,x2,x3)D=\det(y,x_1,x_2,x_3). The total is (1−k)−3(−kD+(1+k)D)=D/(1−k)3(1-k)^{-3}(-kD+(1+k)D)=D/(1-k)^3.

Preamble
import Definitions.Def_HryniewiczCriterion_SelfLinking

open HryniewiczCriterion
open scoped ContDiff
Formal statement
theorem HryniewiczCriterion.volumeIn_stereographic_differential (N y x₁ x₂ x₃ : R4) (hN : euclidNorm N = 1) (hy : euclidNorm y = 1) (hyN : y ≠ N)
    (h₁ : dot4 x₁ y = 0) (h₂ : dot4 x₂ y = 0) (h₃ : dot4 x₃ y = 0) :
    volumeIn N ((1 - dot4 y N)⁻¹ • (x₁ - dot4 x₁ N • N) + (dot4 x₁ N / (1 - dot4 y N) ^ 2) • (y - dot4 y N • N))
      ((1 - dot4 y N)⁻¹ • (x₂ - dot4 x₂ N • N) + (dot4 x₂ N / (1 - dot4 y N) ^ 2) • (y - dot4 y N • N))
      ((1 - dot4 y N)⁻¹ • (x₃ - dot4 x₃ N • N) + (dot4 x₃ N / (1 - dot4 y N) ^ 2) • (y - dot4 y N • N)) =
      Matrix.det (Matrix.of ![y, x₁, x₂, x₃]) / (1 - dot4 y N) ^ 3 := by sorry
Source
Standard (stereographic projection is a conformal orientation-preserving diffeomorphism S^3 \ {N} -> R^3); used for the orientation conventions of the Gauss linking integral in U. Hryniewicz, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Definition 1.5.

View graph