Kraus's criterion: which pairs of invariants come from an integral equation

A pair (c₄, c₆) in a field K where 2 and 3 are invertible, with c₄³ ≠ c₆², is the pair of c-invariants of exactly one Weierstrass equation up to a change of variables with u = 1, namely ofCInvariants c₄ c₆ : y² = x³ - (c₄/48)x - c₆/864. Given a commutative ring R with an algebra map to K — a localisation 𝒪_{K,v} of a ring of integers, in the application — the question Kraus answers is a different one: is there an equation whose coefficients come from R and whose invariants are c₄ and c₆ on the nose? Integrality of c₄, c₆ and Δ is necessary but not sufficient, and what is missing is visible only at the residue characteristics 2 and 3, where the coefficients a₁, a₂, a₃ of the sought equation have to absorb the denominators of ofCInvariants c₄ c₆.

This file states that obstruction as Kraus's local condition and proves it exact: over a local ring the condition holds precisely when an integral equation with those invariants exists. Over a Dedekind domain O with fraction field K the local conditions at all height-one primes are then shown to patch: they hold everywhere exactly when a single equation with coefficients in O has invariants c₄ and c₆. Because every equation is the (b₂/12, a₁/2, a₃/2)-transform of the canonical one (WeierstrassCurve.smul_ofCInvariants), the auxiliary data of the criterion is a candidate for those coefficients — a single b₂ above 3, where completing the square is free, and a pair (a₁, a₃) above 2, where completing the cube is free.

Main definitions

• TauCeti.HasKrausThreeWitness: some b₂ ∈ R makes the (b₂/12, 0, 0)-transform of ofCInvariants c₄ c₆ integral.
• TauCeti.HasKrausTwoWitness: some a₁, a₃ ∈ R make the (a₁²/12, a₁/2, a₃/2)-transform of ofCInvariants c₄ c₆ integral. Each triple specialises the general prescription (b₂/12, a₁/2, a₃/2): the three-witness sets a₁ = a₃ = 0, while the two-witness sets a₂ = 0, so b₂ = a₁².
• TauCeti.KrausLocalCondition: integrality of c₄, c₆ and Δ, nonvanishing of Δ, and the two witness conditions, each imposed only when the corresponding numeral is a nonunit.
• TauCeti.KrausGlobalCondition: Kraus's local condition at the localisation of a Dedekind domain at every height-one prime.

Main results

• TauCeti.krausLocalCondition_iff_exists_integralModel: over a local ring the condition holds exactly when some Weierstrass equation with coefficients in R has c-invariants c₄ and c₆ and nonzero discriminant.
• TauCeti.isIntegral_ofCInvariants: where 6 is a unit and c₄, c₆ lie in the image of R, the canonical equation is itself integral, so no auxiliary data is needed;
• TauCeti.krausLocalCondition_of_isUnit_six: consequently the condition is automatic there, given only the integrality and nonvanishing of the invariants.
• TauCeti.krausGlobalCondition_iff_exists_integralModel: over a Dedekind domain with at least one height-one prime, the global condition holds exactly when some Weierstrass equation with coefficients in O has c-invariants c₄ and c₆ and nonzero discriminant.

Patching the local witnesses

Every witness is a change of variables (B/12, A/2, G/2) with u = 1 and A, B, G in the local ring. Two such triples give the same integrality as soon as the second is congruent to the first modulo 12, after the correction G ↦ G + A·(b - B)/12 of the last entry. The change of variables between the two transforms is then ((b - B)/12, (a - A)/2, (g - G - A(b - B)/12)/2), which has coefficients in the local ring. A single modulus therefore serves the primes above 2 and above 3 alike, and at the remaining primes 12 is a unit. Approximating the local A, B and the corrected G modulo 12 by elements of O (TauCeti.DedekindDomain.exists_forall_sub_mem_span_singleton_localizationAtPrime) produces one global change of variables.

Provenance

Not ported. The criterion and its local auxiliary conditions follow Kraus's paper below; the reduction to a single change of variables off the canonical equation is this file's own.

