Points of naive exact order N on an elliptic curve

Let E be an elliptic curve over a scheme S and x a point of E with values in a scheme Z over S. Following Katz and Mazur, x has naive exact order N when it is a point of the N-torsion E[N], that is Nx = 0, and for every divisor d ≠ N of N the point dx meets the zero section nowhere: the equalizer of dx and 0, the closed subscheme of Z on which the two agree, is empty (EllipticCurveGeom.IsOfNaiveExactOrder). Over a field this says that x has order exactly N in the group of points (EllipticCurveGeom.isOfNaiveExactOrder_iff_orderOf_eq); in general it is the scheme-theoretic form of asking that x have order exactly N in every geometric fibre.

An S-point of naive exact order N is a naive [Γ₁(N)]-structure on E: an S-point Q has empty equalizer with the zero section exactly when it meets the zero section at no point of S (EllipticCurveGeom.isEmpty_equalizer_one_iff), so a homomorphism φ : ℤ/Nℤ →* E(S) is injective on every fibre, the condition defining ModuliProblem.gammaOneNaive, exactly when φ 1 has naive exact order N (EllipticCurveGeom.isFiberwiseInjective_iff_isOfNaiveExactOrder).

Unlike the Drinfeld notion EllipticCurveGeom.IsOfExactOrder, which works over every base, the naive notion behaves poorly where N is not invertible: over a field of characteristic p, a supersingular curve has no point of naive exact order p, while its zero section has exact order p in Drinfeld's sense. Accordingly the scheme of points of naive exact order N below is open in E[N] for every N ≠ 0, and it is closed in E[N], and so finite over S, whenever N is invertible; closedness need not hold over an arbitrary base. Points of naive exact order N are stable under base change, both along morphisms Z' ⟶ Z (EllipticCurveGeom.IsOfNaiveExactOrder.comp) and along base change of the elliptic curve (EllipticCurveGeom.IsOfNaiveExactOrder.pointsPullback).

A point of E[N] with values in Z has naive exact order N exactly when it maps Z into the naive locus EllipticCurveGeom.naiveLocus (E.torsionPointHom N) of the universal point P of E[N]: the set of points of E[N] at which no multiple aP with a ≠ 0 meets the zero section (EllipticCurveGeom.isOfNaiveExactOrder_comp_torsionι_iff). For N ≠ 0 this set is open (EllipticCurveGeom.isOpen_naiveLocus), and the corresponding open subscheme EllipticCurveGeom.naiveLocusOver (E.torsionPointHom N) of E[N], which also represents the naive moduli problem [Γ₁(N)] over Ell/B (ModuliProblem.gammaOneNaiveRelRepData), represents the functor of points of naive exact order N (EllipticCurveGeom.naiveExactOrderRepresentableBy). Pulling it back along an S-point P gives the locus of S over which P has naive exact order N (EllipticCurveGeom.naiveExactOrderPreimage): a morphism T ⟶ S factors through it exactly when the base change of P to T has naive exact order N (EllipticCurveGeom.exists_lift_naiveExactOrderPreimageι_iff). Where N is invertible on S, the naive locus is closed in E[N] as well (EllipticCurveGeom.isClopen_naiveLocus), so this locus is a closed subscheme of S (EllipticCurveGeom.isClosedImmersion_naiveExactOrderPreimageι).

Following EllipticCurveGeom.mulBy, the group law on points of E is written multiplicatively: x ^ d is the point dx, and 1 is the zero section.

