Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Isogeny.Dual.Torsion

Kernels of dual isogenies and degree torsion #

For an isogeny φ : W₁ → W₂, the identity φ̂ ∘ φ = [deg φ] gives an exact sequence ker φ → W₁[deg φ] → ker φ̂. The first map is inclusion and the second is induced by φ. Over a separably closed field, if φ is separable, the second map is surjective. If φ̂ is separable, applying this to the dual lifts every point of ker φ through φ̂ on degree torsion.

These are the native-point counterparts of TauCeti.Isogeny.kerCoeffToTorsionCoeff and TauCeti.Isogeny.torsionCoeffToDualKerCoeff in TauCeti.AlgebraicGeometry.EllipticCurve.GaloisCohomology.Isogeny.Torsion. There TauCeti.Isogeny.torsionShortExact packages the same sequence over a separable closure as discrete Galois modules. Here the maps are defined over any field, without coefficient or cohomology imports; surjectivity only needs separability of the relevant isogeny.

References #

source
theorem TauCeti.Isogeny.nsmul_eq_zero_of_mem_ker_pointMapHom {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) {P : W₁.Point} (hP : P ∈ (Hom.ofIsogeny φ).pointMapHom.ker) :
φ.degree • P = 0

A point killed by an isogeny is killed by its degree.

source
noncomputable def TauCeti.Isogeny.kerToTorsion {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) :
↥(Hom.ofIsogeny φ).pointMapHom.ker →+ ↥(Submodule.torsionBy ℤ W₁.Point ↑φ.degree)

The inclusion of an isogeny's kernel in the torsion subgroup at its degree.

Instances For
    source
    @[simp]
    theorem TauCeti.Isogeny.coe_kerToTorsion {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (P : ↥(Hom.ofIsogeny φ).pointMapHom.ker) :
    ↑(φ.kerToTorsion P) = ↑P

    Inclusion in degree torsion does not change the underlying point.

    source
    theorem TauCeti.Isogeny.pointMap_kerToTorsion {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (P : ↥(Hom.ofIsogeny φ).pointMapHom.ker) :
    (Hom.ofIsogeny φ).pointMap ↑(φ.kerToTorsion P) = 0

    The isogeny kills every point in the image of its kernel inclusion.

    source
    theorem TauCeti.Isogeny.kerToTorsion_injective {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) :
    Function.Injective ⇑φ.kerToTorsion

    The map from the kernel to degree torsion is injective.

    source
    noncomputable def TauCeti.Isogeny.torsionToDualKer {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) :
    ↥(Submodule.torsionBy ℤ W₁.Point ↑φ.degree) →+ ↥(Hom.ofIsogeny φ.dual).pointMapHom.ker

    The map from degree torsion to the dual kernel, R ↦ φ R.

    Instances For
      source
      @[simp]
      theorem TauCeti.Isogeny.coe_torsionToDualKer {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (R : ↥(Submodule.torsionBy ℤ W₁.Point ↑φ.degree)) :
      ↑(φ.torsionToDualKer R) = (Hom.ofIsogeny φ).pointMap ↑R

      The map to the dual kernel is the original isogeny on underlying points.

      source
      theorem TauCeti.Isogeny.dual_pointMap_mem_ker_pointMapHom {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (S : ↥(Submodule.torsionBy ℤ W₂.Point ↑φ.degree)) :
      (Hom.ofIsogeny φ.dual).pointMap ↑S ∈ (Hom.ofIsogeny φ).pointMapHom.ker

      The dual sends degree torsion into the original kernel.

      source
      @[simp]
      theorem TauCeti.Isogeny.torsionToDualKer_eq_zero_iff {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (R : ↥(Submodule.torsionBy ℤ W₁.Point ↑φ.degree)) :
      φ.torsionToDualKer R = 0 ↔ (Hom.ofIsogeny φ).pointMap ↑R = 0

      The kernel of the map from degree torsion consists exactly of the points killed by φ.

      source
      theorem TauCeti.Isogeny.mem_range_kerToTorsion_iff {F : Type u_1} [Field F] [DecidableEq F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) (R : ↥(Submodule.torsionBy ℤ W₁.Point ↑φ.degree)) :
      R ∈ φ.kerToTorsion.range ↔ (Hom.ofIsogeny φ).pointMap ↑R = 0

      The image of the kernel inclusion is exactly the degree-torsion points killed by φ. Together with torsionToDualKer_eq_zero_iff, this expresses exactness at degree torsion.

      source
      theorem TauCeti.Isogeny.torsionToDualKer_surjective {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] :
      Function.Surjective ⇑φ.torsionToDualKer

      For a separable isogeny, every point of the dual kernel is the image under φ of a degree-torsion point.

      source
      theorem TauCeti.Isogeny.exists_dual_pointMap_eq_of_mem_ker {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 (↥φ.dual.fieldPullback.fieldRange) W₂.FunctionField] {P : W₁.Point} (hP : P ∈ (Hom.ofIsogeny φ).pointMapHom.ker) :
      ∃ (S : ↥(Submodule.torsionBy ℤ W₂.Point ↑φ.degree)), (Hom.ofIsogeny φ.dual).pointMap ↑S = P

      If the dual is separable, every point killed by φ lifts through φ̂ on degree torsion.