References

• A. Kraus, Quelques remarques à propos des invariants c₄, c₆ et Δ d'une courbe elliptique, Acta Arith. 54 (1989), 75–80.

def TauCeti.HasKrausThreeWitness (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (c₄ c₆ : K) : Prop

Kraus's witness above 3: some b₂ ∈ R for which the (b₂/12, 0, 0)-transform of the canonical equation ofCInvariants c₄ c₆ has all its coefficients in R. This is the auxiliary datum the criterion requires at a residue characteristic 3, where a change of variables over R can make a₁ and a₃ vanish and b₂ = 4a₂ is the only remaining coefficient.

Equations

• TauCeti.HasKrausThreeWitness R c₄ c₆ = ∃ (b₂ : R), WeierstrassCurve.IsIntegral R ({ u := 1, r := (algebraMap R K) b₂ / 12, s := 0, t := 0 } • WeierstrassCurve.ofCInvariants c₄ c₆)

def TauCeti.HasKrausTwoWitness (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (c₄ c₆ : K) : Prop

Kraus's witness above 2: some a₁, a₃ ∈ R for which the (a₁²/12, a₁/2, a₃/2)-transform of the canonical equation ofCInvariants c₄ c₆ has all its coefficients in R. This is the auxiliary datum the criterion requires at a residue characteristic 2, where a change of variables over R can make a₂ vanish, so that b₂ = a₁²; the triple is the case b₂ = a₁² of the general prescription (b₂/12, a₁/2, a₃/2).

Equations

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

structure TauCeti.KrausLocalCondition (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (c₄ c₆ : K) : Prop

Kraus's local condition on a pair of invariants. The first four fields ask that c₄, c₆ and the discriminant of the canonical equation lie in R and that this discriminant is nonzero; the last two are the auxiliary data, each demanded only at the residue characteristic it concerns.

The structure is stated over any R and K. Where 2 and 3 are invertible in K the first four fields are exactly what an integral equation with these invariants forces: that is how the ← direction of TauCeti.krausLocalCondition_iff_exists_integralModel obtains them, and it is why that direction needs the hypothesis, since without it a pair of c-invariants need not determine the discriminant (WeierstrassCurve.Δ_eq_of_c₄_eq_of_c₆_eq asks for 1728 to be regular). Where 2 and 3 are both units in R the last two fields are vacuous, which is TauCeti.krausLocalCondition_of_isUnit_six.

• exists_c₄ : ∃ (x : R), (algebraMap R K) x = c₄

  c₄ lies in R.

• exists_c₆ : ∃ (x : R), (algebraMap R K) x = c₆

  c₆ lies in R.

• exists_Δ : ∃ (x : R), (algebraMap R K) x = (WeierstrassCurve.ofCInvariants c₄ c₆).Δ

  the discriminant (c₄³ - c₆²)/1728 lies in R.

• Δ_ne_zero : (WeierstrassCurve.ofCInvariants c₄ c₆).Δ ≠ 0

  the pair is nonsingular.

• hasKrausTwoWitness : ¬IsUnit 2 → HasKrausTwoWitness R c₄ c₆

  above 2, a witness.

• hasKrausThreeWitness : ¬IsUnit 3 → HasKrausThreeWitness R c₄ c₆

  above 3, a witness.

theorem TauCeti.isIntegral_ofCInvariants {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {c₄ c₆ : K} (h6 : IsUnit 6) (h₄ : ∃ (x : R), (algebraMap R K) x = c₄) (h₆ : ∃ (x : R), (algebraMap R K) x = c₆) : WeierstrassCurve.IsIntegral R (WeierstrassCurve.ofCInvariants c₄ c₆)

Where 6 is a unit an integral pair of invariants already gives an integral canonical equation. Its two coefficients are -c₄/48 and -c₆/864, so once c₄ and c₆ lie in the image of R so do these, because 48 and 864 are units as soon as 6 is.

theorem TauCeti.krausLocalCondition_of_isUnit_six {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {c₄ c₆ : K} (h6 : IsUnit 6) (h₄ : ∃ (x : R), (algebraMap R K) x = c₄) (h₆ : ∃ (x : R), (algebraMap R K) x = c₆) (hΔ : (WeierstrassCurve.ofCInvariants c₄ c₆).Δ ≠ 0) : KrausLocalCondition R c₄ c₆

Away from the residue characteristics 2 and 3 Kraus's condition carries no auxiliary content: an integral, nonsingular pair of invariants satisfies it outright, because the canonical equation is then already integral and both witness fields are vacuous.

Kraus's global condition over a Dedekind domain

def TauCeti.KrausGlobalCondition {K : Type u_2} [Field K] (O : Type u_3) [CommRing O] [IsDedekindDomain O] [Algebra O K] [IsFractionRing O K] (c₄ c₆ : K) : Prop

Kraus's global condition on a pair of invariants: Kraus's local condition holds over the localisation of the Dedekind domain O at every height-one prime.

Equations

• TauCeti.KrausGlobalCondition O c₄ c₆ = ∀ (v : IsDedekindDomain.HeightOneSpectrum O), TauCeti.KrausLocalCondition (Localization.AtPrime v.asIdeal) c₄ c₆

@[simp]

theorem TauCeti.krausGlobalCondition_iff {K : Type u_2} [Field K] {c₄ c₆ : K} {O : Type u_3} [CommRing O] [IsDedekindDomain O] [Algebra O K] [IsFractionRing O K] : KrausGlobalCondition O c₄ c₆ ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum O), KrausLocalCondition (Localization.AtPrime v.asIdeal) c₄ c₆

Kraus's global condition, unfolded: the local condition at every height-one prime.

theorem TauCeti.krausLocalCondition_iff_exists_integralModel {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {c₄ c₆ : K} [Invertible 2] [Invertible 3] [IsLocalRing R] : KrausLocalCondition R c₄ c₆ ↔ ∃ (W : WeierstrassCurve K), WeierstrassCurve.IsIntegral R W ∧ W.c₄ = c₄ ∧ W.c₆ = c₆ ∧ W.Δ ≠ 0

Kraus's local criterion. For a local ring R with an algebra map to a field K in which 2 and 3 are invertible, the pair (c₄, c₆) is the pair of c-invariants of a nonsingular Weierstrass equation with coefficients in R exactly when Kraus's local condition holds.

The correspondence is concrete in both directions: a witness of KrausLocalCondition is a change of variables carrying ofCInvariants c₄ c₆ to an equation with coefficients in R, and that transform is the model the equivalence produces.

Kraus's global criterion

theorem TauCeti.krausGlobalCondition_iff_exists_integralModel {K : Type u_2} [Field K] {c₄ c₆ : K} {O : Type u_3} [CommRing O] [IsDedekindDomain O] [Algebra O K] [IsFractionRing O K] [Invertible 2] [Invertible 3] [Nonempty (IsDedekindDomain.HeightOneSpectrum O)] : KrausGlobalCondition O c₄ c₆ ↔ ∃ (W : WeierstrassCurve K), WeierstrassCurve.IsIntegral O W ∧ W.c₄ = c₄ ∧ W.c₆ = c₆ ∧ W.Δ ≠ 0

Kraus's global criterion. Let O be a Dedekind domain with fraction field K, in which 2 and 3 are invertible, and assume O has a height-one prime, as the ring of integers of a number field does. Then the pair (c₄, c₆) is the pair of c-invariants of a nonsingular Weierstrass equation with coefficients in O exactly when Kraus's local condition holds at every height-one prime.

The equation produced is the (b₂/12, a₁/2, a₃/2)-transform of ofCInvariants c₄ c₆ for elements a₁, b₂, a₃ of O approximating the local witnesses modulo 12. Without a height-one prime the condition is vacuous and the statement fails, since nothing then forces c₄³ ≠ c₆².