Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Isogeny.TautologicalPoint

The tautological point of a coordinate pullback #

A coordinate pullback p : W₂.CoordinateRing →ₐ[F] W₁.FunctionField — the data underlying an isogeny W₁ ⟶ W₂ — sends the two coordinate functions of W₂ to elements of F(W₁). The Weierstrass relation is exactly what the coordinate ring quotients out, so the pair solves the equation of W₂ over F(W₁), and on an elliptic target that solution is a point. A coordinate pullback therefore cuts out a point of W₂⁄F(W₁), its tautological point, and does so injectively: evaluating the coordinate ring there recovers the pullback it came from.

The pointedness of an isogeny plays no part in any of this, so everything is stated for a bare coordinate pullback; an isogeny φ uses φ.pullback.tautologicalPoint.

For the identity pullback this is the generic point of W, of which the construction here is the pullback-indexed generalisation.

The construction is functorial in F(W₁): post-composing a pullback with an algebra homomorphism into the function field of any third curve is the same as moving its point by the induced map on points. Combined with tautologicalPoint_injective that reflects equality, which is how a fixed-field argument uses a pullback: the condition that a pullback is fixed by an endomorphism, a condition on a whole coordinate ring, becomes one on the two coordinates of a point.

Main definitions #

Main results #

source
noncomputable def TauCeti.CoordinatePullback.tautologicalPoint {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p : CoordinatePullback W₁ W₂) :
(WeierstrassCurve.toAffine (W₂.baseChange W₁.FunctionField)).Point

The tautological point of a coordinate pullback: the point of W₂, with coordinates in the function field of W₁, cut out by the images of the coordinate functions of W₂. They solve the equation of W₂ because the Weierstrass polynomial is what the coordinate ring quotients out.

Equations
Instances For
    source
    theorem TauCeti.CoordinatePullback.tautologicalPoint_ne_zero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p : CoordinatePullback W₁ W₂) :
    p.tautologicalPoint ≠ 0

    The tautological point is affine, never the point at infinity. This is what lets consumers use the coordinate API for nonzero points.

    source
    @[simp]
    theorem TauCeti.CoordinatePullback.xCoord_tautologicalPoint {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p : CoordinatePullback W₁ W₂) :
    p.tautologicalPoint.xCoord = p ((AdjoinRoot.of W₂.polynomial) Polynomial.X)
    source
    @[simp]
    theorem TauCeti.CoordinatePullback.yCoord_tautologicalPoint {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p : CoordinatePullback W₁ W₂) :
    p.tautologicalPoint.yCoord = p (AdjoinRoot.root W₂.polynomial)
    source
    theorem TauCeti.CoordinatePullback.evalAlgHom_tautologicalPoint {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p : CoordinatePullback W₁ W₂) :
    WeierstrassCurve.Affine.CoordinateRing.evalAlgHom ⋯ = p

    Evaluating the coordinate ring at the tautological point recovers the pullback. This is the elimination rule: it turns a statement about the point back into one about the pullback.

    source
    theorem TauCeti.CoordinatePullback.tautologicalPoint_injective {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] :
    Function.Injective tautologicalPoint

    A coordinate pullback is determined by its tautological point. The coordinate ring is generated by its two coordinate functions, so a pullback is fixed by where it sends them.

    source
    @[simp]
    theorem TauCeti.CoordinatePullback.tautologicalPoint_id {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] :
    (id W).tautologicalPoint = W.genericPoint

    The identity pullback's tautological point is the generic point, of which this construction is the pullback-indexed generalisation.

    source
    @[simp]
    theorem TauCeti.CoordinatePullback.tautologicalPoint_comp {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] {W₀ : WeierstrassCurve.Affine F} (p : CoordinatePullback W₁ W₂) (σ : W₁.FunctionField →ₐ[F] W₀.FunctionField) :
    tautologicalPoint (σ.comp p) = (WeierstrassCurve.Affine.Point.map σ) p.tautologicalPoint

    Post-composing with an algebra homomorphism of function fields moves the tautological point by the induced map on points. Both sides are the affine point whose coordinates are the images of the two coordinate functions, so a pullback's interaction with such a homomorphism is read off entirely from its point.

    source
    theorem TauCeti.CoordinatePullback.map_tautologicalPoint_eq_of_apply_eq {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] {Ω : Type u_2} [Field Ω] [Algebra F Ω] [DecidableEq Ω] (p : CoordinatePullback W₁ W₂) (σ τ : W₁.FunctionField →ₐ[F] Ω) (hx : σ (p ((AdjoinRoot.of W₂.polynomial) Polynomial.X)) = τ (p ((AdjoinRoot.of W₂.polynomial) Polynomial.X))) (hy : σ (p (AdjoinRoot.root W₂.polynomial)) = τ (p (AdjoinRoot.root W₂.polynomial))) :
    (WeierstrassCurve.Affine.Point.map σ) p.tautologicalPoint = (WeierstrassCurve.Affine.Point.map τ) p.tautologicalPoint

    Two homomorphisms agreeing on the pullback's two coordinate values move the tautological point to the same place. The point's coordinates are those two values, so the induced map on points cannot see anything else about the homomorphism.