Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.TateModule.WeilPairing

The ℓ-adic Weil pairing #

Over a separably closed field in which the prime ℓ is invertible, the finite Weil pairings assemble into a continuous, alternating, nondegenerate ℤ_ℓ-bilinear pairing

T_ℓ E × T_ℓ E → ℤ_ℓ(1).

The codomain is TauCeti.PadicTateTwist, not a chosen copy of ℤ_ℓ: keeping the roots of unity makes the Galois equivariance canonical. The pairing is characterized by its projections to μ_{ℓ^n}. Its Galois equivariance is the input for identifying the determinant of the Tate-module representation with the cyclotomic character.

Main results #

References #

source
theorem WeierstrassCurve.instNeZeroNat_tauCeti {ℓ : ℕ} [Fact (Nat.Prime ℓ)] :
NeZero ℓ
source
noncomputable def WeierstrassCurve.tateModuleWeilPairing {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) :
TauCeti.TateModule ℓ W.toAffine.Point →ₗ[ℤ_[ℓ]] TauCeti.TateModule ℓ W.toAffine.Point →ₗ[ℤ_[ℓ]] TauCeti.PadicTateTwist ℓ K

The ℓ-adic Weil pairing, with values in the Tate twist ℤ_ℓ(1), obtained from the compatible finite Weil pairings over a separably closed field in which ℓ is invertible.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem WeierstrassCurve.proj_tateModuleWeilPairing {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) (x y : TauCeti.TateModule ℓ W.toAffine.Point) (n : ℕ) :
    (TauCeti.PadicTateTwist.proj n) (((W.tateModuleWeilPairing hℓ) x) y) = ((TauCeti.Isogeny.weilPairing W (ℓ ^ n) ⋯) ((TauCeti.TateModule.proj n) x)) ((TauCeti.TateModule.proj n) y)

    The finite components of the ℓ-adic pairing are the ordinary Weil pairings.

    source
    @[simp]
    theorem WeierstrassCurve.tateModuleWeilPairing_self {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) (x : TauCeti.TateModule ℓ W.toAffine.Point) :
    ((W.tateModuleWeilPairing hℓ) x) x = 0

    The ℓ-adic Weil pairing is alternating.

    source
    theorem WeierstrassCurve.neg_tateModuleWeilPairing {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) (x y : TauCeti.TateModule ℓ W.toAffine.Point) :
    -((W.tateModuleWeilPairing hℓ) x) y = ((W.tateModuleWeilPairing hℓ) y) x

    The ℓ-adic Weil pairing is skew-symmetric, in additive notation on the Tate twist.

    source
    theorem WeierstrassCurve.tateModuleWeilPairing_nondegenerate {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) {x : TauCeti.TateModule ℓ W.toAffine.Point} (hx : ∀ (y : TauCeti.TateModule ℓ W.toAffine.Point), ((W.tateModuleWeilPairing hℓ) x) y = 0) :
    x = 0

    The ℓ-adic Weil pairing is nondegenerate in its first variable.

    source
    theorem WeierstrassCurve.eq_zero_of_forall_tateModuleWeilPairing_eq_zero {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) {y : TauCeti.TateModule ℓ W.toAffine.Point} (hy : ∀ (x : TauCeti.TateModule ℓ W.toAffine.Point), ((W.tateModuleWeilPairing hℓ) x) y = 0) :
    y = 0

    The ℓ-adic Weil pairing is nondegenerate in its second variable.

    source
    theorem WeierstrassCurve.continuous_tateModuleWeilPairing {K : Type u_1} [Field K] [IsSepClosed K] (W : WeierstrassCurve K) [W.IsElliptic] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) :
    Continuous fun (q : TauCeti.TateModule ℓ W.toAffine.Point × TauCeti.TateModule ℓ W.toAffine.Point) => ((W.tateModuleWeilPairing hℓ) q.1) q.2

    The ℓ-adic Weil pairing is jointly continuous for the inverse-limit topologies.

    source
    theorem WeierstrassCurve.tateModuleWeilPairing_galoisRepresentation {K : Type u_1} [Field K] [IsSepClosed K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) {F : Type u_2} [Field F] [Algebra F K] (E : WeierstrassCurve F) [E.IsElliptic] (σ : Gal(K/F)) (x y : TauCeti.TateModule ℓ (E.baseChange K).toAffine.Point) :
    (((E.baseChange K).tateModuleWeilPairing hℓ) (((E.tateModuleGaloisRepresentation ℓ) σ) x)) (((E.tateModuleGaloisRepresentation ℓ) σ) y) = (TauCeti.PadicTateTwist.galoisRepresentation σ) ((((E.baseChange K).tateModuleWeilPairing hℓ) x) y)

    The ℓ-adic Weil pairing intertwines the elliptic Galois representation with the action on ℤ_ℓ(1). Thus its equivariance does not require choosing a generator of the Tate twist.