Rank two over a Weierstrass curve's rational parameter

Mathlib gives the coordinate ring R[W] a power basis {1, Y} over R[X], and defines the total fraction ring R(W) as its fraction ring. Its rank over any fraction ring of R[X] acting through a compatible scalar tower is two, for any nontrivial commutative base ring R. Over an integral domain these fraction rings are fields. The algebra structure for that pair is Mathlib's FractionRing.liftAlgebra, which is not a general instance because it collides with the identity structure on FractionRing R[X] itself. This file exports the specialized action as an instance. Over a field F, it also computes the degree above the copy of the rational function field that sits inside F(W) as an intermediate field.

Main results

• WeierstrassCurve.Affine.moduleFinite_coordinateRing: the coordinate ring is a finite R[X]-module — the companion of Mathlib's Module.Free instance, which Mathlib has only as a lemma, so instance search cannot reach it.
• WeierstrassCurve.Affine.finrank_coordinateRing: the coordinate ring's Module.finrank over R[X] is two, over any nontrivial commutative base ring.
• WeierstrassCurve.Affine.algebraFractionRingFunctionField: the R(x)-algebra structure on R(W), over any integral domain. Exporting it is enough to bring Mathlib's own FractionRing.liftAlgebra API to bear on this pair — the tower R[X] ⊆ R(x) ⊆ R(W) is then found by instance search, and the induced map is FractionRing.algebraMap_liftAlgebra R[X] W.FunctionField; neither needs restating here.
• WeierstrassCurve.Affine.finrank_functionField: [R(W) : L] = 2 for any commutative fraction ring L of R[X] acting through the polynomial-ring scalar tower — so it serves RatFunc R as well as FractionRing R[X] when R is a field.
• WeierstrassCurve.Affine.finiteDimensional_functionField: the extension is finite-dimensional over any fraction field L of R[X], which finrank = 2 does not give by instance search.
• WeierstrassCurve.Affine.isFunctionField: W.FunctionField is an algebraic function field of one variable over F.
• WeierstrassCurve.Affine.ratFuncRange: the copy of the rational function field F(x) inside F(W), as an IntermediateField. Its API is ratFuncRange_eq_map, the defining equation in the ⊤.map form that IntermediateField.map lemmas consume, and mem_ratFuncRange, the membership characterisation; the body is not exposed, so those two lemmas are the interface.
• WeierstrassCurve.Affine.finrank_ratFuncRange: [F(W) : F(x)] = 2 for that copy. This is the degree above a subfield of F(W) rather than above an abstract L, which is what any argument comparing two subfields of F(W) — a tower, or a relative degree — needs; the two are related by AlgHom.finrank_fieldRange, since the copy and RatFunc F are isomorphic as fields acting on F(W).
• WeierstrassCurve.Affine.relfinrank_map_ratFuncRange_fieldRange: mapping the pair F(x) ⊆ F(W) along a function-field embedding preserves its relative degree two.
• WeierstrassCurve.Affine.finrank_map_ratFuncRange: consequently the image of F(x) sits twice the degree of the image of F(W) below the target.

The degree is useful in function-field towers, such as K(W) ⊇ K(x) ⊇ K(x^q) when computing the degree of Frobenius. It follows from Mathlib's IsFractionRing.finrank_eq: L and R(W) are fraction rings of R[X] and R[W], so their ranks agree, without algebraicity, finiteness or base-change hypotheses.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.

Provenance

Ported from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, dev/hasse-weil @ 513e83879e2f), HasseWeil/FrobeniusIsogeny.lean: the declarations coordinateRing_finite, finrank_coordinateRing_eq_two, its anonymous Algebra (FractionRing K[X]) K(W) instance, and finrank_functionField_eq_two. finiteDimensional_functionField is not in the source.

Changes from the source. They are stated there inside a file that also builds the Frobenius isogeny; here they are separated out, since the degree of R(W) over the rational function field is a fact about the curve and not about any isogeny. The source states everything over a field; here both rank computations need only a nontrivial commutative base ring, and the degree is stated over an arbitrary commutative fraction ring of R[X] rather than over FractionRing R[X] alone. The canonical fraction-field algebra instance still assumes an integral domain, while finiteness over a field L needs no separate domain or nontriviality hypothesis on R.

The source's remaining declarations are not ported, each being reachable without them: its Module K[X] K[W], IsScalarTower K[X] K(x) K(W), Algebra.IsIntegral K[X] K[W] and two FaithfulSMul instances are all found by instance search (algebraMap_poly_injective is now an instance in Affine/Point.lean, and Mathlib has FaithfulSMul.algebraMap_injective); and its isBaseChange_coordToFunc, with the two private localization instances beneath it, is not needed at all — Mathlib's IsFractionRing.finrank_eq states the degree equality outright, and Mathlib has deprecated its own base-change-flavoured version in favour of it.

toAlgHom_ratFuncX and relfinrank_map_ratFuncRange_fieldRange are not ported: the first names the affine coordinate inside the copy of the rational function field, and the second is the IntermediateField.relfinrank_map_map transport of finrank_ratFuncRange, which the source has only in the specialised form finrank_over_frobenius_image.

instance WeierstrassCurve.Affine.moduleFinite_coordinateRing {R : Type u_1} [CommRing R] (W : Affine R) : Module.Finite (Polynomial R) W.CoordinateRing

The coordinate ring is a finite R[X]-module.

@[simp]

