Multiplication by an integer on the projective Weierstrass model

Let W be an elliptic Weierstrass curve over a commutative ring R and E = projModel W its projective model, a commutative group scheme over Spec R (WeierstrassCurve.grpObjProjModel). This file studies the morphism [n] : E ⟶ E of schemes underlying multiplication by an integer n, which is multiplication by n on the elliptic curve toEllipticCurveGeom W read on E (WeierstrassCurve.projModelMulBy_eq).

A point of W with coordinates in a field L over R is a point of E with values in L, and [n] sends the point of P to the point of n • P. Over a field, applied to the generic point of W, whose coordinates are the affine coordinates in the function field, this computes the action of [n] on the generic point of the scheme E: the equation-level pullback of rational functions along [n] (TauCeti.Isogeny.mulByIntIsogenyOfNeZero, given by the division polynomials) describes where [n] sends the generic point. Hence for n ≠ 0 the morphism [n] is dominant, and its pullback of rational functions [n]^* : K(E) ⟶ K(E) (AlgebraicGeometry.Scheme.Hom.functionFieldMap) is the equation-level pullback, read through the identification projModelFunctionFieldEquiv of K(E) with W.toAffine.FunctionField. This identifies the extension of function fields induced by the scheme [n] with the one whose degree n² is computed from the equations (TauCeti.Isogeny.degree_mulByIntIsogenyOfNeZero), so [K(E) : [n]^* K(E)] = n². Over a field [n] is also flat, being a dominant morphism to a curve smooth over the field. For a finite flat dominant morphism of integral schemes the rank at every point is the degree of the function-field extension (AlgebraicGeometry.Scheme.Hom.finrank_eq_finrank_fieldRange_functionFieldMap), so together with the finiteness of [n] these compute the rank of [n] over a field as n²: the fibre of [n] over every point is the spectrum of an algebra of dimension n² over its residue field.

Main definitions

• WeierstrassCurve.projModelMulBy W n: the morphism [n] : projModel W ⟶ projModel W.
• WeierstrassCurve.mulByFunctionFieldPullback W n: over a field, for n ≠ 0, the pullback [n]^* : K(E) →+* K(E) of rational functions along [n].

Main results

• WeierstrassCurve.projModelMulBy_eq: it is multiplication by n on toEllipticCurveGeom W.
• WeierstrassCurve.projModelMulBy_comp_of_isPullback and WeierstrassCurve.comp_projModelMulBy_of_isPullback: [n] commutes with pointed base changes from and to the projective model.
• WeierstrassCurve.isFinite_projModelMulBy: for n ≠ 0, [n] is finite.
• WeierstrassCurve.comp_projModelMulBy_eq_homMk_zpow_left: for a section P of the projective model, nP is the n-th power of P bundled as a morphism of Over (Spec R).
• WeierstrassCurve.comp_projModelMulBy_add, WeierstrassCurve.comp_projModelMulBy_two and WeierstrassCurve.comp_projModelMulBy_add_one_eq_projModelZero_iff: for a section P of the projective model, (m + n)P is mP + nP through the addition morphism, 2P is P + P, and (n + 1)P = 0 exactly when nP = -P.
• WeierstrassCurve.projModelPointsEquiv_symm_projModelBaseChange_projModelMulBy: [n] sends the point with values in a field L of a point P of W over L to that of n • P; WeierstrassCurve.projModelPoint_projModelMulBy_of_zsmul_some and WeierstrassCurve.projModelPoint_projModelMulBy_of_zsmul_eq_zero state this on the point with homogeneous coordinates [x : y : 1], according as n • (x, y) is affine or zero.
• WeierstrassCurve.projModelAffinePoint_projModelMulBy_ne_projModelZero_iff and WeierstrassCurve.isUnit_evalEval_ψ_iff: over a commutative ring, the n-th multiple of the point [x : y : 1] misses the zero section over a point s of the base exactly when ψₙ(x, y) does not lie in s, and over every point exactly when ψₙ(x, y) is a unit.
• WeierstrassCurve.isDominant_projModelMulBy: over a field, for n ≠ 0, [n] is dominant.
• WeierstrassCurve.projModelFunctionFieldEquiv_mulByFunctionFieldPullback: over a field, for n ≠ 0, the pullback of rational functions along [n] is the equation-level pullback (TauCeti.Isogeny.mulByIntIsogenyOfNeZero W hn).fieldPullback.
• WeierstrassCurve.flat_projModelMulBy: over a field, for n ≠ 0, [n] is flat.
• WeierstrassCurve.finrank_fieldRange_mulByFunctionFieldPullback: over a field, for n ≠ 0, [K(E) : [n]^* K(E)] = n².
• WeierstrassCurve.finrank_projModelMulBy: over a field, for n ≠ 0, [n] has rank n² at every point.

