Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Affine.Point.MapEquiv

Transport of elliptic-curve points along an algebra equivalence #

Let W be a Weierstrass curve over a field F. Mathlib's WeierstrassCurve.Affine.Point.map carries the points of W over one F-algebra to its points over another along an algebra homomorphism. This file packages that map, for an F-algebra equivalence K ≃ₐ[F] L, as an additive equivalence of point groups, and proves its identity, composition and inverse laws.

Main definitions #

Main results #

References #

source
noncomputable def WeierstrassCurve.Affine.Point.mapEquiv {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [DecidableEq K] [DecidableEq L] [Algebra F K] [Algebra F L] (W : WeierstrassCurve F) (e : K ≃ₐ[F] L) :
(toAffine (Affine.baseChange W K)).Point ≃+ (toAffine (Affine.baseChange W L)).Point

Transport of elliptic-curve points along an algebra equivalence. This is Mathlib's additive point map, with inverse induced by the inverse algebra equivalence.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.mapEquiv_apply {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [DecidableEq K] [DecidableEq L] [Algebra F K] [Algebra F L] (W : WeierstrassCurve F) (e : K ≃ₐ[F] L) (P : (toAffine (Affine.baseChange W K)).Point) :
    (mapEquiv W e) P = (map ↑e) P

    mapEquiv W e applies Mathlib's point map along e.

    source
    theorem WeierstrassCurve.Affine.Point.mapEquiv_symm_apply {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [DecidableEq K] [DecidableEq L] [Algebra F K] [Algebra F L] (W : WeierstrassCurve F) (e : K ≃ₐ[F] L) (P : (toAffine (Affine.baseChange W L)).Point) :
    (mapEquiv W e).symm P = (map ↑e.symm) P

    The inverse of mapEquiv W e applies Mathlib's point map along e.symm.

    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.mapEquiv_refl {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq K] [Algebra F K] (W : WeierstrassCurve F) :
    mapEquiv W AlgEquiv.refl = AddEquiv.refl (toAffine (Affine.baseChange W K)).Point

    Transport along the identity algebra equivalence is the identity.

    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.mapEquiv_trans {F : Type u_1} {K : Type u_2} {L : Type u_3} {M : Type u_4} [Field F] [Field K] [Field L] [Field M] [DecidableEq K] [DecidableEq L] [DecidableEq M] [Algebra F K] [Algebra F L] [Algebra F M] (W : WeierstrassCurve F) (e : K ≃ₐ[F] L) (f : L ≃ₐ[F] M) :
    mapEquiv W (e.trans f) = (mapEquiv W e).trans (mapEquiv W f)

    Transport along a composite algebra equivalence is the composite of the transports.

    source
    @[simp]
    theorem WeierstrassCurve.Affine.Point.mapEquiv_symm {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] [DecidableEq K] [DecidableEq L] [Algebra F K] [Algebra F L] (W : WeierstrassCurve F) (e : K ≃ₐ[F] L) :
    (mapEquiv W e).symm = mapEquiv W e.symm

    The inverse of the transport along e is the transport along e.symm.