Instance pack for elliptic function fields

For a Weierstrass curve W : WeierstrassCurve.Affine k and an abstract fraction field K of W.CoordinateRing, this file constructs the coordinate-place hypothesis pack required to state the place dictionary: the k[X]- and k⟮X⟯-algebra structures with their scalar towers, the {1, y} basis giving FunctionField k K and [K : k⟮X⟯] = 2, separability of the Weierstrass generator in every characteristic, and (over an algebraically closed base) IsFullConstantField k K.

Curve-side facts: W.CoordinateRing over k[X]

instance WeierstrassCurve.Affine.CoordinateRing.instFinitePolynomial_leanPool {k : Type u_1} [Field k] (W : Affine k) : Module.Finite (Polynomial k) W.CoordinateRing

theorem WeierstrassCurve.Affine.CoordinateRing.algebraMap_polynomial_injective' {k : Type u_1} [Field k] (W : Affine k) : Function.Injective ⇑(algebraMap (Polynomial k) W.CoordinateRing)

instance WeierstrassCurve.Affine.CoordinateRing.instFaithfulSMulPolynomial_leanPool {k : Type u_1} [Field k] (W : Affine k) : FaithfulSMul (Polynomial k) W.CoordinateRing

instance WeierstrassCurve.Affine.CoordinateRing.instIsIntegralPolynomial_leanPool {k : Type u_1} [Field k] (W : Affine k) : Algebra.IsIntegral (Polynomial k) W.CoordinateRing

theorem WeierstrassCurve.Affine.derivative_polynomial {k : Type u_1} [Field k] (W : Affine k) : Polynomial.derivative W.polynomial = W.polynomialY

The derivative (in Y) of the Weierstrass polynomial is W.polynomialY.

theorem WeierstrassCurve.Affine.polynomialY_ne_zero {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] : W.polynomialY ≠ 0

For an elliptic curve, the partial derivative W_Y is nonzero (even in char 2).

Item 1: Algebra k[X] K and towers

@[reducible]

noncomputable def WeierstrassCurve.Affine.algebraPolynomial {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] : Algebra (Polynomial k) K

The k[X]-algebra structure on a fraction field of the coordinate ring, sending X to the coordinate function x.

Equations

• W.algebraPolynomial K = ((algebraMap W.CoordinateRing K).comp (algebraMap (Polynomial k) W.CoordinateRing)).toAlgebra

theorem WeierstrassCurve.Affine.algebraPolynomial_isScalarTower {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] : IsScalarTower (Polynomial k) W.CoordinateRing K

algebraPolynomial is compatible with the coordinate ring inclusion.

theorem WeierstrassCurve.Affine.algebraMap_polynomial_injective {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] : Function.Injective ⇑(algebraMap (Polynomial k) K)

Item 2: Algebra k⟮X⟯ K

@[reducible]

noncomputable def WeierstrassCurve.Affine.algebraRatFunc {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] : Algebra (RatFunc k) K

The rational function field structure on K, lifting k[X] → K to k⟮X⟯.

Equations

• W.algebraRatFunc K = (IsFractionRing.lift ⋯).toAlgebra

theorem WeierstrassCurve.Affine.algebraRatFunc_isScalarTower {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] : IsScalarTower (Polynomial k) (RatFunc k) K

Item 3: FunctionField k K via the localized {1, y} basis

noncomputable def WeierstrassCurve.Affine.yCoord {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] : K

The coordinate function y ∈ K, the image of the AdjoinRoot generator.

Equations

• W.yCoord K = (algebraMap W.CoordinateRing K) ((WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X)

noncomputable def WeierstrassCurve.Affine.basisRatFunc {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : Module.Basis (Fin 2) (RatFunc k) K

The {1, y} basis of K over k⟮X⟯, localized from CoordinateRing.basis.

Equations

• W.basisRatFunc K = Module.Basis.localizationLocalization (RatFunc k) (nonZeroDivisors (Polynomial k)) K (WeierstrassCurve.Affine.CoordinateRing.basis W)

@[simp]

theorem WeierstrassCurve.Affine.basisRatFunc_zero {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : (W.basisRatFunc K) 0 = 1

@[simp]

theorem WeierstrassCurve.Affine.basisRatFunc_one {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : (W.basisRatFunc K) 1 = W.yCoord K

theorem WeierstrassCurve.Affine.functionField {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : _root_.FunctionField k K

A fraction field of an elliptic coordinate ring is a function field.

theorem WeierstrassCurve.Affine.finrank_ratFunc_eq_two {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : Module.finrank (RatFunc k) K = 2

The Weierstrass extension has degree 2 over k(x).

Item 4: separability

theorem WeierstrassCurve.Affine.aeval_yCoord {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : (Polynomial.aeval (W.yCoord K)) (Polynomial.map (algebraMap (Polynomial k) (RatFunc k)) W.polynomial) = 0

theorem WeierstrassCurve.Affine.yCoord_isIntegral {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : IsIntegral (RatFunc k) (W.yCoord K)

theorem WeierstrassCurve.Affine.yCoord_notMem_range {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : W.yCoord K ∉ Set.range ⇑(algebraMap (RatFunc k) K)

theorem WeierstrassCurve.Affine.minpoly_yCoord {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : minpoly (RatFunc k) (W.yCoord K) = Polynomial.map (algebraMap (Polynomial k) (RatFunc k)) W.polynomial

theorem WeierstrassCurve.Affine.isSeparable {k : Type u_1} [Field k] (W : Affine k) (K : Type u_2) [Field K] [Algebra W.CoordinateRing K] [IsFractionRing W.CoordinateRing K] [Algebra (Polynomial k) K] [IsScalarTower (Polynomial k) W.CoordinateRing K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [WeierstrassCurve.IsElliptic W] : Algebra.IsSeparable (RatFunc k) K

The elliptic function field is separable over k(x), in every characteristic.

Constant-field algebra structure (no curve needed)

@[reducible]

noncomputable def FunctionField.algebraConstants (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] : Algebra k K

The constant field structure Algebra k K through k[X].

Equations

• FunctionField.algebraConstants k K = ((algebraMap (Polynomial k) K).comp (algebraMap k (Polynomial k))).toAlgebra

theorem FunctionField.algebraConstants_isScalarTower (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] : IsScalarTower k (Polynomial k) K

Item 5: IsFullConstantField over an algebraically closed base

theorem FunctionField.isFullConstantField_of_isAlgClosed (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [IsAlgClosed k] : IsFullConstantField k K

Over an algebraically closed base field, any field extension has full constant field: an element algebraic over k has a linear minimal polynomial.