The nonsingular group of an additive special Weierstrass cubic

Over the residue fields at five and eleven, a Weierstrass cubic with vanishing discriminant and c₄ is cuspidal. This file proves the precise group-theoretic form needed by the tame additive reduction consumer: its group of nonsingular points is additively equivalent to the residue field.

The proof normalizes the equation to short Weierstrass form, where the two invariant equalities force the equation to be Y² = X³. The cardinality of that one concrete nonsingular point type is then checked by finite enumeration over ZMod 5 and ZMod 11. Prime cardinality supplies the additive group equivalence; no Hasse bound or ellipticity assumption is used.

def MazurTorsion.EllipticCurve.cuspidalShortCurve (F : Type u_1) [CommRing F] : WeierstrassCurve F

The standard cuspidal short Weierstrass equation Y² = X³.

Equations

• MazurTorsion.EllipticCurve.cuspidalShortCurve F = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 0, a₆ := 0 }

theorem MazurTorsion.EllipticCurve.card_cuspidalShortCurve_five : Fintype.card (cuspidalShortCurve (ZMod 5)).toAffine.Point = 5

The standard cusp has five nonsingular projective points over F₅.

theorem MazurTorsion.EllipticCurve.card_cuspidalShortCurve_eleven : Fintype.card (cuspidalShortCurve (ZMod 11)).toAffine.Point = 11

The standard cusp has eleven nonsingular projective points over F₁₁.

theorem MazurTorsion.EllipticCurve.short_eq_cuspidal_of_invariants {F : Type u_1} [Field F] [Invertible 2] [Invertible 3] (W : WeierstrassCurve F) [W.IsShortNF] (hΔ : W.Δ = 0) (hc₄ : W.c₄ = 0) : W = cuspidalShortCurve F

A short Weierstrass equation with vanishing discriminant and c₄ is the standard cusp in every characteristic different from two and three.

theorem MazurTorsion.EllipticCurve.exists_affine_singular_of_cuspidal {F : Type u_1} [Field F] (W : WeierstrassCurve F) (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) (hΔ : W.Δ = 0) (hc₄ : W.c₄ = 0) : ∃ (x : F) (y : F), W.toAffine.Equation x y ∧ ¬W.toAffine.Nonsingular x y

A Weierstrass cubic with vanishing discriminant and c₄ has an affine singular point whenever two and three are nonzero in the ground field. The proof normalizes to the standard cusp and transports its origin back through the admissible variable change.

theorem MazurTorsion.EllipticCurve.natCard_point_eq_five_of_cuspidal (W : WeierstrassCurve (ZMod 5)) (hΔ : W.Δ = 0) (hc₄ : W.c₄ = 0) : Nat.card W.toAffine.Point = 5

A Weierstrass cubic over F₅ with vanishing discriminant and c₄ has exactly five nonsingular projective points.

theorem MazurTorsion.EllipticCurve.natCard_point_eq_eleven_of_cuspidal (W : WeierstrassCurve (ZMod 11)) (hΔ : W.Δ = 0) (hc₄ : W.c₄ = 0) : Nat.card W.toAffine.Point = 11

A Weierstrass cubic over F₁₁ with vanishing discriminant and c₄ has exactly eleven nonsingular projective points.

noncomputable def MazurTorsion.EllipticCurve.pointAddEquivZModFiveOfCuspidal (W : WeierstrassCurve (ZMod 5)) (hΔ : W.Δ = 0) (hc₄ : W.c₄ = 0) : W.toAffine.Point ≃+ ZMod 5

The nonsingular point group of a cuspidal Weierstrass cubic over F₅ is the additive group of F₅.

Equations

• MazurTorsion.EllipticCurve.pointAddEquivZModFiveOfCuspidal W hΔ hc₄ = addEquivOfPrimeCardEq ⋯ MazurTorsion.EllipticCurve.pointAddEquivZModFiveOfCuspidal._proof_2

noncomputable def MazurTorsion.EllipticCurve.pointAddEquivZModElevenOfCuspidal (W : WeierstrassCurve (ZMod 11)) (hΔ : W.Δ = 0) (hc₄ : W.c₄ = 0) : W.toAffine.Point ≃+ ZMod 11

The nonsingular point group of a cuspidal Weierstrass cubic over F₁₁ is the additive group of F₁₁.

Equations

• MazurTorsion.EllipticCurve.pointAddEquivZModElevenOfCuspidal W hΔ hc₄ = addEquivOfPrimeCardEq ⋯ MazurTorsion.EllipticCurve.pointAddEquivZModElevenOfCuspidal._proof_2

@[instance_reducible]

noncomputable def MazurTorsion.EllipticCurve.cuspidalDecidableEqResidueAtFive : DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atFive))

Equations

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

@[instance_reducible]

noncomputable def MazurTorsion.EllipticCurve.cuspidalDecidableEqResidueAtEleven : DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven))

Equations

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

noncomputable def MazurTorsion.EllipticCurve.specialFiberPointAddEquivAtFiveOfCuspidal (W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atFive)) (hΔ : WeierstrassCurve.Δ (WeierstrassCurve.Affine.adicRedCurve W₀) = 0) (hc₄ : WeierstrassCurve.c₄ (WeierstrassCurve.Affine.adicRedCurve W₀) = 0) : (WeierstrassCurve.Affine.adicRedCurve W₀).Point ≃+ IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atFive)

The nonsingular point group of the actual five-adic special fibre is the additive residue field when its discriminant and c₄ vanish.

Equations

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

noncomputable def MazurTorsion.EllipticCurve.specialFiberPointAddEquivAtElevenOfCuspidal (W₀ : WeierstrassCurve ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)) (hΔ : WeierstrassCurve.Δ (WeierstrassCurve.Affine.adicRedCurve W₀) = 0) (hc₄ : WeierstrassCurve.c₄ (WeierstrassCurve.Affine.adicRedCurve W₀) = 0) : (WeierstrassCurve.Affine.adicRedCurve W₀).Point ≃+ IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ IntegerPrimeSpecialization.atEleven)

The analogous checked cuspidal classification for the actual eleven-adic special fibre.

Equations

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