Compatibility of the class-group point map with places

For a separable isogeny over a separably closed field, the place of the image of a point under Isogeny.toPointHom is the restriction of its place along the function-field pullback. The proof combines the affine-point evaluation theorem with the point at infinity.

Main results

• TauCeti.Isogeny.coe_pointEquivDegreeOnePlace_toPointHom: the point map commutes with restriction of places.
• TauCeti.Isogeny.valuation_fieldPullback_lt_one_of_toPointHom_eq_some: the pullback of a function vanishing at φ(Q) vanishes at Q.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4.10.

theorem TauCeti.Isogeny.instIsIntegrallyClosedCoordinateRing_2 {F : Type u_1} [Field F] {W₁ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] : IsIntegrallyClosed W₁.CoordinateRing

theorem TauCeti.Isogeny.instIsIntegrallyClosedCoordinateRing_3 {F : Type u_1} [Field F] {W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] : IsIntegrallyClosed W₂.CoordinateRing

theorem TauCeti.Isogeny.instIsDedekindDomainCoordinateRing_3 {F : Type u_1} [Field F] {W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] : IsDedekindDomain W₂.CoordinateRing

@[simp]

theorem TauCeti.Isogeny.coe_pointEquivDegreeOnePlace_toPointHom {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] [Algebra W₂.FunctionField W₁.FunctionField] (hφ : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) (P : W₁.Point) : ↑(W₂.pointEquivDegreeOnePlace (φ.toPointHom P)) = Place.restrict F W₂.FunctionField ↑(W₁.pointEquivDegreeOnePlace P)

The place of the image of a point is the restriction of the point's place along the isogeny's function-field pullback.

theorem TauCeti.Isogeny.valuation_fieldPullback_lt_one_of_toPointHom_eq_some {F : Type u_1} [Field F] [DecidableEq F] [IsSepClosed F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] {Q : W₁.Point} {x' y' : F} {h' : W₂.Nonsingular x' y'} (hQ : φ.toPointHom Q = WeierstrassCurve.Affine.Point.some x' y' h') {z : W₂.FunctionField} (hz : (Place.ofPrime F W₂.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯)).valuation z < 1) : (↑(W₁.pointEquivDegreeOnePlace Q)).valuation (φ.fieldPullback z) < 1

The pullback of a function vanishing at φ(Q) vanishes at Q: if φ sends Q to the affine point (x', y') and z vanishes there, then φ^* z vanishes at Q.