The determinant of the elliptic Tate-module representation

For an elliptic curve over a field F, a separably closed extension K, and a prime ℓ invertible in K, the determinant of the action of Gal(K/F) on T_ℓ E is the ℓ-adic cyclotomic character. The statement uses LinearMap.det and is independent of a basis of the Tate module or a generator of ℤ_ℓ(1).

The alternating Weil pairing identifies the determinant action with the action on the Tate twist. This uses the rank-two determinant transformation law LinearMap.det_eq_of_compl₁₂_self_eq_smul from TauCeti.LinearAlgebra.Determinant, together with nondegeneracy of WeierstrassCurve.tateModuleWeilPairing. Cancellation is justified by the rank-one freeness of the Tate twist, so it does not require a perfect-pairing theorem.

Main result

• TauCeti.det_tateModuleGaloisRepresentation: the determinant is the cyclotomic character.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.7–8.

@[simp]

theorem TauCeti.det_tateModuleGaloisRepresentation {F : Type u_1} {K : Type u_2} [Field F] [Field K] [IsSepClosed K] [Algebra F K] {W : WeierstrassCurve F} [W.IsElliptic] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : ↑ℓ ≠ 0) (σ : Gal(K/F)) : LinearMap.det ((W.tateModuleGaloisRepresentation ℓ) σ) = ↑((cyclotomicCharacter K ℓ) σ.toRingEquiv)

The determinant of the elliptic ℓ-adic Galois representation is the cyclotomic character. The extension is allowed to be any separably closed extension of the ground field, and the equality is independent of all choices of bases.