How many points [n] sends to a given one

The points that [n] carries to a fixed T form a coset of ker [n] as soon as there is one of them, so there are exactly #ker [n] of them — and over an algebraically closed field with n invertible that is n ². The coset count itself is group theory, and lives in TauCeti/GroupTheory/Coset/Fiber.lean; what is added here is the identification of the kernel with ker [n] and the value n ².

The count is what turns a sum over the places above a point into a sum of n ² terms, which is how the pullback of a divisor along [n] is read.

Main results

• TauCeti.Isogeny.card_zsmul_fiber_eq_card_ker: a nonempty [n]-fiber has as many points as ker [n].
• TauCeti.Isogeny.card_zsmul_fiber: over an algebraically closed field, for n invertible there, that count is n ².

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.6.4(b).

theorem TauCeti.Isogeny.card_zsmul_fiber_eq_card_ker {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) {T P₀ : (WeierstrassCurve.toAffine (W.baseChange F)).Point} (hP₀ : n • P₀ = T) : Nat.card { P : (WeierstrassCurve.toAffine (W.baseChange F)).Point // n • P = T } = Nat.card ↥(mulByIntIsogeny W hn).ker

A nonempty [n]-fiber has as many points as ker [n].

theorem TauCeti.Isogeny.card_zsmul_fiber {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] [IsAlgClosed F] {n : ℤ} (hchar : ↑n ≠ 0) {T P₀ : (WeierstrassCurve.toAffine (W.baseChange F)).Point} (hP₀ : n • P₀ = T) : Nat.card { P : (WeierstrassCurve.toAffine (W.baseChange F)).Point // n • P = T } = n.natAbs ^ 2

[n] is n ²-to-one where it hits at all, over an algebraically closed field in which n is invertible.