Papers With

← All papers
First page of A complete classification of left-invariant Einstein metrics on $S^3\times S^3$

A complete classification of left-invariant Einstein metrics on $S^3\times S^3$

Sixuan Gu, Wei Qi

math.DG Sep 6, 2026 · v1 math-ph
formalization mathlib geometry
Read PDF arXiv abstract Code
TL;DR
The two main classification theorems are formalized in Lean 4 using Mathlib, with the code in a public GitHub repository.
Abstract
We complete the classification of compact simply connected homogeneous Einstein manifolds in dimension six by resolving the remaining cases for left-invariant Einstein metrics on $G=\mathrm{SU}(2)\times\mathrm{SU}(2)\cong S^3\times S^3$. Previous work leaves two cases for the isotropy group $K$, namely $K=\{e\}$ and $K\cong\mathbb Z_2$. We first rule out $K=\{e\}$. Then we show that any $\mathbb Z_2$ symmetry generated by an inner involution $σ$ with $\trσ=-2$ necessarily extends to a $\mathbb Z_2\times\mathbb Z_2$ symmetry. Together with the previously known classification results, these theorems imply that every left-invariant Einstein metric on $G$ is, up to homothety and isometry, either the standard product metric $g_{\rm can}$ or the Jensen nearly Kähler metric $g_{\rm NK}$.
Problem

The classification of compact simply connected six-dimensional homogeneous Einstein manifolds reduces to classifying left-invariant Einstein metrics on SU(2)×SU(2). Two isotropy cases remained open: trivial isotropy and Z2 isotropy.

Approach

Left-invariant metrics are parametrized globally by graph coordinates (P,Q,M): two positive-definite symmetric matrices and one arbitrary 3×3 matrix. In these coordinates the scalar curvature has an explicit formula. Einstein metrics are critical points of scalar curvature at fixed volume, which yields matrix critical equations. Radial identities, strict spectral bounds, rank case analysis, and a factor-interchange symmetry then exclude trivial isotropy and show that a Z2 symmetry from an inner involution of trace −2 extends to Z2×Z2. Both main theorems are formalized in Lean 4 with Mathlib.

Results

Up to homothety and isometry, every left-invariant Einstein metric on S^3×S^3 is either the standard product metric or the Jensen nearly Kähler metric. This completes the six-dimensional classification.