The function field of a Weierstrass curve is a separable extension

The Weierstrass polynomial, read over a fraction field L of F[X], is the minimal polynomial of the generic y-coordinate, and on an elliptic curve it is separable. Since y generates, F(W) is a separable extension of L.

Main results

• WeierstrassCurve.Affine.isSeparable_genericY_iff: y is separable over L exactly when the Y-partial W_Y is a nonzero polynomial.
• WeierstrassCurve.Affine.isSeparable_functionField_iff: the same for the whole extension, y being a generator.
• WeierstrassCurve.Affine.isSeparable_functionField: the instance for an elliptic curve.

L is an arbitrary fraction field of F[X], so RatFunc F and FractionRing F[X] are both covered rather than one being privileged; that is the generality of finrank_functionField, which the degree computation uses.

Separability is equivalent to the condition the argument needs — that the Y-partial W_Y = 2y + a₁x + a₃ is a nonzero polynomial — because that partial is the derivative of the minimal polynomial. In characteristic two its leading term vanishes, so this is not automatic; Δ ≠ 0 implies it (polynomialY_ne_zero), and an elliptic curve is the special case of that.

Provenance

isSeparable_functionField is functionField_isSeparable of projects/HasseWeil/HasseWeil/Ramification.lean in AINTLIB at revision 513e83879e2f, Apache-2.0, there stated for L = FractionRing F[X].

theorem WeierstrassCurve.Affine.isSeparable_genericY_iff {F : Type u_1} [CommRing F] [IsDomain F] (W : Affine F) (L : Type u_2) [Field L] [Algebra (Polynomial F) L] [IsFractionRing (Polynomial F) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial F) L W.FunctionField] : IsSeparable L W.genericY ↔ W.polynomialY ≠ 0

The generic y-coordinate is separable over L exactly when W_Y is nonzero. The minimal polynomial is the Weierstrass polynomial, so its derivative is W_Y.

theorem WeierstrassCurve.Affine.isSeparable_functionField_iff {F : Type u_1} [CommRing F] [IsDomain F] (W : Affine F) (L : Type u_2) [Field L] [Algebra (Polynomial F) L] [IsFractionRing (Polynomial F) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial F) L W.FunctionField] : Algebra.IsSeparable L W.FunctionField ↔ W.polynomialY ≠ 0

The function field is a separable extension of L exactly when W_Y is nonzero. The generic y-coordinate generates, so the extension is separable exactly when it is.

instance WeierstrassCurve.Affine.isSeparable_functionField {F : Type u_1} [CommRing F] [IsDomain F] (W : Affine F) (L : Type u_2) [Field L] [Algebra (Polynomial F) L] [IsFractionRing (Polynomial F) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial F) L W.FunctionField] [WeierstrassCurve.IsElliptic W] : Algebra.IsSeparable L W.FunctionField

The function field of an elliptic curve is a separable extension of L.