Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.Scheme.Geom.ExactOrder.Basic

Points of exact order N on an elliptic curve #

Let E be an elliptic curve over a scheme S and P an S-point of E. Following Katz and Mazur, P has exact order N when the relative effective Cartier divisor

D = [P] + [2P] + ⋯ + [NP]

on E is a subgroup scheme of E. This is Drinfeld's notion of a point of exact order N, and it is the definition of a [Γ₁(N)]-structure over an arbitrary base. It is not a condition on the order of P in a group of points: over a base of characteristic p, the divisor p[0] is the kernel of the relative Frobenius of E, so the zero section has exact order p.

Each [aP] is the divisor of the section aP of the smooth separated curve E ⟶ S, cut out by its ideal sheaf, and the sum of divisors is the product of ideal sheaves (EllipticCurveGeom.multiplesDivisor), the divisor of the family of points P, 2P, …, NP (EllipticCurveGeom.multiplesDivisor_eq_pointsDivisor). The subgroup condition asks that the closed subscheme D carry a group-scheme structure for which its inclusion into E is a homomorphism (EllipticCurveGeom.IsOfExactOrder); by the closed-subgroup criterion this says that the ideal sheaf of D vanishes on the identity, on the sum of two points of D and on the negative of a point of D, scheme-theoretically.

The main theorem is that a point of exact order N is killed by N (EllipticCurveGeom.IsOfExactOrder.pow_eq_one), so it is an S-point of the N-torsion E[N] (EllipticCurveGeom.IsOfExactOrder.comp_mulBy_eq_one). This holds over every base, including nonreduced ones, with no finiteness or rank hypothesis on D.

Points of exact order N are stable under base change (EllipticCurveGeom.IsOfExactOrder.pointsPullback): along a pullback square of elliptic curves, the divisor [P'] + ⋯ + [NP'] of the base change P' of P is the inverse image of [P] + ⋯ + [NP], and the inverse image of a closed subgroup scheme is again a closed subgroup scheme (EllipticCurveGeom.exists_grpObj_isMonHom_comap). This is the base-change functoriality of [Γ₁(N)]-structures.

Following EllipticCurveGeom.mulBy, the group law on points of E is written multiplicatively: P ^ a is the point aP, and 1 is the zero section.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.multiplesDivisor {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) :
E.carrier.IdealSheafData

The divisor [P] + [2P] + ⋯ + [NP] of the first N positive multiples of an S-point P of an elliptic curve E over S, as an ideal sheaf on E: the product of the ideal sheaves of the sections P ^ a for 1 ≤ a ≤ N. For N = 0 it is the empty divisor ⊤.

