The class-group point map at an affine point

Isogeny.toPointHom φ is defined through class groups: the class of a point is extended into the intermediate ring and normed down to the target coordinate ring. Its geometric reading is that φ sends a point P of W₁ to the point lying under it — the point Q of W₂ whose place is the restriction along φ^* of the place of P. PointHom/Basic.lean proves this when Q is the point at infinity; this file proves it when Q is affine. Together, for a separable isogeny over a separably closed field, they show that the class-group construction computes the value of the rational map at every rational point.

The affine case is a computation of the relative norm of the prime of the intermediate ring over the ideal 𝔮 of Q. The core theorem assumes only that every prime of the intermediate ring over 𝔮 has residue degree one — the condition under which Ideal.relNorm_eq_of_forall_inertiaDeg_eq_one computes that norm — and nothing about F or the separability of φ. Over a separably closed field a separable isogeny splits every place completely (Isogeny.isSplitCompletely), which discharges the condition and gives the corollary.

Main results

• TauCeti.Isogeny.toPointHom_some_eq_some_of_isEquiv_comap_pointPlace_of_forall_inertiaDeg_eq_one: if the place of the affine point P of W₁ restricts along φ to the place of the affine point Q of W₂, and every prime of the intermediate ring over the ideal of Q has inertia degree one, then φ.toPointHom P = Q.
• TauCeti.Isogeny.toPointHom_some_eq_some_of_isEquiv_comap_pointPlace: the same conclusion over a separably closed field for a separable isogeny, where the residue-degree condition always holds.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.3 (the pushforward of divisors along a map of curves, computed by the norm), III.4.8 (an isogeny is a homomorphism on points: the identification of the additive class-group map toPointHom with the map on points that φ^* x₂, φ^* y₂ define is this theorem in the form the repository consumes), and III.4.10 (a separable isogeny over a separably closed field has fibres of full size).

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

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

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

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

theorem TauCeti.Isogeny.toPointHom_some_eq_some_of_isEquiv_comap_pointPlace_of_forall_inertiaDeg_eq_one {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [inst : Algebra W₂.CoordinateRing ↥φ.intermediateRing] (halg : inst = φ.pullbackToIntermediateRing.toAlgebra) {x y : F} (h : W₁.Nonsingular x y) {x' y' : F} (h' : W₂.Nonsingular x' y') (hP : (Valuation.comap (↑φ.fieldPullback) (IsDedekindDomain.HeightOneSpectrum.valuation W₁.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))).IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation W₂.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))) (hf : ∀ Q ∈ (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯).asIdeal.primesOver ↥φ.intermediateRing, Q.inertiaDeg W₂.CoordinateRing = 1) : φ.toPointHom (WeierstrassCurve.Affine.Point.some x y h) = WeierstrassCurve.Affine.Point.some x' y' h'

The class-group point map evaluates at affine points, given trivial residue extensions over the target point. If the place of the affine point (x, y) of W₁ restricts along φ^* to the place of the affine point (x', y') of W₂ — that is, if φ^* x₂ and φ^* y₂ take the values x' and y' at (x, y) — and every prime of the intermediate ring over the ideal of (x', y') has inertia degree one, then φ.toPointHom sends (x, y) to (x', y').

Nothing is assumed of F or of the separability of φ: the residue-degree hypothesis is the whole input beyond the places, and toPointHom_some_eq_some_of_isEquiv_comap_pointPlace discharges it over a separably closed field for a separable isogeny. The algebra structure of W₂.CoordinateRing on the intermediate ring is the caller's, pinned to the pullback one by halg exactly as Isogeny.isScalarTower_intermediateRing pins it, so that the hypothesis can be stated.

theorem TauCeti.Isogeny.toPointHom_some_eq_some_of_isEquiv_comap_pointPlace {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) [IsSepClosed F] [Algebra.IsSeparable (↥φ.fieldPullback.fieldRange) W₁.FunctionField] {x y : F} (h : W₁.Nonsingular x y) {x' y' : F} (h' : W₂.Nonsingular x' y') (hP : (Valuation.comap (↑φ.fieldPullback) (IsDedekindDomain.HeightOneSpectrum.valuation W₁.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))).IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation W₂.FunctionField (WeierstrassCurve.Affine.CoordinateRing.pointPlace ⋯))) : φ.toPointHom (WeierstrassCurve.Affine.Point.some x y h) = WeierstrassCurve.Affine.Point.some x' y' h'

The class-group point map evaluates at affine points. Over a separably closed field, a separable isogeny φ sends the affine point (x, y) of W₁ to the affine point (x', y') of W₂ as soon as the place of (x, y) restricts along φ^* to the place of (x', y') — that is, as soon as φ^* x₂ and φ^* y₂ take the values x' and y' at (x, y).

Together with Isogeny.toPointHom_some_eq_zero_of_isEquiv_comap_infinityPlace this identifies the class-group construction with the map on points that the rational functions φ^* x₂, φ^* y₂ define.