theorem WeierstrassCurve.Affine.finrank_coordinateRing {R : Type u_1} [CommRing R] (W : Affine R) [Nontrivial R] : Module.finrank (Polynomial R) W.CoordinateRing = 2

The coordinate ring has rank two over R[X] for any nontrivial commutative base ring.

@[simp]

theorem WeierstrassCurve.Affine.finrank_functionField {R : Type u_1} [CommRing R] (W : Affine R) [Nontrivial R] (L : Type u_2) [CommRing L] [Algebra (Polynomial R) L] [IsFractionRing (Polynomial R) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial R) L W.FunctionField] : Module.finrank L W.FunctionField = 2

The total fraction ring of the coordinate ring has rank two over any fraction ring L of R[X] acting through a compatible scalar tower. When R is an integral domain, this says that the function field is a quadratic extension of the rational function field.

instance WeierstrassCurve.Affine.finiteDimensional_functionField {R : Type u_1} [CommRing R] (W : Affine R) (L : Type u_2) [Field L] [Algebra (Polynomial R) L] [IsFractionRing (Polynomial R) L] [Algebra L W.FunctionField] [IsScalarTower (Polynomial R) L W.FunctionField] : FiniteDimensional L W.FunctionField

The function field is finite-dimensional over any fraction field of R[X]. finrank = 2 does not give this by instance search, and downstream norm/trace/separability arguments need it.

@[instance_reducible]

noncomputable instance WeierstrassCurve.Affine.algebraFractionRingFunctionField {R : Type u_1} [CommRing R] [IsDomain R] (W : Affine R) : Algebra (FractionRing (Polynomial R)) W.FunctionField

The action of R(x) on R(W) obtained by extending the polynomial-ring action to fractions. It supplies the scalar tower R[X] ⊆ R(x) ⊆ R(W).

Equations

• W.algebraFractionRingFunctionField = FractionRing.liftAlgebra (Polynomial R) W.FunctionField

theorem WeierstrassCurve.Affine.isFunctionField {F : Type u_1} [Field F] (W : Affine F) : TauCeti.IsFunctionField F W.FunctionField

The function field of a Weierstrass curve is an algebraic function field of one variable over the base field, the affine coordinate x being a rational parameter: F(W) / F(x) is finite, of degree two.

This is what makes the general theory of places, divisors and degrees applicable to a Weierstrass curve.

noncomputable def WeierstrassCurve.Affine.ratFuncRange {F : Type u_1} [Field F] (W : Affine F) : IntermediateField F W.FunctionField

The image of the rational function field F(x) inside the function field F(W).

Equations

• W.ratFuncRange = (IsScalarTower.toAlgHom F (RatFunc F) W.FunctionField).fieldRange

theorem WeierstrassCurve.Affine.ratFuncRange_eq_map {F : Type u_1} [Field F] (W : Affine F) : W.ratFuncRange = IntermediateField.map (IsScalarTower.toAlgHom F (RatFunc F) W.FunctionField) ⊤

The copy of the rational function field inside F(W) is the image of all of F(x). This is the defining equation of ratFuncRange, in the form that carries it along IntermediateField.map lemmas.

@[simp]

theorem WeierstrassCurve.Affine.toAlgHom_ratFuncX {F : Type u_1} [Field F] (W : Affine F) : (IsScalarTower.toAlgHom F (RatFunc F) W.FunctionField) RatFunc.X = (algebraMap (Polynomial F) W.FunctionField) Polynomial.X

The affine coordinate of W, read as the image of the rational function X.

@[simp]

theorem WeierstrassCurve.Affine.mem_ratFuncRange {F : Type u_1} [Field F] (W : Affine F) {z : W.FunctionField} : z ∈ W.ratFuncRange ↔ ∃ (r : RatFunc F), (IsScalarTower.toAlgHom F (RatFunc F) W.FunctionField) r = z

An element of F(W) lies in the copy of the rational function field exactly when it is the image of a rational function.

@[simp]

theorem WeierstrassCurve.Affine.finrank_ratFuncRange {F : Type u_1} [Field F] (W : Affine F) : Module.finrank (↥W.ratFuncRange) W.FunctionField = 2

[F(W) : F(x)] = 2, for the copy of the rational function field inside F(W): the L = RatFunc F case of finrank_functionField, transported along the embedding by AlgHom.finrank_fieldRange.

@[simp]

theorem WeierstrassCurve.Affine.relfinrank_map_ratFuncRange_fieldRange {F : Type u_1} [Field F] (W : Affine F) {M : Type u_2} [Field M] [Algebra F M] (f : W.FunctionField →ₐ[F] M) : (IntermediateField.map f W.ratFuncRange).relfinrank f.fieldRange = 2

The image of F(W) has degree two over the image of F(x). Mapping the pair F(x) ⊆ F(W) along a function-field embedding preserves its relative degree.

@[simp]

theorem WeierstrassCurve.Affine.finrank_map_ratFuncRange {F : Type u_1} [Field F] (W : Affine F) {M : Type u_2} [Field M] [Algebra F M] (f : W.FunctionField →ₐ[F] M) : Module.finrank (↥(IntermediateField.map f W.ratFuncRange)) M = 2 * Module.finrank (↥f.fieldRange) M

The image of F(x) sits twice the degree of the image of F(W) below the target, the bottom step of the tower having relative degree 2. It converts a degree over the image of F(W) into one over a rational subfield.