The place of a point restricts along [n] to the place of its multiple

An affine point P of W has a place of F(W), and pulling that place back along the function-field map of [n] gives a valuation of F(W) again. This file identifies it: it is equivalent to the place of n • P, which is the place at infinity when n • P = 0. So among the places attached to the F-rational points of W, those above the place of a point T, for the covering [n], are the places of the [n]-preimages of T. A fibre can also contain places of higher degree, which are not attached to points and are not treated here; over an algebraically closed field there are none. That is what turns the pullback of a divisor along [n] into a sum over a fibre, which is the form in which the divisor construction of the Weil pairing uses it.

The restricted valuation need not be normalized, since [n] can multiply orders, which is why the statements are equivalences rather than equalities.

Main results

• TauCeti.Isogeny.isEquiv_comap_pointPlace: the place of P restricted along [n] is equivalent to the place of n • P, when n • P is affine.
• TauCeti.Isogeny.isEquiv_comap_pointPlace_infinityPlace_iff: the place of an affine point P restricts to the place at infinity exactly when n • P = 0, over any field.
• TauCeti.Isogeny.isEquiv_comap_pointPlace_iff: and conversely, the place of an affine point restricts to the place of T only if the point is an [n]-preimage of T, so the affine F-rational places over the place of T are exactly those of its [n]-preimages.
• TauCeti.Isogeny.isEquiv_comap_valuation_pointEquivDegreeOnePlace_iff: the same for every pair of points, read through the point--place dictionary, the point at infinity included.
• TauCeti.Isogeny.finite_setOf_zsmul_eq: the fibre {R | n • R = T} is finite.
• TauCeti.Isogeny.restrict_eq_pointEquivDegreeOnePlace_iff: over a separably closed field, the places over the place of T are exactly the places of its [n]-preimages, since [n] splits every place completely.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, III.1.
• J. Silverman, The Arithmetic of Elliptic Curves, II.2.

The construction follows TauCeti.Isogeny.isEquiv_comap_infinityPlace (TauCeti/AlgebraicGeometry/EllipticCurve/Isogeny/InfinityPlace.lean), the same statement for the place at infinity; the ordering of the argument, and the choice to work at the Valuation.comap level rather than through Place.restrict, are taken from there.

Prior art

The same statement for [ℓ] is proved in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), projects/HasseWeil/HasseWeil/Foundation/EC/MulByIntSamePlace.lean, which also covers the case of a point that [ℓ] sends to infinity. Nothing here is adapted from it: that proof identifies the two valuation rings directly, via Valuation.isEquiv_of_val_le_one and the division-polynomial group law, where this one takes the centre of the normalized restriction on the coordinate ring.

theorem TauCeti.Isogeny.instIsDedekindDomainCoordinateRingToAffine {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] : IsDedekindDomain W.toAffine.CoordinateRing

Ellipticity already makes the coordinate ring integrally closed, hence a Dedekind domain. Deriving it here as a local instance — the pattern Affine/FunctionField/PointPlace.lean uses — keeps the assumption out of the exported signatures instead of making every caller supply it.

theorem TauCeti.Isogeny.isEquiv_comap_pointPlace {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] {x y : F} (h : W.toAffine.Nonsingular x y) {n : ℤ} {x' y' : F} (h' : W.toAffine.Nonsingular x' y') (hnP : n • WeierstrassCurve.Affine.Point.some x y h = WeierstrassCurve.Affine.Point.some x' y' h') : (Valuation.comap (mulByIntIsogenyOfNeZero W ⋯).fieldPullback.toRingHom (IsDedekindDomain.HeightOneSpectrum.valuation W.toAffine.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))).IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation W.toAffine.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))

The place of P restricts along [n] to the place of n • P, for an affine n • P. The case n • P = 0 is isEquiv_comap_pointPlace_infinityPlace_iff.

theorem TauCeti.Isogeny.isEquiv_comap_pointPlace_infinityPlace_of_zsmul_eq_zero {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] {x y : F} (h : W.toAffine.Nonsingular x y) {n : ℤ} (hn : psiFunctionField W n ≠ 0) (hnP : n • WeierstrassCurve.Affine.Point.some x y h = 0) : (Valuation.comap (mulByIntIsogeny W hn).fieldPullback.toRingHom (IsDedekindDomain.HeightOneSpectrum.valuation W.toAffine.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))).IsEquiv W.toAffine.infinityPlace

The place of an affine n-torsion point restricts along [n] to the place at infinity. For P = (x, y) with n • P = 0, the valuation z ↦ v_P([n]^* z) of F(W) is equivalent to the place at infinity: [n]*x = Φₙ/ΨSqₙ has a pole at P. No closure hypothesis on F is needed.

@[simp]

theorem TauCeti.Isogeny.isEquiv_comap_pointPlace_infinityPlace_iff {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] {x y : F} (h : W.toAffine.Nonsingular x y) {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (Valuation.comap (↑(mulByIntIsogeny W hn).fieldPullback) (IsDedekindDomain.HeightOneSpectrum.valuation W.toAffine.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))).IsEquiv W.toAffine.infinityPlace ↔ n • WeierstrassCurve.Affine.Point.some x y h = 0

The affine points over the place at infinity are the n-torsion points. For an F-rational affine point P, the place of P restricts along [n] to the place at infinity exactly when n • P = 0.

@[simp]

theorem TauCeti.Isogeny.isEquiv_comap_pointPlace_iff {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] {x y : F} (h : W.toAffine.Nonsingular x y) {n : ℤ} (hn : psiFunctionField W n ≠ 0) {x' y' : F} (h' : W.toAffine.Nonsingular x' y') : (Valuation.comap (↑(mulByIntIsogeny W hn).fieldPullback) (IsDedekindDomain.HeightOneSpectrum.valuation W.toAffine.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))).IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation W.toAffine.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯)) ↔ n • WeierstrassCurve.Affine.Point.some x y h = WeierstrassCurve.Affine.Point.some x' y' h'

The affine points over the place of T are its [n]-preimages. For F-rational affine points P and T, the place of P restricts along [n] to the place of T precisely when n • P = T.

theorem TauCeti.Isogeny.isEquiv_comap_valuation_pointEquivDegreeOnePlace_iff {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (R T : W.toAffine.Point) : (Valuation.comap (mulByIntIsogeny W hn).fieldPullback.toRingHom (↑(W.toAffine.pointEquivDegreeOnePlace R)).valuation).IsEquiv (↑(W.toAffine.pointEquivDegreeOnePlace T)).valuation ↔ n • R = T

The places over the place of T along [n] are the places of the [n]-preimages of T, among the places of points.

theorem TauCeti.Isogeny.finite_setOf_zsmul_eq {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (T : W.toAffine.Point) : {R : W.toAffine.Point | n • R = T}.Finite

The [n]-fibre over a point is finite: the places of its points lie over the place of T, and a place has finitely many places above it in the finite extension [n].

theorem TauCeti.Isogeny.restrict_eq_pointEquivDegreeOnePlace_iff {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) [W.IsElliptic] [IsSepClosed F] {n : ℤ} (hchar : ↑n ≠ 0) (T : W.toAffine.Point) (P : Place F W.toAffine.FunctionField) : Place.restrict F W.toAffine.FunctionField P = ↑(W.toAffine.pointEquivDegreeOnePlace T) ↔ ∃ (R : W.toAffine.Point), n • R = T ∧ ↑(W.toAffine.pointEquivDegreeOnePlace R) = P

The places over the place of T along [n] are the places of its [n]-preimages, over a separably closed field in which n is invertible: a place above a point place has degree one, since [n] splits every place completely.