References

• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.3.1.
• J. H. Silverman, The Arithmetic of Elliptic Curves, III.4.2 and III.6.4.

noncomputable def WeierstrassCurve.projModelMulBy {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (n : ℤ) : W.projModel ⟶ W.projModel

Multiplication by an integer on the projective Weierstrass model: the morphism of schemes [n] : projModel W ⟶ projModel W underlying the n-th power of the identity of the commutative group scheme projModel W over Spec R (grpObjProjModel). It sends every point x of the projective model to x ^ n (comp_projModelMulBy), and it is multiplication by n on the elliptic curve toEllipticCurveGeom W (projModelMulBy_eq).

@[simp]

theorem WeierstrassCurve.comp_projModelMulBy {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)} (x : Z ⟶ CategoryTheory.Over.mk W.projModelOver) (n : ℤ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left x) (W.projModelMulBy n) = CategoryTheory.Over.Hom.left (x ^ n)

Multiplication by n sends a point x of the projective model, with values in any Z over Spec R, to x ^ n.

@[simp]

theorem WeierstrassCurve.comp_projModelMulBy_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {Z : CategoryTheory.Over (AlgebraicGeometry.Spec ↧R)} (x : Z ⟶ CategoryTheory.Over.mk W.projModelOver) (n : ℤ) {Z✝ : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left x) (CategoryTheory.CategoryStruct.comp (W.projModelMulBy n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (x ^ n)) h

Multiplication by n sends a point x of the projective model, with values in any Z over Spec R, to x ^ n.

@[simp]

theorem WeierstrassCurve.projModelMulBy_projModelOver {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (n : ℤ) : CategoryTheory.CategoryStruct.comp (W.projModelMulBy n) W.projModelOver = W.projModelOver

Multiplication by n lies over Spec R.

@[simp]

theorem WeierstrassCurve.projModelMulBy_projModelOver_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (n : ℤ) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.projModelMulBy n) (CategoryTheory.CategoryStruct.comp W.projModelOver h) = CategoryTheory.CategoryStruct.comp W.projModelOver h

Multiplication by n lies over Spec R.

theorem WeierstrassCurve.projModelMulBy_eq {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (n : ℤ) : W.projModelMulBy n = CategoryTheory.CategoryStruct.comp W.toEllipticCurveGeomIso.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (W.toEllipticCurveGeom.mulBy n)) W.toEllipticCurveGeomIso.hom)

Multiplication by n on the projective model is multiplication by n on the elliptic curve toEllipticCurveGeom W, read on the projective model through toEllipticCurveGeomIso.

theorem WeierstrassCurve.projModelMulBy_comp_of_isPullback {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {S : AlgebraicGeometry.Scheme} {E : TauCeti.AlgebraicGeometry.EllipticCurveGeom S} {a : W.projModel ⟶ E.carrier} {b : AlgebraicGeometry.Spec ↧R ⟶ S} (hab : CategoryTheory.IsPullback a W.projModelOver E.structureMap b) (h₀ : CategoryTheory.CategoryStruct.comp W.projModelZero a = CategoryTheory.CategoryStruct.comp b E.zero) (n : ℤ) : CategoryTheory.CategoryStruct.comp (W.projModelMulBy n) a = CategoryTheory.CategoryStruct.comp a (CategoryTheory.Over.Hom.left (E.mulBy n))

Multiplication by n commutes with a pointed base change from the projective model. Let a : projModel W ⟶ E be a morphism to an elliptic curve E over a scheme S, forming a pullback square over a morphism b : Spec R ⟶ S and carrying the zero section to the zero section. Then a carries multiplication by n on the projective model to multiplication by n on E.

theorem WeierstrassCurve.projModelMulBy_comp_of_isPullback_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {S : AlgebraicGeometry.Scheme} {E : TauCeti.AlgebraicGeometry.EllipticCurveGeom S} {a : W.projModel ⟶ E.carrier} {b : AlgebraicGeometry.Spec ↧R ⟶ S} (hab : CategoryTheory.IsPullback a W.projModelOver E.structureMap b) (h₀ : CategoryTheory.CategoryStruct.comp W.projModelZero a = CategoryTheory.CategoryStruct.comp b E.zero) (n : ℤ) {Z : AlgebraicGeometry.Scheme} (h : E.carrier ⟶ Z) : CategoryTheory.CategoryStruct.comp (W.projModelMulBy n) (CategoryTheory.CategoryStruct.comp a h) = CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E.mulBy n)) h)

