3 Toric heights

The height is defined from the fan of \(S\). We retain the paper’s notation: \(v_0,v_1,v_2\) are its primitive rays, \(M_E\) is the character lattice, and \(\ell _w\) is the local logarithm map. At a finite place, this map records the normalized valuations of characters; at the infinite place it records their logarithmic absolute values. The local height is the exponential of the corresponding piecewise linear support function. We write \(e_1=X+Y+Z\), \(e_2=XY+YZ+ZX\), and \(e_3=XYZ\). In the affine chart, \(\varepsilon =e_1=X+Y+Z\).

Proposition 1 The local logarithm

✓

Let \(w\) be a place of \(E\) lying over a place \(v\) of \(\mathbb {Q}\). There is an exact sequence

\begin{equation*} 1 \longrightarrow K_v^{\mathrm{max}} \longrightarrow T(\mathbb {Q}_v) \xrightarrow {\ell _w} \mathfrak t_w. \end{equation*}

If \(w\) is infinite then \(\ell _w\) is surjective, and if \(w\) is finite then the image of \(\ell _w\) is the lattice \(X_\ast (T_{E})^{\Gamma (w/v)}\).

Proof in Lean ▼

Express torus points by characters over the splitting field. Applying the normalized valuation gives the finite-place image lattice and compact kernel. The logarithmic absolute value gives the analogous statement at infinity.

Equation 5

✓

\begin{equation*} H(x,\varphi ) = \prod _{v \in Pl_\mathbb {Q}} q_v^{-\frac{1}{e_v}\varphi (\ell _w(x_v)) } \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Lemma 1 Weight vectors

✓

Let \(\mathbf1\) denote the global section in \(H^0(S_E,\mathcal O(3D_0))\) associated to the effective Cartier divisor \(3D_0\), namely the image of \(1\) under the natural inclusion \(\mathcal O_{S_E}\hookrightarrow \mathcal O_{S_E}(3D_0)\). The space \(H^0(S_E,\mathcal O(3D_0))\) is spanned over \(E\) by the following four weight vectors:

\begin{align*} & \mathbf1,\qquad (1-3e_2e_1^{-2})\mathbf1, \\ & (e_1^3-\tfrac 92 e_1 e_2+ \tfrac {27}{2} e_3 + \tfrac {\sqrt{-27}}{2} \sqrt{\mathrm{disc}}) e_1^{-3}\mathbf1,\qquad (e_1^3-\tfrac 92 e_1 e_2+ \tfrac {27}{2} e_3 - \tfrac {\sqrt{-27}}{2} \sqrt{\mathrm{disc}}) e_1^{-3}\mathbf1 \end{align*}

where \(\sqrt{\mathrm{disc}} \mathrel {:=}(X-Z)(Y-X)(Z-Y)\). The associated characters of \(T_E\) are, respectively,

\begin{equation*} 1,\quad \chi ^{a'+b'},\quad \chi ^{2a'+b'},\quad \chi ^{2b'+a'} \end{equation*}

where \(a' = 2v_1^\vee - v_2^\vee \) and \(b' = 2v_2^\vee - v_1^\vee \) in the character lattice \(M_E = X^\ast T_E\) and \((v_1^\vee ,v_2^\vee )\) is the dual basis to \((v_1,v_2)\).

Proof in Lean ▼

Compute the invariant cubic forms, divide by \(e_1^3\), and diagonalize the torus action. The four displayed forms and their characters give the required basis of sections.

Equation 6

✓

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 7

✓

\begin{equation*} \chi ^{a'+b'}(uv_0’ + vv_1’+wv_2’) = \frac{vw}{u^2} = \frac{(X+\zeta Y+\zeta ^2 Z)(X+\zeta ^2 Y+\zeta Z)}{(X+Y+Z)^2} = \frac{e_1^2-3e_2}{e_1^2} \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 8

✓

\begin{equation*} \chi ^{2b'+a'}(uv_0’ + vv_1’+wv_2’) =\frac{w^3}{u^3} = \frac{e_1^3-\tfrac 92 e_1 e_2+ \tfrac {27}{2} e_3 - \tfrac {\sqrt{-27}}{2} \sqrt{\mathrm{disc}}}{e_1^3} \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Lemma 2 Integral points in the affine chart

✓

Write \(e_2,e_3,\delta \) for the dehomogenized invariants