Main definitions

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder E x N: the point x has naive exact order N.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderSubfunctor E N: the points of E of naive exact order N, as a subfunctor of the functor of points of E.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderPreimage N P: the locus of S over which an S-point P has naive exact order N ≠ 0, with inclusion TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderPreimageι N P.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_iff_orderOf_eq: over a field, a point has naive exact order N exactly when its order in the group of points is N.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder.pointsPullback: points of naive exact order N are stable under base change of the elliptic curve.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_pointsBaseChangeEquiv_iff: identifying points of a base change with points valued in the new base preserves and reflects naive exact order.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_isOfNaiveExactOrder_over: over each separably closed field point where N is invertible, there is a point of naive exact order N.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFiberwiseInjective_iff_isOfNaiveExactOrder: a homomorphism ℤ/Nℤ →* E(S) is a naive [Γ₁(N)]-structure exactly when the image of 1 has naive exact order N.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_iff_forall_lt: a point x has naive exact order N exactly when Nx = 0 and kx meets the zero section nowhere for 0 < k < N.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_comp_torsionι_iff: a point of E[N] has naive exact order N exactly when it lands in the naive locus of the universal point of E[N].
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderRepresentableBy: for N ≠ 0, the naive locus of the universal point of E[N], an open subscheme of E[N], represents the points of E of naive exact order N.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_lift_naiveExactOrderPreimageι_iff: a morphism T ⟶ S factors through the locus where P has naive exact order N exactly when the base change of P to T has naive exact order N.
• TauCeti.AlgebraicGeometry.EllipticCurveGeom.isClosedImmersion_naiveExactOrderPreimageι: where N is invertible on S, the locus where P has naive exact order N is a closed subscheme of S.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 1.4.4 and §3.7 (naive level structures).
• P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, LNM 349, IV, Construction 4.8 (a naive [Γ₁(N)]-structure as a section everywhere of exact order N).
• D. Loeffler, Modular Curves, lecture notes, §3.8.

def TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {Z : CategoryTheory.Over S} (x : Z ⟶ CategoryTheory.Over.mk E.structureMap) (N : ℕ) : Prop

Points of naive exact order N. A point x of an elliptic curve E over S, with values in a scheme Z over S, has naive exact order N when Nx = 0 and, for every divisor d ≠ N of N, the point dx meets the zero section nowhere: the equalizer of dx and 0 is empty. Over a field this says that x has order exactly N (isOfNaiveExactOrder_iff_orderOf_eq). For N = 0 every d ≥ 1 divides N, so this asks that x have infinite order in every fibre.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {x : Z ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} : E.IsOfNaiveExactOrder x N ↔ x ^ N = 1 ∧ ∀ (d : ℕ), d ∣ N → d ≠ N → IsEmpty ↥(CategoryTheory.Limits.equalizer (x ^ d) 1).left

