NYLL

theorem · Jacobian varieties

Nondegeneracy of the divisorial Weil pairing

Every nonzero torsion divisor class is detected by a character obtained from supplied divisorial Weil-pairing data.

Nondegeneracy allows torsion divisor classes to be studied through their pairing characters. It is what makes the pairing useful for duality and for constraining automorphisms or Galois actions on torsion. The result belongs to classical abelian-variety duality: Milne's Abelian Varieties, Section 16, describes pairings through divisors and rational functions and relates them to torsion in an abelian variety and its dual.

JacobianVarieties on GitHub ↗

Mathematical statement

Let $K$ be algebraically closed of characteristic $0$, and let $F/K$ have principal-divisor data. Assume there is a transcendental $t\in F$ with $[F:K(t)]<\infty$. For $n\ge1$, let $w$ be divisorial Weil-pairing data on $\operatorname{Pic}^0(F/K)[n]$: its pairing agrees with divisor evaluation, and torsion classes admit rational divisor representatives avoiding any given finite set of places. Then

$$x\longmapsto\bigl(y\longmapsto w(x,y)\bigr)$$

is injective. In particular, $w(x,y)=1$ for every $y$ implies $x=0$.

Lean code

AlgebraicCurve.DivisorialWeilPairingData.toHom_injective_charZero

Published library source ↗Same source in NYLL ↗

theorem toHom_injective_charZero
    {K F : Type*} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Algebra K F] [HasPrincipalDivisors K F]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    {n : ℕ} [NeZero n] (w : DivisorialWeilPairingData K F n) :
    Function.Injective w.toHom
In-scope Lean context
noncomputable section

open AlgebraicCurve

namespace AlgebraicCurve.DivisorialWeilPairingData
Full declaration and proof
/-- In characteristic zero the actual divisorial Weil pairing is
nondegenerate. The auxiliary divisibility of Picard groups is proved by
the existing Jacobian construction, rather than assumed. -/
theorem toHom_injective_charZero
    {K F : Type*} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Algebra K F] [HasPrincipalDivisors K F]
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    {n : ℕ} [NeZero n] (w : DivisorialWeilPairingData K F n) :
    Function.Injective w.toHom := by
  obtain ⟨x, hx, hfin⟩ := hfg
  have hxrange : x ∉ Set.range (algebraMap K F) := by
    rintro ⟨a, rfl⟩
    exact hx (isAlgebraic_algebraMap a)
  obtain ⟨φ, hφ⟩ := FunctionField.exists_ratFuncAlgHom_apply_X_eq hxrange
  let : Algebra (RatFunc K) F := φ.toRingHom.toAlgebra
  have : IsScalarTower K (RatFunc K) F :=
    IsScalarTower.of_algebraMap_eq fun a => (φ.commutes a).symm
  have : FiniteDimensional (RatFunc K) F :=
    JacobianVarieties.Pic0.Proofs.ClosedFieldWeilData.AlgebraicCurve.WC7P.finite_ratFunc_of_adjoin
      φ hφ hfin
  apply w.toHom_injective_of_divisible_coprime_of_isAlgClosed
    (Nat.cast_ne_zero.mpr (NeZero.ne n))
  intro L _ _ _ _ _
  exact Pic0.exists_zsmul_eq_of_finiteDimensional_ratFunc_of_forall_pow_eq_self K 1
    (fun a => ⟨1, Nat.zero_lt_one, by simp only [pow_one]⟩) L
Source credits and license
Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

  1. J. S. Milne. Abelian Varieties. Springer, New York, in Arithmetic Geometry (Storrs, Conn., 1984), Chapter V, 103–150, 1986. Author's revised version dated January 2, 2022; original numbering retained.

Published source: fec50451.

← All selected results in Jacobian varieties