The tautological point of 1 − π

The tautological point is additive on morphisms, and the identity's is the generic point, so the tautological point of 1 − π_q is the generic point minus that of Frobenius.

Transported into an extension Ω of F along a homomorphism σ of the function field, that reads Q − Q^q for Q = σ(g) the image there of the generic point. This is the form the embedding count of 1 − π_q is built from, and the rest of the file draws the two consequences it needs. The left-hand side depends on σ only through the pulled-back field, so two homomorphisms agreeing there give points Q_σ, Q_τ whose difference is fixed by the q-power map; and a point of W over Ω fixed by that map descends to a point over F. Together these say that the embeddings over the pulled-back field are indexed injectively by rational points, which is what bounds the degree of 1 − π_q by the point count.

Main results

• TauCeti.Isogeny.tautologicalPoint_oneSubFrobeniusIsogeny: the tautological point of 1 − π_q is g − π_q(g).
• TauCeti.Isogeny.map_tautologicalPoint_oneSubFrobeniusIsogeny: transported along σ, it is Q − Q^q.
• TauCeti.Isogeny.map_frobeniusAlgHom_sub_map_genericPoint_eq_self: two homomorphisms agreeing on the pulled-back field move the generic point by a q-power-fixed difference.
• TauCeti.Isogeny.exists_baseChange_eq_sub_map_genericPoint: that difference is the image of a rational point.

theorem TauCeti.Isogeny.tautologicalPoint_oneSubFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] : (oneSubFrobeniusIsogeny W).pullback.tautologicalPoint = W.genericPoint - (frobeniusIsogeny W).pullback.tautologicalPoint

The tautological point of 1 − π_q is the generic point minus that of Frobenius.

theorem TauCeti.Isogeny.map_tautologicalPoint_oneSubFrobeniusIsogeny {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {Ω : Type u_2} [Field Ω] [DecidableEq Ω] [Algebra F Ω] (σ : W.FunctionField →ₐ[F] Ω) : (WeierstrassCurve.Affine.Point.map σ) (oneSubFrobeniusIsogeny W).pullback.tautologicalPoint = (WeierstrassCurve.Affine.Point.map σ) W.genericPoint - (WeierstrassCurve.Affine.Point.map (FiniteField.frobeniusAlgHom F Ω)) ((WeierstrassCurve.Affine.Point.map σ) W.genericPoint)

The tautological point of 1 − π_q, transported into any extension, is Q − Q^q for Q the image there of the generic point. This is the form the embedding count needs: the left side depends on the homomorphism only through the pulled-back field, while the right side is visibly a difference of a point and its q-power image.

theorem TauCeti.Isogeny.map_frobeniusAlgHom_sub_map_genericPoint_eq_self {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {Ω : Type u_2} [Field Ω] [DecidableEq Ω] [Algebra F Ω] (σ τ : W.FunctionField →ₐ[F] Ω) (h : ∀ z ∈ (oneSubFrobeniusIsogeny W).fieldPullback.fieldRange, σ z = τ z) : (WeierstrassCurve.Affine.Point.map (FiniteField.frobeniusAlgHom F Ω)) ((WeierstrassCurve.Affine.Point.map σ) W.genericPoint - (WeierstrassCurve.Affine.Point.map τ) W.genericPoint) = (WeierstrassCurve.Affine.Point.map σ) W.genericPoint - (WeierstrassCurve.Affine.Point.map τ) W.genericPoint

Two homomorphisms that agree on the pulled-back field move the generic point to points whose difference is q-power fixed. Their images of the tautological point of 1 − π_q agree, and that image is Q − Q^q, so the two Q's differ by a Frobenius-fixed point.

theorem TauCeti.Isogeny.exists_baseChange_eq_sub_map_genericPoint {F : Type u_1} [Field F] [Finite F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {Ω : Type u_2} [Field Ω] [DecidableEq Ω] [Algebra F Ω] [DecidableEq F] (σ τ : W.FunctionField →ₐ[F] Ω) (h : ∀ z ∈ (oneSubFrobeniusIsogeny W).fieldPullback.fieldRange, σ z = τ z) : ∃ (P : (WeierstrassCurve.toAffine (W.baseChange F)).Point), (WeierstrassCurve.Affine.Point.baseChange F Ω) P = (WeierstrassCurve.Affine.Point.map σ) W.genericPoint - (WeierstrassCurve.Affine.Point.map τ) W.genericPoint

That difference descends to a rational point. A point over an extension fixed by the q-power map comes from the base field, so two homomorphisms agreeing on the pulled-back field move the generic point by a rational point.