Points of Weierstrass curves over finite fields: decidability and finiteness

Source: MichaelStollBayreuth/EllipticCurves at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f. Exact-pin changes are documented in PORTING.md.

This file provides Decidable instances for the predicates WeierstrassCurve.Affine.Equation and WeierstrassCurve.Affine.Nonsingular (over any commutative ring with decidable equality), and deduces Finite and Fintype instances for the type WeierstrassCurve.Affine.Point of nonsingular points of a Weierstrass curve over a finite ring, via Mathlib's WeierstrassCurve.Affine.nonsingularPointEquiv.

The decision procedure goes through equation_iff/nonsingular_iff, so it evaluates the Weierstrass polynomials directly in the base ring, with no Polynomial arithmetic involved. Consequently, for a concrete curve over ZMod p the number of points is computable by decide: Fintype.card W.Point enumerates the pairs in ZMod p × ZMod p and filters by the (decidable) nonsingularity condition.

We also provide WeierstrassCurve.Affine.Point.mapEquiv, the group isomorphism on points induced by an isomorphism of base fields (the equiv version of WeierstrassCurve.Affine.Point.map); it transports point counts along residue-field identifications such as ℤ ⧸ (p) ≃+* ZMod p.

@[instance_reducible]

instance WeierstrassCurve.Affine.instDecidableEquationOfDecidableEq {R : Type u_1} [CommRing R] {W' : Affine R} [DecidableEq R] (x y : R) : Decidable (W'.Equation x y)

Equations

• WeierstrassCurve.Affine.instDecidableEquationOfDecidableEq x y = decidable_of_iff (y ^ 2 + W'.a₁ * x * y + W'.a₃ * y = x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆) ⋯

@[instance_reducible]

instance WeierstrassCurve.Affine.instDecidableNonsingularOfDecidableEq {R : Type u_1} [CommRing R] {W' : Affine R} [DecidableEq R] (x y : R) : Decidable (W'.Nonsingular x y)

Equations

• WeierstrassCurve.Affine.instDecidableNonsingularOfDecidableEq x y = decidable_of_iff (W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ -y - W'.a₁ * x - W'.a₃)) ⋯

instance WeierstrassCurve.Affine.instFinitePoint {R : Type u_1} [CommRing R] {W' : Affine R} [Finite R] : Finite W'.Point

@[instance_reducible]

instance WeierstrassCurve.Affine.instFintypePointOfDecidableEq {R : Type u_1} [CommRing R] {W' : Affine R} [Fintype R] [DecidableEq R] : Fintype W'.Point

Equations

• WeierstrassCurve.Affine.instFintypePointOfDecidableEq = Fintype.ofEquiv (Option { xy : R × R // W'.Nonsingular xy.1 xy.2 }) W'.nonsingularPointEquiv.symm

theorem WeierstrassCurve.Affine.baseChange_self {K : Type u_2} [Field K] (W : Affine K) : toAffine (W.baseChange K) = W

Base change from a field to itself leaves an affine Weierstrass curve unchanged.

def WeierstrassCurve.Affine.Point.congr {K : Type u_2} [Field K] [DecidableEq K] {W₁ W₂ : Affine K} (h : W₁ = W₂) : W₁.Point ≃+ W₂.Point

Transport of points along an equality of Weierstrass curves.

Equations

• WeierstrassCurve.Affine.Point.congr h = h ▸ AddEquiv.refl W₁.Point

theorem WeierstrassCurve.Affine.Point.congr_zero {K : Type u_2} [Field K] [DecidableEq K] {W₁ W₂ : Affine K} (h : W₁ = W₂) : (congr h) 0 = 0

theorem WeierstrassCurve.Affine.Point.congr_some {K : Type u_2} [Field K] [DecidableEq K] {W₁ W₂ : Affine K} (h : W₁ = W₂) {x y : K} (hp : W₁.Nonsingular x y) : (congr h) (some x y hp) = some x y ⋯

noncomputable def WeierstrassCurve.Affine.pointMap {K : Type u_2} [Field K] (W : Affine K) [DecidableEq K] (L : Type u_3) [Field L] [Algebra K L] [DecidableEq L] : W.Point →+ (toAffine (W.baseChange L)).Point

The base-change homomorphism on points induced by a field extension.

Equations

• W.pointMap L = (WeierstrassCurve.Affine.Point.map (Algebra.ofId K L)).comp (WeierstrassCurve.Affine.Point.congr ⋯).toAddMonoidHom

theorem WeierstrassCurve.Affine.pointMap_zero {K : Type u_2} [Field K] (W : Affine K) [DecidableEq K] (L : Type u_3) [Field L] [Algebra K L] [DecidableEq L] : (W.pointMap L) 0 = 0

theorem WeierstrassCurve.Affine.pointMap_nonsingular {K : Type u_2} [Field K] (W : Affine K) (L : Type u_3) [Field L] [Algebra K L] {x y : K} (h : W.Nonsingular x y) : (toAffine (W.baseChange L)).Nonsingular ((algebraMap K L) x) ((algebraMap K L) y)

Base change preserves nonsingularity, with the target expressed using the canonical base-changed affine curve.

theorem WeierstrassCurve.Affine.pointMap_some {K : Type u_2} [Field K] (W : Affine K) [DecidableEq K] (L : Type u_3) [Field L] [Algebra K L] [DecidableEq L] {x y : K} (h : W.Nonsingular x y) : (W.pointMap L) (Point.some x y h) = Point.some ((algebraMap K L) x) ((algebraMap K L) y) ⋯

theorem WeierstrassCurve.Affine.pointMap_injective {K : Type u_2} [Field K] (W : Affine K) [DecidableEq K] (L : Type u_3) [Field L] [Algebra K L] [DecidableEq L] : Function.Injective ⇑(W.pointMap L)

Base change of points along a field extension is injective.

noncomputable def WeierstrassCurve.Affine.Point.mapEquiv {R : Type u_1} [CommRing R] {W' : Affine R} {S : Type u_2} {F : Type u_3} {K : Type u_4} [CommRing S] [Field F] [Field K] [DecidableEq F] [DecidableEq K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (σ : F ≃ₐ[S] K) : (W'.baseChange F).Point ≃+ (W'.baseChange K).Point

The group isomorphism on nonsingular points induced by an algebra isomorphism σ : F ≃ₐ[S] K, where W is defined over a subring of a ring S, and F and K are field extensions of S; the equiv version of WeierstrassCurve.Affine.Point.map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.Affine.Point.coe_mapEquiv {R : Type u_1} [CommRing R] {W' : Affine R} {S : Type u_2} {F : Type u_3} {K : Type u_4} [CommRing S] [Field F] [Field K] [DecidableEq F] [DecidableEq K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (σ : F ≃ₐ[S] K) : ⇑(mapEquiv σ) = ⇑(map ↑σ)