The generic x-coordinate is a separating element

For an elliptic curve E over a field F, the function field F(E) is separable over the subfield F⟮genericX E⟯ generated by the affine coordinate x.

No Weierstrass-specific argument is repeated here. isSeparable_functionField already gives the extension separable over any fraction field of F[X] inside F(E), and RatFunc F is one; since genericX E is transcendental over F (transcendental_genericX), RatFunc.algEquivOfTranscendental identifies RatFunc F with F⟮genericX E⟯ compatibly with their two maps into F(E), and Algebra.IsSeparable.of_equiv_equiv carries the separability across.

Together with transcendental_genericX, this separability exhibits genericX E as a separating element of F(E)/F, which is what proves the Kähler differentials of F(E) to have basis dx, and hence basis the invariant differential.

Main results

• WeierstrassCurve.Affine.isSeparable_adjoin_genericX: F(E) is separable over F⟮genericX E⟯.

instance WeierstrassCurve.Affine.isSeparable_adjoin_genericX {F : Type u_1} [Field F] (E : Affine F) [WeierstrassCurve.IsElliptic E] : Algebra.IsSeparable (↥F⟮E.genericX⟯) E.FunctionField

The function field is separable over F⟮x⟯, so that genericX is a separating element of F(E)/F. Together with transcendental_genericX this is what the general separating-element API for function fields runs on: it supplies the separability hypothesis of TauCeti.D_ne_zero_of_separating, TauCeti.span_D_eq_top_of_separating and TauCeti.finrank_kaehlerDifferential_eq_one_of_separating at x = genericX E.