The defining property of a point of naive exact order N.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder.pow_eq_one {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {x : Z ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} (h : E.IsOfNaiveExactOrder x N) : x ^ N = 1

A point of naive exact order N is killed by N.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder.comp_mulBy_eq_one {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {x : Z ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} (h : E.IsOfNaiveExactOrder x N) : CategoryTheory.CategoryStruct.comp x (E.mulBy ↑N) = 1

A point of naive exact order N is killed by multiplication by N, so it is a point of the N-torsion E[N] (EllipticCurveGeom.exists_comp_torsionι_iff).

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder.isEmpty_equalizer {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {x : Z ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} (h : E.IsOfNaiveExactOrder x N) {d : ℕ} (hd : d ∣ N) (hdN : d ≠ N) : IsEmpty ↥(CategoryTheory.Limits.equalizer (x ^ d) 1).left

If x has naive exact order N, then for every divisor d ≠ N of N the point dx meets the zero section nowhere.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder.comp {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {x : Z ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} {Z' : CategoryTheory.Over S} (h : E.IsOfNaiveExactOrder x N) (k : Z' ⟶ Z) : E.IsOfNaiveExactOrder (CategoryTheory.CategoryStruct.comp k x) N

Points of naive exact order N pull back: if x has naive exact order N, then so has its composite with any morphism k : Z' ⟶ Z of schemes over S.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_one_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {x : Z ⟶ CategoryTheory.Over.mk E.structureMap} : E.IsOfNaiveExactOrder x 1 ↔ x = 1

The only point of naive exact order one is the zero section.

Over a field

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_iff_orderOf_eq {N : ℕ} {K : Type u} [Field K] {E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧K)} {P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk E.structureMap} : E.IsOfNaiveExactOrder P N ↔ orderOf P = N

Naive exact order over a field. A K-point of an elliptic curve over a field K has naive exact order N exactly when its order in the group of K-points is N.

Base change

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_pointsBaseChangeEquiv_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {N : ℕ} {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} : E.IsOfNaiveExactOrder ((pointsBaseChangeEquiv hg h0) P) N ↔ E'.IsOfNaiveExactOrder P N

Under the group equivalence identifying points of a base change with points valued in the new base, naive exact order is preserved and reflected.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.IsOfNaiveExactOrder.pointsPullback {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {N : ℕ} {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} (h : E.IsOfNaiveExactOrder P N) : E'.IsOfNaiveExactOrder ((EllipticCurveGeom.pointsPullback hg h0) P) N

Points of naive exact order N are stable under base change: if an S-point P of E has naive exact order N, then so does its base change, the S'-point P' of E'.

Comparison with injectivity on fibres

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isEmpty_equalizer_one_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (Q : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) : IsEmpty ↥(CategoryTheory.Limits.equalizer Q 1).left ↔ ∀ (s : ↥(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S)).left), (CategoryTheory.Over.Hom.left Q) s ≠ E.zero s

An S-point Q of E has empty equalizer with the zero section exactly when it meets the zero section at no point of S.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFiberwiseInjective_iff_isOfNaiveExactOrder {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {N : ℕ} {φ : Multiplicative (ZMod N) →* (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap)} : E.IsFiberwiseInjective φ ↔ E.IsOfNaiveExactOrder (φ (Multiplicative.ofAdd 1)) N

Naive [Γ₁(N)]-structures are the S-points of naive exact order N. A homomorphism φ : ℤ/Nℤ →* E(S) is injective on every fibre, that is, it is a naive [Γ₁(N)]-structure (ModuliProblem.gammaOneNaive), exactly when the S-point φ 1 has naive exact order N.

Existence over separably closed fields

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_isOfNaiveExactOrder {N : ℕ} {K : Type u} [Field K] [IsSepClosed K] (E : EllipticCurveGeom (AlgebraicGeometry.Spec ↧K)) (hN : ↑N ≠ 0) : ∃ (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧K)) ⟶ CategoryTheory.Over.mk E.structureMap), E.IsOfNaiveExactOrder P N

Over a separably closed field where N is invertible, an elliptic curve has a point of naive exact order N.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_isOfNaiveExactOrder_over {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {N : ℕ} {K : Type u} [Field K] [IsSepClosed K] (t : AlgebraicGeometry.Spec ↧K ⟶ S) (hN : ↑N ≠ 0) : ∃ (P : CategoryTheory.Over.mk t ⟶ CategoryTheory.Over.mk E.structureMap), E.IsOfNaiveExactOrder P N

For a geometric point of the base in a characteristic prime to N, there is a point of naive exact order N above it, valued in the same separably closed field.

The functor of points of naive exact order N

def TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderSubfunctor {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) : CategoryTheory.Subfunctor (CategoryTheory.yoneda.obj (CategoryTheory.Over.mk E.structureMap))

The functor of points of naive exact order N: the subfunctor of the functor of points Z ↦ (Z ⟶ E) of E, on schemes over S, whose values at Z are the points of naive exact order N with values in Z.

@[simp]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.mem_naiveExactOrderSubfunctor_obj {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {N : ℕ} {Z : (CategoryTheory.Over S)ᵒᵖ} {x : Opposite.unop Z ⟶ CategoryTheory.Over.mk E.structureMap} : x ∈ (E.naiveExactOrderSubfunctor N).obj Z ↔ E.IsOfNaiveExactOrder x N

The values of naiveExactOrderSubfunctor E N are the points of naive exact order N.

The locus of naive exact order N in E[N]

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_iff_forall_lt {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {x : Z ⟶ CategoryTheory.Over.mk E.structureMap} {N : ℕ} [NeZero N] : E.IsOfNaiveExactOrder x N ↔ x ^ N = 1 ∧ ∀ (k : ℕ), 0 < k → k < N → IsEmpty ↥(CategoryTheory.Limits.equalizer (x ^ k) 1).left

Naive exact order among the multiples below N. A point x of E with values in Z has naive exact order N ≠ 0 exactly when Nx = 0 and, for every 0 < k < N, the point kx meets the zero section nowhere: where kx and Nx meet the zero section, so does gcd(k, N) x, a proper multiple.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isOfNaiveExactOrder_comp_torsionι_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {N : ℕ} [NeZero N] (y : Z ⟶ (E.torsion ↑N).X) : E.IsOfNaiveExactOrder (CategoryTheory.CategoryStruct.comp y (E.torsionι ↑N)) N ↔ Set.range ⇑(CategoryTheory.Over.Hom.left y) ⊆ naiveLocus (E.torsionPointHom N)

Points of E[N] of naive exact order N. A point y of the N-torsion E[N] with values in Z has naive exact order N, as a point of E, exactly when it maps Z into the naive locus of the universal point P of E[N] (EllipticCurveGeom.torsionPointHom), the set of points of E[N] at which no multiple aP with a ≠ 0 meets the zero section.

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderRepresentableBy {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) (N : ℕ) [NeZero N] : (E.naiveExactOrderSubfunctor N).toFunctor.RepresentableBy (naiveLocusOver (E.torsionPointHom N))

The scheme of points of naive exact order N represents them. For N ≠ 0, morphisms over S from Z to the naive locus of the universal point of E[N], the open subscheme of E[N] representing the naive moduli problem [Γ₁(N)], correspond, by composing with the inclusions into E[N] and into E, to the points of E of naive exact order N with values in Z, naturally in Z.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.coe_naiveExactOrderRepresentableBy_homEquiv {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} {N : ℕ} [NeZero N] (u : Z ⟶ naiveLocusOver (E.torsionPointHom N)) : ↑((E.naiveExactOrderRepresentableBy N).homEquiv u) = CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (naiveLocusι (E.torsionPointHom N)) (E.torsionι ↑N))

The point of naive exact order N corresponding to a morphism u into the naive locus of the universal point of E[N] is the composite of u with the inclusions into E[N] and into E.

The locus where an S-point has naive exact order N

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderPreimage {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (N : ℕ) [NeZero N] (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) : AlgebraicGeometry.Scheme

The locus where an S-point has naive exact order N: for N ≠ 0, the preimage under the S-point P of the naive locus of the universal point of E[N], the open subscheme of E[N] of points of naive exact order N. A morphism t : T ⟶ S factors through it exactly when the base change of P along t has naive exact order N (exists_lift_naiveExactOrderPreimageι_iff).

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderPreimageι {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (N : ℕ) [NeZero N] (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) : naiveExactOrderPreimage N P ⟶ S

The inclusion of the locus where P has naive exact order N into S.

instance TauCeti.AlgebraicGeometry.EllipticCurveGeom.mono_naiveExactOrderPreimageι {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (N : ℕ) [NeZero N] (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) : CategoryTheory.Mono (naiveExactOrderPreimageι N P)

The inclusion of the locus where P has naive exact order N into S is a monomorphism.

noncomputable def TauCeti.AlgebraicGeometry.EllipticCurveGeom.naiveExactOrderPreimagePoint {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (N : ℕ) [NeZero N] (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) : naiveExactOrderPreimage N P ⟶ ↑(naiveLocusOpens (E.torsionPointHom N))

The restriction of P to the locus where P has naive exact order N, as a point of the naive locus of the universal point of E[N], the scheme of points of naive exact order N.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isPullback_naiveExactOrderPreimage {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (N : ℕ) [NeZero N] (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) : CategoryTheory.IsPullback (naiveExactOrderPreimageι N P) (naiveExactOrderPreimagePoint N P) (CategoryTheory.Over.Hom.left P) (CategoryTheory.CategoryStruct.comp (naiveLocusOpens (E.torsionPointHom N)).ι (CategoryTheory.Over.Hom.left (E.torsionι ↑N)))

The locus where P has naive exact order N is the preimage under P of the naive locus of the universal point of E[N].

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_lift_naiveExactOrderPreimageι_iff {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {Z : CategoryTheory.Over S} (N : ℕ) [NeZero N] (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) {x : Z ⟶ CategoryTheory.Over.mk E.structureMap} (hx : CategoryTheory.Over.Hom.left x = CategoryTheory.CategoryStruct.comp Z.hom (CategoryTheory.Over.Hom.left P)) : (∃ (l : Z.left ⟶ naiveExactOrderPreimage N P), CategoryTheory.CategoryStruct.comp l (naiveExactOrderPreimageι N P) = Z.hom) ↔ E.IsOfNaiveExactOrder x N

The universal property of the locus where P has naive exact order N. Let x be the point of E with values in a scheme Z over S given by the base change of P, that is x = P ∘ (Z ⟶ S). Then Z ⟶ S factors through the locus where P has naive exact order N exactly when x has naive exact order N.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.isClosedImmersion_naiveExactOrderPreimageι {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} (N : ℕ) [NeZero N] (P : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over S) ⟶ CategoryTheory.Over.mk E.structureMap) (hN : ∀ (s : ↥S), ↑N ≠ 0) : AlgebraicGeometry.IsClosedImmersion (naiveExactOrderPreimageι N P)

The locus where P has naive exact order N is closed where N is invertible. If N is invertible in every residue field of S, the naive locus of the universal point of E[N] is closed in E[N] (EllipticCurveGeom.isClopen_naiveLocus), so its preimage under P is a closed subscheme of S.