`Definitions/Def_EllipticCurve_ZeroComponentAt.lean`

Points in the identity component at a place of $Q$

The module defines a single predicate, WeierstrassCurve.InZeroComponentAt W A P. Its data are: a Weierstrass curve W over \mathbb{Z} (a bare Weierstrass equation, with no minimality or nonsingularity assumption); a valuation subring A of \overline{\mathbb{Q}}, i.e. a place of \overline{\mathbb{Q}}, with its maximal ideal and residue field k_A = IsLocalRing.ResidueField A; and a point P of the affine point type of W base changed along \mathbb{Z}\to\mathbb{Q} and then to \overline{\mathbb{Q}}. The predicate is the disjunction of the following cases. Either P is the point at infinity 0; or P is an affine point .some x y h with coordinates x,y\in\overline{\mathbb{Q}} and a proof h that (x,y) is a nonsingular point of the base-changed affine equation, and then one of two further conditions holds: (i) x\notin A, i.e. the abscissa is not A-integral; or (ii) both x\in A and y\in A, and the images \bar x,\bar y of x,y under the residue map A\to k_A form a nonsingular point of the affine curve obtained by reducing the integral model W modulo the maximal ideal of A (that is, of W mapped along \mathbb{Z}\to k_A).

Thus the predicate is stated relative to the chosen integral Weierstrass model W and to the chosen place A, and it is a bare Prop: nothing here asserts that the points satisfying it form a subgroup, nor that A-integrality of x forces that of y (condition (ii) demands both). For a model minimal at the residue characteristic of A, case (i) describes the kernel of reduction and case (ii) the points reducing into the smooth locus, so that the predicate cuts out the classical subgroup E_0 of points reducing to nonsingular points; the group-theoretic and reduction-theoretic properties are proved elsewhere as separate theorems.

Relation to Mathlib

Built entirely from Mathlib notions — WeierstrassCurve, its base change and affine points, Nonsingular, ValuationSubring and IsLocalRing.ResidueField with its residue map — but Mathlib has no notion of the identity component or of the reduction of a point at a place, so this predicate is the project's own.

Where it is used

The predicate is used in the local analysis of torsion points on the integral Frey model: at primes of multiplicative reduction and at p one asks whether a point of order p lies on the identity component, and this feeds Mazur's Eisenstein-ideal argument showing that the mod-p representation of the Frey curve has no cofixed line for p\ge 17 (including the global input WeierstrassCurve.mazurStepThree_not_inZeroComponentAt).

References

J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 2nd ed., 2009, Chapter VII
B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

23 lines
1 declarations
used in the statements of 43 theorems and imported by 50 proofs
imports 1 definition modules

Source file: Definitions/Def_EllipticCurve_ZeroComponentAt.lean

Imports

Def_FLTPrelim_GaloisRep

Imported by

Def_ModularCurve_MazurStepThree

Declarations

defWeierstrassCurve.InZeroComponentAt

Source

import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point ↗
import Mathlib.RingTheory.Valuation.ValuationSubring ↗
import Mathlib.RingTheory.LocalRing.ResidueField.Basic ↗
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure ↗
import Definitions.Def_FLTPrelim_GaloisRep

set_option autoImplicit false

namespace WeierstrassCurve

open scoped WeierstrassCurve.Affine

def InZeroComponentAt (W : WeierstrassCurve ℤ) (A : ValuationSubring (AlgebraicClosure ℚ))
    (P : ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).Point) : Prop :=
  P = 0 ∨ ∃ (x y : AlgebraicClosure ℚ)
      (h : ((W.map (Int.castRingHom ℚ))⁄(AlgebraicClosure ℚ)).toAffine.Nonsingular x y),
    P = .some x y h ∧
      (x ∉ A ∨ ∃ (hx : x ∈ A) (hy : y ∈ A),
        (W.map (Int.castRingHom (IsLocalRing.ResidueField A))).toAffine.Nonsingular
          (IsLocalRing.residue A ⟨x, hx⟩) (IsLocalRing.residue A ⟨y, hy⟩))

end WeierstrassCurve

Definitions/Def_EllipticCurve_ZeroComponentAt.lean

Points in the identity component at a place of Q​