Module

CharZeroNondegeneracy.lean

Nyll.JacobianVarieties.WeilPairing.CharZeroNondegeneracy

1 declaration indexed from sourceView source ↗

Module documentation

Nondegeneracy of the divisorial Weil pairing in characteristic zero

The divisibility input in the existing Kummer detection proof is supplied by the proved geometric Jacobian construction and multiplication surjectivity, for every finite rational-function-field extension. No divisibility or nondegeneracy hypothesis is left to the caller.

Imports4

Imported by2

theorem

toHom_injective_charZero

L30 ↗

AlgebraicCurve.DivisorialWeilPairingData.toHom_injective_charZero

Documentation

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.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve.DivisorialWeilPairingData

Lean source · statement

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

Module documentation

Nondegeneracy of the divisorial Weil pairing in characteristic zero

Declarations

toHom_injective_charZero