Instances For
    source
    def TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfExactOrder {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) :
    Prop

    Points of exact order N (Katz–Mazur). An S-point P of an elliptic curve E over S has exact order N when the closed subscheme of the divisor [P] + [2P] + ⋯ + [NP] is a subgroup scheme of E: it carries a group-object structure in Over S for which its inclusion into E is a homomorphism. By the closed-subgroup criterion (TauCeti.GroupScheme.exists_grpObj_isMonHom_iff_ker_le), such a structure is unique when it exists. The divisor is indexed by 1 ≤ a ≤ N, not by residues modulo N, since NP = 0 is a consequence (IsOfExactOrder.pow_eq_one) rather than an assumption. No rank condition is imposed: being a sum of N divisors of degree one, the divisor already has degree N.

    Instances For
      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_def {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} :
      E.IsOfExactOrder P N ↔ ∃ (x : CategoryTheory.GrpObj (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.comp (E.multiplesDivisor P N).subschemeι E.structureMap))), CategoryTheory.IsMonHom (CategoryTheory.Over.homMk (E.multiplesDivisor P N).subschemeι ⋯)

      A point P has exact order N exactly when the closed subscheme of [P] + ⋯ + [NP] is a subgroup scheme of E.

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_of_isEmpty {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} [IsEmpty ↥S] {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} :
      E.IsOfExactOrder P N

      Over an empty base every object of Over S is a group object and every morphism to a group object is a monoid homomorphism, so every point has exact order N.

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} :
      E.IsOfExactOrder P N ↔ E.multiplesDivisor P N ≤ AlgebraicGeometry.Scheme.Hom.ker E.zero ∧ E.multiplesDivisor P N ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Over.homMk (E.multiplesDivisor P N).subschemeι ⋯) (CategoryTheory.Over.homMk (E.multiplesDivisor P N).subschemeι ⋯)) CategoryTheory.MonObj.mul)) ∧ E.multiplesDivisor P N ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.homMk (E.multiplesDivisor P N).subschemeι ⋯) CategoryTheory.GrpObj.inv))

      The closed-subgroup criterion for points of exact order N. A point P has exact order N exactly when the ideal sheaf of D = [P] + ⋯ + [NP] vanishes on the identity, on the product of two points of D and on the inverse of a point of D.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.multiplesDivisor_zero {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) :
      E.multiplesDivisor P 0 = ⊤

      The divisor of the first zero multiples of a point is empty.

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.multiplesDivisor_succ {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) :
      E.multiplesDivisor P (N + 1) = E.multiplesDivisor P N * AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (P ^ (N + 1)))

      [P] + ⋯ + [(N + 1)P] is [P] + ⋯ + [NP] plus [(N + 1)P].

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.multiplesDivisor_eq_pointsDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) :
      E.multiplesDivisor P N = E.pointsDivisor fun (a : Fin N) => P ^ (↑a + 1)

      [P] + [2P] + ⋯ + [NP] is the divisor of the family of points P, 2P, …, NP, indexed by Fin N.

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isRelativeEffectiveCartier_multiplesDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) :
      (E.multiplesDivisor P N).IsRelativeEffectiveCartier E.structureMap

      The divisor [P] + [2P] + ⋯ + [NP] is a relative effective Cartier divisor on E over S.

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.multiplesDivisor_le_ker {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N a : ℕ} (ha : a < N) :
      E.multiplesDivisor P N ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (P ^ (a + 1)))

      Each of the points P, 2P, …, NP lies on the divisor [P] + [2P] + ⋯ + [NP].

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.coe_support_multiplesDivisor {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) :
      ↑(E.multiplesDivisor P N).support = ⋃ (a : ℕ), ⋃ (_ : a < N), Set.range ⇑(CategoryTheory.Over.Hom.left (P ^ (a + 1)))

      The support of the divisor [P] + [2P] + ⋯ + [NP] is the union of the images of the sections P, 2P, …, NP.

      Translating divisors of points #

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.ker_comap_leftTranslation_hom {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (Q x : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) :
      (AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left x)).comap (CategoryTheory.Over.Hom.left (leftTranslation Q).hom) = AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left (Q⁻¹ * x))

      Translating the divisor of a point. Left translation y ↦ Q * y on E pulls the divisor [x] of an S-point x back to the divisor [Q⁻¹ * x].

      Points of exact order N are killed by N #

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfExactOrder.pow_eq_one {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} (h : E.IsOfExactOrder P N) :
      P ^ N = 1

      A point of exact order N is killed by N (Katz–Mazur, §1.4): if the divisor [P] + [2P] + ⋯ + [NP] is a subgroup scheme of E, then NP = 0.

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfExactOrder.comp_mulBy_eq_one {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} (h : E.IsOfExactOrder P N) :
      CategoryTheory.CategoryStruct.comp P (E.mulBy ↑N) = 1

      A point of exact order N is killed by multiplication by N: [N] P = 0. Equivalently (EllipticCurveGeom.exists_comp_torsionι_iff), P is an S-point of the N-torsion E[N].

      Exact order one #

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfExactOrder_one_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} :
      E.IsOfExactOrder P 1 ↔ P = 1

      The points of exact order one: an S-point of E has exact order one exactly when it is the zero section. The divisor [0] is the trivial subgroup scheme of E.

      Base change #

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.multiplesDivisor_pointsPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {g : E'.carrier ⟶ E.carrier} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) :
      E'.multiplesDivisor ((pointsPullback hg h0) P) N = (E.multiplesDivisor P N).comap g

      The divisor [P] + ⋯ + [NP] commutes with base change: for the base change P' of an S-point P of E, the divisor [P'] + ⋯ + [NP'] on E' is the inverse image along g of the divisor [P] + ⋯ + [NP] on E.

      source
      theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfExactOrder.pointsPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {S' : AlgebraicGeometry.Scheme} {E' : EllipticCurveGeom S'} {g : E'.carrier ⟶ E.carrier} {f : S' ⟶ S} (hg : CategoryTheory.IsPullback g E'.structureMap E.structureMap f) (h0 : CategoryTheory.CategoryStruct.comp E'.zero g = CategoryTheory.CategoryStruct.comp f E.zero) {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} (h : E.IsOfExactOrder P N) :
      E'.IsOfExactOrder ((EllipticCurveGeom.pointsPullback hg h0) P) N

      Points of exact order N are stable under base change (Katz–Mazur, §1.4): if an S-point P of E has exact order N, then so does its base change, the S'-point P' of E'.