\[ e_2=\frac{XY+YZ+ZX}{\varepsilon ^2},\qquad e_3=\frac{XYZ}{\varepsilon ^3},\qquad \delta =\frac{X^2Y+Y^2Z+Z^2X}{\varepsilon ^3}. \]

Then

\begin{equation*} \mathbb {Z}[X/\varepsilon ,Y/\varepsilon ]^{C_3} =\mathbb {Z}[e_2,e_3,\delta ]. \end{equation*}

A rational point \(P\) of \(S\setminus D_0\) is integral if and only if \(e_2(P),e_3(P)\in \mathbb {Z}\).

Proof in Lean ▼

Compute the cyclic invariants in the affine chart. The invariant relation makes \(\delta \) integral over \(\mathbb {Z}[e_2,e_3]\), so integral values of \(e_2,e_3\) force the rational value of \(\delta \) to be integral.

Equation 9

✓

\begin{equation*} \mathbb {Z}[X/\varepsilon ,Y/\varepsilon ]^{C_3} =\mathbb {Z}[e_2,e_3,\delta ]. \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 10

✓

\begin{equation*} \mathbb {Z}[X,Y,Z]^{C_3} =\mathbb {Z}[e_1,e_2,e_3,X^2Y+Y^2Z+Z^2X] \end{equation*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Proposition 2 Integral coefficients and toric height

✓

The characteristic polynomial \(f = t^3-t^2+at+b \in \mathbb {Q}[t]\) of a rational point \((K/\mathbb Q,x) \in T(\mathbb Q)\) has integer coefficients if and only if \((K/\mathbb Q,x)\) is integral. For any integral rational point \((K/\mathbb {Q},x)\) on \(T\),

\begin{equation*} H((K/\mathbb Q,x),\mathcal O(D_0)) = \sqrt{1-3a}. \end{equation*}

Proof in Lean ▼

Apply the invariant-ring criterion to the characteristic polynomial. Evaluate the local height factors; their product reduces to \(\sqrt{1-3a}\).

Equation 11

✓

\begin{align*} \max \Bigg( 1, |1-3e_2|_w, & \left| 1-\tfrac {9}{2} e_2+ \tfrac {27}{2} e_3 - \tfrac {\sqrt{-27}}{2} \sqrt{\mathrm{disc}} \right|_w, \\ & \left| 1-\tfrac {9}{2} e_2+ \tfrac {27}{2} e_3 + \tfrac {\sqrt{-27}}{2} \sqrt{\mathrm{disc}} \right|_w \Bigg)^{\frac{1}{[E:\mathbb {Q}]}} \end{align*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Equation 12

✓

\begin{align*} \max \left( 1, |1-3e_2|^2, \left|1-\tfrac 92 e_2+ \tfrac {27}{2} e_3 + \tfrac {\sqrt{-27}}{2} \sqrt{\mathrm{disc}}\right|^2 \right)^{1/2}. \end{align*}

Proof in Lean ▼

The linked Lean proof establishes this statement.

Lemma 3 Comparing heights

✓

Let \(P=(K/\mathbb {Q},x)\) be an integral rational point of \(T\) with characteristic polynomial \(f=t^3-t^2+at+b\in \mathbb {Z}[t]\). Write \(H_{\mathrm{tor}}(f)=H(P,\mathcal O(D_0))\) for its toric height and set \(h(f)=\max (|a|^{1/2},|b|^{1/3})\), so that \(H(f)=\max \{ 1,h(f)\} \). Then \(a\leq 0\) and

\begin{equation*} h(f)^2=-a, \qquad H_{\mathrm{tor}}(f)^2=1+3h(f)^2, \end{equation*}

so for every \(B\geq 0\),

\begin{equation*} h(f)\leq B \quad \Longleftrightarrow \quad H_{\mathrm{tor}}(f)\leq \sqrt{1+3B^2}. \end{equation*}

In particular, \(H_{\mathrm{tor}}(f)\asymp H(f)\). The only polynomial here with \(h(f)=0\) is \(t^3-t^2\), for which \(H_{\mathrm{tor}}(f)=1\).

Proof in Lean ▼

The three roots are real. The resulting coefficient inequalities give \(a\leq 0\) and \(|b|^{2/3}\leq -a\). Substitute this into the root-height definition and use the toric-height formula.