Multiplication by n commutes with a pointed base change from the projective model. Let a : projModel W ⟶ E be a morphism to an elliptic curve E over a scheme S, forming a pullback square over a morphism b : Spec R ⟶ S and carrying the zero section to the zero section. Then a carries multiplication by n on the projective model to multiplication by n on E.

theorem WeierstrassCurve.comp_projModelMulBy_of_isPullback {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {S : AlgebraicGeometry.Scheme} {E : TauCeti.AlgebraicGeometry.EllipticCurveGeom S} {g : E.carrier ⟶ W.projModel} {f : S ⟶ AlgebraicGeometry.Spec ↧R} (hg : CategoryTheory.IsPullback g E.structureMap W.projModelOver f) (h₀ : CategoryTheory.CategoryStruct.comp E.zero g = CategoryTheory.CategoryStruct.comp f W.projModelZero) (n : ℤ) : CategoryTheory.CategoryStruct.comp g (W.projModelMulBy n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E.mulBy n)) g

Multiplication by n commutes with a pointed base change to the projective model. Let g : E ⟶ projModel W be a morphism from an elliptic curve E over a scheme S, forming a pullback square over a morphism f : S ⟶ Spec R and carrying the zero section to the zero section. Then g carries multiplication by n on E to multiplication by n on the projective model.

