Documentation

Atlas.AlgebraicGeometryI.code.Cor21Genus1Group

source
def WeierstrassCurve.Affine.arithmeticGenus {F : Type u_1} [Field F] :
Affine F → ℕ

The arithmetic genus of any affine Weierstrass curve, fixed at 1.

Instances For
    source
    structure IsSmooth_Genus1 {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) :
    Prop

    Predicate witnessing that an affine Weierstrass curve is smooth (elliptic) and of genus 1.

    Instances For
      source
      theorem isSmooth_Genus1_of_isElliptic {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [hW : WeierstrassCurve.IsElliptic W] :
      IsSmooth_Genus1 W

      Every elliptic Weierstrass curve satisfies the IsSmooth_Genus1 predicate.

      source
      @[reducible]
      def corollary21_genus1_group {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (hg1 : IsSmooth_Genus1 W) :
      AddCommGroup W.Point

      Corollary 21 (Lec 17): a smooth (elliptic) curve of genus 1 carries a canonical abelian group structure on its points.

      Instances For
        source
        theorem corollary21_genus1_abelJacobi_surjective {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (hg1 : IsSmooth_Genus1 W) :
        Function.Surjective ⇑WeierstrassCurve.Affine.Point.toClass

        The Abel-Jacobi map Point → Pic⁰ from points on a smooth genus 1 curve to its class group is surjective.

        source
        theorem corollary21_genus1_abelJacobi_bijective {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) (hg1 : IsSmooth_Genus1 W) :
        Function.Bijective ⇑WeierstrassCurve.Affine.Point.toClass

        The Abel-Jacobi map for a smooth genus 1 curve is bijective; combined with its group structure, this realizes the curve as an elliptic curve.