The Frobenius trace of a reduction, and the local polynomial

Over the fraction field of a discrete valuation ring with finite residue field, the reduction of a minimal Weierstrass equation is a Weierstrass model over a finite field, so it has a Frobenius trace a = q + 1 − #W(k), counted with its singular point. This file evaluates that trace at bad reduction: it is 1 at split multiplicative, -1 at nonsplit multiplicative, and 0 at additive reduction. At good reduction it is the classical trace q + 1 − #E(k) of the smooth reduction.

These are exactly the coefficients of T in Mathlib's WeierstrassCurve.localPolynomial, which is defined by cases on the reduction type. Read through the trace, the case split collapses: the local polynomial is 1 − a T + q T² at good reduction and 1 − a T otherwise.

Main results

• WeierstrassCurve.reduction_Δ_eq_zero_iff, WeierstrassCurve.HasMultiplicativeReduction.reduction_c₄_ne_zero, WeierstrassCurve.HasMultiplicativeReduction.reduction_c₆_ne_zero and WeierstrassCurve.HasAdditiveReduction.reduction_c₄_eq_zero: the reduction types read on the invariants of the reduced model.
• WeierstrassCurve.HasMultiplicativeReduction.splits_nodePolynomial_reduction_iff: a multiplicative reduction is split exactly when the reduced model's node polynomial splits.
• WeierstrassCurve.HasSplitMultiplicativeReduction.frobeniusTrace_reduction_eq_one, WeierstrassCurve.HasMultiplicativeReduction.frobeniusTrace_reduction_eq_neg_one and WeierstrassCurve.HasAdditiveReduction.frobeniusTrace_reduction_eq_zero: the trace of the reduction is 1, -1 and 0 at split multiplicative, nonsplit multiplicative and additive reduction.
• WeierstrassCurve.localPolynomial_eq_of_hasGoodReduction and WeierstrassCurve.localPolynomial_eq_of_not_hasGoodReduction: the local polynomial is 1 − a T + q T² at good reduction and 1 − a T at bad reduction, with a the trace of the reduction.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.5 and Appendix C.16.

theorem WeierstrassCurve.reduction_Δ_eq_zero_iff (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [IsMinimal R W] : (reduction R W).Δ = 0 ↔ ¬HasGoodReduction R W

The reduction is singular exactly when it is bad.

theorem WeierstrassCurve.HasMultiplicativeReduction.reduction_c₄_ne_zero (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} (h : HasMultiplicativeReduction R W) : (reduction R W).c₄ ≠ 0

A multiplicative reduction has c₄ ≠ 0: its singular point is a node.

theorem WeierstrassCurve.HasMultiplicativeReduction.reduction_c₆_ne_zero (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} (h : HasMultiplicativeReduction R W) : (reduction R W).c₆ ≠ 0

A multiplicative reduction has c₆ ≠ 0. By 1728 Δ = c₄³ - c₆² on the reduced model, the vanishing of Δ and the nonvanishing of c₄ there force that of c₆.

theorem WeierstrassCurve.HasAdditiveReduction.reduction_c₄_eq_zero (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} (h : HasAdditiveReduction R W) : (reduction R W).c₄ = 0

An additive reduction has c₄ = 0: its singular point is a cusp.

theorem WeierstrassCurve.HasMultiplicativeReduction.splits_nodePolynomial_reduction_iff (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} (h : HasMultiplicativeReduction R W) : (reduction R W).nodePolynomial.Splits ↔ HasSplitMultiplicativeReduction R W

A multiplicative reduction is split exactly when the node polynomial of the reduced model splits, which is HasSplitMultiplicativeReduction read on the reduced model.

theorem WeierstrassCurve.HasSplitMultiplicativeReduction.frobeniusTrace_reduction_eq_one (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [Finite (IsLocalRing.ResidueField R)] (h : HasSplitMultiplicativeReduction R W) : (reduction R W).frobeniusTrace = 1

The Frobenius trace of a split multiplicative reduction is 1.

theorem WeierstrassCurve.HasMultiplicativeReduction.frobeniusTrace_reduction_eq_neg_one (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [Finite (IsLocalRing.ResidueField R)] (h : HasMultiplicativeReduction R W) (hs : ¬HasSplitMultiplicativeReduction R W) : (reduction R W).frobeniusTrace = -1

The Frobenius trace of a nonsplit multiplicative reduction is -1.

theorem WeierstrassCurve.HasAdditiveReduction.frobeniusTrace_reduction_eq_zero (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [Finite (IsLocalRing.ResidueField R)] (h : HasAdditiveReduction R W) : (reduction R W).frobeniusTrace = 0

The Frobenius trace of an additive reduction is 0.

theorem WeierstrassCurve.localPolynomial_eq_of_hasGoodReduction (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [Finite (IsLocalRing.ResidueField R)] (W : WeierstrassCurve K) (h : HasGoodReduction R (minimal R W)) : localPolynomial R W = 1 - Polynomial.C (reduction R (minimal R W)).frobeniusTrace * Polynomial.X + Polynomial.C ↑(Nat.card (IsLocalRing.ResidueField R)) * Polynomial.X ^ 2

At good reduction the local polynomial is 1 − a T + q T², with a the Frobenius trace of the reduction and q the size of the residue field.

theorem WeierstrassCurve.localPolynomial_eq_of_not_hasGoodReduction (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [Finite (IsLocalRing.ResidueField R)] (W : WeierstrassCurve K) (h : ¬HasGoodReduction R (minimal R W)) : localPolynomial R W = 1 - Polynomial.C (reduction R (minimal R W)).frobeniusTrace * Polynomial.X

At bad reduction the local polynomial is 1 − a T, with a the Frobenius trace of the reduction. This one formula covers the split multiplicative, nonsplit multiplicative and additive cases of the definition.