The function field is generated by the y-coordinate

F(W) = F(x)(y): the function field is generated over the rational functions of the affine coordinate x by the single element y. The coordinate ring is free of rank two over F[X] with basis {1, y}, so every one of its elements is p + q y with p and q polynomial in x; the function field is its fraction field, so a subfield containing the image of the coordinate ring is everything.

Together with finrank_ratFuncRange, which puts the degree at two, this is what makes y a primitive element of the extension — the form in which questions about F(W)/F(x) reduce to questions about the minimal polynomial of y.

The base is any field L between F[X] and F(W), following finrank_functionField in Finrank.lean, so that the statement serves RatFunc F and FractionRing F[X] alike. What it needs of L is the algebra structures displayed below together with their scalar-tower compatibility; being a fraction field of F[X] is not among them.

Main results

• WeierstrassCurve.Affine.adjoin_genericY_eq_top: F(x)⟮y⟯ = F(W).
• WeierstrassCurve.Affine.minpoly_genericY: the minimal polynomial of y is the Weierstrass polynomial itself. This is generation and degree read together, so it lives here; it needs L to be a fraction field of F[X], which the statement above does not.
• WeierstrassCurve.Affine.adjoin_genericX_genericY_eq_top: over the constants, K⟮x, y⟯ = K(W), and WeierstrassCurve.Affine.fieldRange_eq_adjoin_genericX_genericY: the image of K(W) under an embedding over K is generated by the images of x and y.
• WeierstrassCurve.Affine.fieldRange_eq_adjoin_range_pow: an embedding K(W') → K(W) carrying the generic point of W' to the q-th powers of that of W, and whose image contains every q-th power, has image K(K(W)^q). The one-step and the iterated relative Frobenius each supply their own values at the generic point and read off their pulled-back function field.

Provenance

minpoly_genericY corresponds to the inline step h_eq inside functionField_isSeparable of projects/HasseWeil/HasseWeil/Ramification.lean in AINTLIB at revision 513e83879e2f, Apache-2.0, exported here as a statement in its own right and proved from generation rather than from Gauss's lemma.

The coordinate-ring containment follows the plan of algebraMap_mem_adjoin_genericX_genericY in Affine/FunctionField/GenericPoint/Basic.lean, which proves the analogous statement for the F-subalgebra generated by both coordinates: the same basis decomposition and scalar-action step. It is not derived from that theorem, because passing from an F-subalgebra to an L-subfield would force an Algebra F L instance that nothing else here needs. The fraction-field step is Mathlib's IsFractionRing.closure_range_algebraMap (Mathlib/RingTheory/Localization/FractionRing.lean), that the image of the ring generates its fraction field as a subfield. What is new here is only their combination, and the observation that no IsFractionRing F[X] L hypothesis is needed for it.

theorem WeierstrassCurve.Affine.algebraMap_mem_adjoin_genericY {F : Type u_1} [CommRing F] [IsDomain F] (W' : Affine F) (L : Type u_2) [Field L] [Algebra (Polynomial F) L] [Algebra L W'.FunctionField] [IsScalarTower (Polynomial F) L W'.FunctionField] (w : W'.CoordinateRing) : (algebraMap W'.CoordinateRing W'.FunctionField) w ∈ L⟮W'.genericY⟯

Every element of the coordinate ring lies in a subfield of the function field that contains the image of F[X] and the generic y-coordinate: it is p + q y with p and q polynomial in x.

theorem WeierstrassCurve.Affine.adjoin_genericY_eq_top {F : Type u_1} [CommRing F] [IsDomain F] (W' : Affine F) (L : Type u_2) [Field L] [Algebra (Polynomial F) L] [Algebra L W'.FunctionField] [IsScalarTower (Polynomial F) L W'.FunctionField] : L⟮W'.genericY⟯ = ⊤

The function field is generated by the generic y-coordinate over any field L carrying the image of F[X]: L⟮y⟯ = F(W). Taking L = F(x) gives F(x)⟮y⟯ = F(W), which is the form that makes y a primitive element of the quadratic extension.

@[simp]

theorem WeierstrassCurve.Affine.minpoly_genericY {F : Type u_1} [CommRing F] [IsDomain F] (W' : Affine F) (L : Type u_3) [Field L] [Algebra (Polynomial F) L] [IsFractionRing (Polynomial F) L] [Algebra L W'.FunctionField] [IsScalarTower (Polynomial F) L W'.FunctionField] : minpoly L W'.genericY = Polynomial.map (algebraMap (Polynomial F) L) W'.polynomial

The Weierstrass polynomial is the minimal polynomial of y. The equation defining the curve is exactly the relation y satisfies over L, and it has no smaller one.

theorem WeierstrassCurve.Affine.adjoin_genericX_genericY_eq_top {K : Type u_3} [Field K] (W : Affine K) : K⟮W.genericX, W.genericY⟯ = ⊤

The function field is generated over the constants by the generic point: K⟮x, y⟯ = K(W). This is the form of generation that computes the image of an embedding of K(W) over K from its two values at x and y (fieldRange_eq_adjoin_genericX_genericY).

theorem WeierstrassCurve.Affine.fieldRange_eq_adjoin_genericX_genericY {K : Type u_3} [Field K] (W : Affine K) {L : Type u_4} [Field L] [Algebra K L] (f : W.FunctionField →ₐ[K] L) : f.fieldRange = K⟮f W.genericX, f W.genericY⟯

The image of the function field under an embedding over the constants is generated by the images of the generic coordinates: f(K(W)) = K⟮f x, f y⟯. This computes the image of a function-field embedding — the pullback of an isogeny, say — from its values at the two coordinates.

theorem WeierstrassCurve.Affine.fieldRange_eq_adjoin_range_pow {K : Type u_3} [Field K] (W : Affine K) {W' : Affine K} {q : ℕ} (f : W'.FunctionField →ₐ[K] W.FunctionField) (hx : f W'.genericX = W.genericX ^ q) (hy : f W'.genericY = W.genericY ^ q) (h : ∀ (z : W.FunctionField), z ^ q ∈ f.fieldRange) : f.fieldRange = IntermediateField.adjoin K (Set.range fun (z : W.FunctionField) => z ^ q)

An embedding K(W') → K(W) carrying the generic point to q-th powers has image K(K(W)^q), the subfield generated over the constants by the q-th powers, provided every q-th power lies in its image. The image is generated by the two values x ^ q, y ^ q at the generic point, and conversely every q-th power is in it by hypothesis.