theorem WeierstrassCurve.comp_projModelMulBy_of_isPullback_assoc {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {S : AlgebraicGeometry.Scheme} {E : TauCeti.AlgebraicGeometry.EllipticCurveGeom S} {g : E.carrier ⟶ W.projModel} {f : S ⟶ AlgebraicGeometry.Spec ↧R} (hg : CategoryTheory.IsPullback g E.structureMap W.projModelOver f) (h₀ : CategoryTheory.CategoryStruct.comp E.zero g = CategoryTheory.CategoryStruct.comp f W.projModelZero) (n : ℤ) {Z : AlgebraicGeometry.Scheme} (h : W.projModel ⟶ Z) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (W.projModelMulBy n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (E.mulBy n)) (CategoryTheory.CategoryStruct.comp g h)

Multiplication by n commutes with a pointed base change to the projective model. Let g : E ⟶ projModel W be a morphism from an elliptic curve E over a scheme S, forming a pullback square over a morphism f : S ⟶ Spec R and carrying the zero section to the zero section. Then g carries multiplication by n on E to multiplication by n on the projective model.

instance WeierstrassCurve.isFinite_projModelMulBy {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (n : ℤ) [NeZero n] : AlgebraicGeometry.IsFinite (W.projModelMulBy n)

Multiplication by a nonzero integer on the projective Weierstrass model is finite, being multiplication by n on the elliptic curve toEllipticCurveGeom W (TauCeti.AlgebraicGeometry.EllipticCurveGeom.isFinite_mulBy_left).

theorem WeierstrassCurve.comp_projModelMulBy_eq_homMk_zpow_left {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {P : AlgebraicGeometry.Spec ↧R ⟶ W.projModel} (hP : CategoryTheory.CategoryStruct.comp P W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) (n : ℤ) : CategoryTheory.CategoryStruct.comp P (W.projModelMulBy n) = CategoryTheory.Over.Hom.left (CategoryTheory.Over.homMk P ⋯ ^ n)

Multiplication by n on a section. A section P of the projective model, bundled as a morphism of Over (Spec R) from the terminal object, has n-th multiple the n-th power of that morphism.

theorem WeierstrassCurve.comp_projModelMulBy_add {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {P : AlgebraicGeometry.Spec ↧R ⟶ W.projModel} (hP : CategoryTheory.CategoryStruct.comp P W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) (m n : ℤ) : CategoryTheory.CategoryStruct.comp P (W.projModelMulBy (m + n)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp P (W.projModelMulBy m)) (CategoryTheory.CategoryStruct.comp P (W.projModelMulBy n)) ⋯) W.additionMorphism

Multiplication by a sum on a section. For a section P of the projective model, the (m + n)-th multiple of P is the sum of its m-th and n-th multiples, computed by the addition morphism.

theorem WeierstrassCurve.comp_projModelMulBy_two {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {P : AlgebraicGeometry.Spec ↧R ⟶ W.projModel} (hP : CategoryTheory.CategoryStruct.comp P W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) : CategoryTheory.CategoryStruct.comp P (W.projModelMulBy 2) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift P P ⋯) W.additionMorphism

Doubling a section. For a section P of the projective model, 2P is the addition morphism at the pair (P, P).

theorem WeierstrassCurve.comp_projModelMulBy_add_one_eq_projModelZero_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {P : AlgebraicGeometry.Spec ↧R ⟶ W.projModel} (hP : CategoryTheory.CategoryStruct.comp P W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) (n : ℤ) : CategoryTheory.CategoryStruct.comp P (W.projModelMulBy (n + 1)) = W.projModelZero ↔ CategoryTheory.CategoryStruct.comp P (W.projModelMulBy n) = CategoryTheory.CategoryStruct.comp P W.projModelNeg

For a section P of the projective model, (n + 1)P = 0 exactly when nP = -P.

theorem WeierstrassCurve.projModelPointsEquiv_symm_projModelBaseChange_projModelMulBy {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {L : Type u} [Field L] (g : R →+* L) [DecidableEq L] (P : (W.map g).toAffine.Point) (n : ℤ) : CategoryTheory.CategoryStruct.comp (↑((W.map g).projModelPointsEquiv.symm P)) (CategoryTheory.CategoryStruct.comp (W.projModelBaseChange g) (W.projModelMulBy n)) = CategoryTheory.CategoryStruct.comp (↑((W.map g).projModelPointsEquiv.symm (n • P))) (W.projModelBaseChange g)

Multiplication by n on points with values in a field. Let g : R →+* L be a ring homomorphism to a field. A point P of W over L gives the point (projModelPointsEquiv (W.map g)).symm P of the projective model of W.map g over Spec L, hence, through the base change morphism projModelBaseChange, a point of projModel W with values in L. Multiplication by n sends the point of P to the point of n • P.

theorem WeierstrassCurve.projModelPointsEquiv_symm_some_projModelBaseChange {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {L : Type u} [Field L] (g : R →+* L) {x y : L} (h : (W.map g).toAffine.Nonsingular x y) : CategoryTheory.CategoryStruct.comp (↑((W.map g).projModelPointsEquiv.symm (Affine.Point.some x y h))) (W.projModelBaseChange g) = W.projModelPoint g ⋯ ⋯

The point with values in a field L of an affine point (x, y) of W over L, through the base change morphism projModelBaseChange, is the point with homogeneous coordinates [x : y : 1] along g.

theorem WeierstrassCurve.projModelPoint_projModelMulBy_of_zsmul_some {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {L : Type u} [Field L] (g : R →+* L) [DecidableEq L] {x y x' y' : L} {h : (W.map g).toAffine.Nonsingular x y} {h' : (W.map g).toAffine.Nonsingular x' y'} {n : ℤ} (hn : n • Affine.Point.some x y h = Affine.Point.some x' y' h') : CategoryTheory.CategoryStruct.comp (W.projModelPoint g ⋯ ⋯) (W.projModelMulBy n) = W.projModelPoint g ⋯ ⋯

If multiplication by n sends the affine point (x, y) of W over a field L to (x', y'), then [n] sends the point with homogeneous coordinates [x : y : 1] along g to the one with homogeneous coordinates [x' : y' : 1].

theorem WeierstrassCurve.projModelPoint_projModelMulBy_of_zsmul_eq_zero {R : Type u} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {L : Type u} [Field L] (g : R →+* L) [DecidableEq L] {x y : L} {h : (W.map g).toAffine.Nonsingular x y} {n : ℤ} (hn : n • Affine.Point.some x y h = 0) : CategoryTheory.CategoryStruct.comp (W.projModelPoint g ⋯ ⋯) (W.projModelMulBy n) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom g)) W.projModelZero

If multiplication by n kills the affine point (x, y) of W over a field L, then [n] sends the point with homogeneous coordinates [x : y : 1] along g to the zero section, along g.

theorem WeierstrassCurve.projModelAffinePoint_projModelMulBy_ne_projModelZero_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {x y : R} (h : W.toAffine.Equation x y) (n : ℤ) (s : ↥(AlgebraicGeometry.Spec ↧R)) : (CategoryTheory.CategoryStruct.comp (W.projModelAffinePoint h) (W.projModelMulBy n)) s ≠ W.projModelZero s ↔ Polynomial.evalEval x y (W.ψ n) ∉ s.asIdeal

The n-th multiple of [x : y : 1] over a point of the base. Over a point s of Spec R, the n-th multiple of the point [x : y : 1] misses the zero section exactly when the value ψₙ(x, y) of the n-th division polynomial does not lie in s.

theorem WeierstrassCurve.isUnit_evalEval_ψ_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {x y : R} (h : W.toAffine.Equation x y) (n : ℤ) : IsUnit (Polynomial.evalEval x y (W.ψ n)) ↔ ∀ (s : ↥(AlgebraicGeometry.Spec ↧R)), (CategoryTheory.CategoryStruct.comp (W.projModelAffinePoint h) (W.projModelMulBy n)) s ≠ W.projModelZero s

The n-th multiple of [x : y : 1] misses the zero section exactly when ψₙ(x, y) is a unit. The n-th multiple of the point [x : y : 1] of the projective model over Spec R meets the zero section over no point of Spec R exactly when the value ψₙ(x, y) of the n-th division polynomial is a unit of R.

instance WeierstrassCurve.isDominant_projModelMulBy {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (n : ℤ) [NeZero n] : AlgebraicGeometry.IsDominant (W.projModelMulBy n)

Over a field, multiplication by a nonzero integer on the projective Weierstrass model is dominant.

noncomputable def WeierstrassCurve.mulByFunctionFieldPullback {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (n : ℤ) [NeZero n] : ↑W.projModel.functionField →+* ↑W.projModel.functionField

The pullback of rational functions along multiplication by n. Over a field, for n ≠ 0, the pullback [n]^* : K(E) →+* K(E) of rational functions along the dominant morphism [n] of the projective Weierstrass model E (AlgebraicGeometry.Scheme.Hom.functionFieldMap). Through projModelFunctionFieldEquiv it is the equation-level pullback (projModelFunctionFieldEquiv_mulByFunctionFieldPullback).

@[simp]

theorem WeierstrassCurve.projModelFunctionFieldEquiv_mulByFunctionFieldPullback {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (n : ℤ) [NeZero n] (f : ↑W.projModel.functionField) : W.projModelFunctionFieldEquiv ((W.mulByFunctionFieldPullback n) f) = (TauCeti.Isogeny.mulByIntIsogenyOfNeZero W ⋯).fieldPullback (W.projModelFunctionFieldEquiv f)

The pullback of rational functions along [n] is the equation-level one. Over a field, for n ≠ 0, the pullback [n]^* : K(E) →+* K(E) of rational functions along multiplication by n on the projective Weierstrass model E, read through the identification projModelFunctionFieldEquiv of K(E) with the function field of the affine equation, is the pullback of rational functions along the equation-level multiplication by n, (TauCeti.Isogeny.mulByIntIsogenyOfNeZero W hn).fieldPullback.

instance WeierstrassCurve.flat_projModelMulBy {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (n : ℤ) [NeZero n] : AlgebraicGeometry.Flat (W.projModelMulBy n)

Over a field, multiplication by a nonzero integer on the projective Weierstrass model is flat, as is every dominant morphism to a curve smooth over a field.

@[simp]

theorem WeierstrassCurve.finrank_fieldRange_mulByFunctionFieldPullback {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (n : ℤ) [NeZero n] : Module.finrank ↥(W.mulByFunctionFieldPullback n).fieldRange ↑W.projModel.functionField = n.natAbs ^ 2

The degree of the function-field extension of [n] is n². Over a field, for n ≠ 0, the function field K(E) of the projective Weierstrass model E has degree n² over its image [n]^* K(E) under the pullback of rational functions along multiplication by n. Through projModelFunctionFieldEquiv, this is the degree of the equation-level multiplication by n (TauCeti.Isogeny.degree_mulByIntIsogenyOfNeZero).

@[simp]

theorem WeierstrassCurve.finrank_projModelMulBy {K : Type u} [Field K] (W : WeierstrassCurve K) [W.IsElliptic] (n : ℤ) [NeZero n] (y : ↥W.projModel) : AlgebraicGeometry.Scheme.Hom.finrank (W.projModelMulBy n) y = n.natAbs ^ 2

Multiplication by n has rank n² (Katz–Mazur 2.3.1). Over a field, for n ≠ 0, the finite flat morphism [n] of the projective Weierstrass model has rank n² at every point y: the fibre of [n] over y is the spectrum of an algebra of dimension n² over the residue field of y. The rank of a finite flat dominant morphism of integral schemes is the degree of its function-field extension, here n² (finrank_fieldRange_mulByFunctionFieldPullback).