Documentation

LeanPool.KasamiCyclicAdditive.Geometry.BaseChange

Base change of points along a field extension #

basePt K F : E(K) →+ E(F) is the group homomorphism induced by algebraMap K F on points of the Fermat cubic, built the same way as frobPt (via WeierstrassCurve.Affine.Point.baseChange and curveCast). It commutes with frobPt (basePt_frobPt), which is exactly the naturality needed to transport the G-preimage identity from E(K) to E(F) = E(AlgebraicClosure K).

source
noncomputable def KasamiCyclicAdditive.PointFrobenius.basePt (K : Type u_3) (F : Type u_4) [Field K] [DecidableEq K] [Field F] [DecidableEq F] [Algebra K F] :
(FermatCubic.fer K).toAffine.Point →+ (FermatCubic.fer F).toAffine.Point

The group homomorphism E(K) →+ E(F) induced by algebraMap K F.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem KasamiCyclicAdditive.PointFrobenius.basePt_some {K : Type u_1} {F : Type u_2} [Field K] [DecidableEq K] [Field F] [DecidableEq F] [Algebra K F] {x y : K} (hns : (FermatCubic.fer K).toAffine.Nonsingular x y) (hns2 : (FermatCubic.fer F).toAffine.Nonsingular ((algebraMap K F) x) ((algebraMap K F) y)) :
    (basePt K F) (WeierstrassCurve.Affine.Point.some x y hns) = WeierstrassCurve.Affine.Point.some ((algebraMap K F) x) ((algebraMap K F) y) hns2

    basePt sends an affine point to the point with base-changed coordinates.

    source
    theorem KasamiCyclicAdditive.PointFrobenius.basePt_pt {K : Type u_1} {F : Type u_2} [Field K] [DecidableEq K] [CharP K 2] [Field F] [DecidableEq F] [CharP F 2] [Algebra K F] {w t : K} (h : w ^ 3 + t ^ 3 = 1) :
    (basePt K F) (FermatCubic.pt w t h) = FermatCubic.pt ((algebraMap K F) w) ((algebraMap K F) t) ⋯

    basePt maps affine Fermat points to affine Fermat points.

    source
    theorem KasamiCyclicAdditive.PointFrobenius.basePt_ptInf {K : Type u_1} {F : Type u_2} [Field K] [DecidableEq K] [CharP K 2] [Field F] [DecidableEq F] [CharP F 2] [Algebra K F] {a : K} (ha : a ^ 3 = 1) :
    (basePt K F) (FermatCubic.ptInf a ha) = FermatCubic.ptInf ((algebraMap K F) a) ⋯

    basePt maps points at infinity to points at infinity.

    source
    theorem KasamiCyclicAdditive.PointFrobenius.basePt_frobPt {K : Type u_1} {F : Type u_2} [Field K] [DecidableEq K] [CharP K 2] [Field F] [DecidableEq F] [CharP F 2] [Algebra K F] (x : (FermatCubic.fer K).toAffine.Point) :
    (basePt K F) ((frobPt K) x) = (frobPt F) ((basePt K F) x)

    Naturality of basePt with respect to Frobenius.

    source
    theorem KasamiCyclicAdditive.PointFrobenius.basePt_gMap {K : Type u_1} {F : Type u_2} [Field K] [DecidableEq K] [CharP K 2] [Field F] [DecidableEq F] [CharP F 2] [Algebra K F] (a b : ℤ) (x : (FermatCubic.fer K).toAffine.Point) :
    (basePt K F) (Isogeny.gMap (frobPt K) a b x) = Isogeny.gMap (frobPt F) a b ((basePt K F) x)

    Naturality of basePt with respect to gMap.

    source
    theorem KasamiCyclicAdditive.PointFrobenius.basePt_t3 {K : Type u_1} {F : Type u_2} [Field K] [DecidableEq K] [CharP K 2] [Field F] [DecidableEq F] [CharP F 2] [Algebra K F] :
    (basePt K F) (FermatCubic.t3 K) = FermatCubic.t3 F

    basePt commutes with t3.