The unique place at infinity of a Weierstrass function field

For the Weierstrass equation, put t = x⁻¹ and z = y t². The transformed equation is monic in z, so z belongs to the integral closure of the valuation ring at infinity. Modulo any prime above infinity it first gives z = 0, and then t ∈ P². Thus every such prime has ramification index two. The fundamental ramification–inertia identity for the quadratic extension then proves that the prime is unique and has inertia degree one.

@[instance_reducible]

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

The canonical constant-field algebra structure used locally in the infinity chart.

Equations

• WeierstrassCurve.Affine.Chart.instAlgebraConstants K = FunctionField.algebraConstants k K

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

theorem WeierstrassCurve.Affine.Chart.instCoordinateConstantsTower {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] : IsScalarTower k W.CoordinateRing K

theorem WeierstrassCurve.Affine.Chart.instFaithfulInfinity {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (RatFunc k) K] : FaithfulSMul ↥(FunctionField.Chart.inftyValuationSubring k) ↥(FunctionField.Chart.infiniteIntegers k K)

theorem WeierstrassCurve.Affine.Chart.instNoZeroSMulDivisorsInfinity {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (RatFunc k) K] : NoZeroSMulDivisors ↥(FunctionField.Chart.inftyValuationSubring k) ↥(FunctionField.Chart.infiniteIntegers k K)

theorem WeierstrassCurve.Affine.Chart.instInfinityConstantsTower {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : IsScalarTower k (↥(FunctionField.Chart.inftyValuationSubring k)) K

theorem WeierstrassCurve.Affine.Chart.xCoord_eq_XK {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] : (algebraMap W.CoordinateRing K) ((CoordinateRing.mk W) (Polynomial.C Polynomial.X)) = FunctionField.Chart.XK k K

theorem WeierstrassCurve.Affine.Chart.yCoord_equation {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] : (W.baseChange K).Equation (FunctionField.Chart.XK k K) (W.yCoord K)

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

The integral infinity-chart coordinate z = y t².

Equations

• WeierstrassCurve.Affine.Chart.infinityZ W K = W.yCoord K * FunctionField.Chart.tK k K ^ 2

theorem WeierstrassCurve.Affine.Chart.infinityZ_equation {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] : infinityZ W K ^ 2 + ((algebraMap k K) W.a₁ * FunctionField.Chart.tK k K + (algebraMap k K) W.a₃ * FunctionField.Chart.tK k K ^ 2) * infinityZ W K - (FunctionField.Chart.tK k K + (algebraMap k K) W.a₂ * FunctionField.Chart.tK k K ^ 2 + (algebraMap k K) W.a₄ * FunctionField.Chart.tK k K ^ 3 + (algebraMap k K) W.a₆ * FunctionField.Chart.tK k K ^ 4) = 0

theorem WeierstrassCurve.Affine.Chart.infinityZ_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 (↥(FunctionField.Chart.inftyValuationSubring k)) (infinityZ W K)

noncomputable def WeierstrassCurve.Affine.Chart.infinityZInt {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] : ↥(FunctionField.Chart.infiniteIntegers k K)

The infinity-chart coordinate z as an element of the integral closure at infinity.

Equations

• WeierstrassCurve.Affine.Chart.infinityZInt W K = ⟨WeierstrassCurve.Affine.Chart.infinityZ W K, ⋯⟩

noncomputable def WeierstrassCurve.Affine.Chart.infinityTInt {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (RatFunc k) K] : ↥(FunctionField.Chart.infiniteIntegers k K)

The local parameter t = X⁻¹ in the integral closure at infinity.

Equations

• WeierstrassCurve.Affine.Chart.infinityTInt K = (algebraMap ↥(FunctionField.Chart.inftyValuationSubring k) ↥(FunctionField.Chart.infiniteIntegers k K)) (FunctionField.Chart.tA k)

theorem WeierstrassCurve.Affine.Chart.infinityZInt_equation {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] : have z := infinityZInt W K; have t := infinityTInt K; have c := (algebraMap ↥(FunctionField.Chart.inftyValuationSubring k) ↥(FunctionField.Chart.infiniteIntegers k K)).comp (algebraMap k ↥(FunctionField.Chart.inftyValuationSubring k)); z ^ 2 + (c W.a₁ * t + c W.a₃ * t ^ 2) * z - (t + c W.a₂ * t ^ 2 + c W.a₄ * t ^ 3 + c W.a₆ * t ^ 4) = 0

theorem WeierstrassCurve.Affine.Chart.infinity_map_maximalIdeal_le_sq {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] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.Chart.infiniteIntegers k K)) : Ideal.map (algebraMap ↥(FunctionField.Chart.inftyValuationSubring k) ↥(FunctionField.Chart.infiniteIntegers k K)) (IsLocalRing.maximalIdeal ↥(FunctionField.Chart.inftyValuationSubring k)) ≤ v.asIdeal ^ 2

theorem WeierstrassCurve.Affine.Chart.infinity_ramificationIdx_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] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.Chart.infiniteIntegers k K)) : (IsLocalRing.maximalIdeal ↥(FunctionField.Chart.inftyValuationSubring k)).ramificationIdx' v.asIdeal = 2

theorem WeierstrassCurve.Affine.Chart.infinity_sum_ramification_inertia {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] [Algebra.IsSeparable (RatFunc k) K] : have p := IsLocalRing.maximalIdeal ↥(FunctionField.Chart.inftyValuationSubring k); ∑ P ∈ IsDedekindDomain.primesOverFinset p ↥(FunctionField.Chart.infiniteIntegers k K), p.ramificationIdx' P * p.inertiaDeg' P = 2

theorem WeierstrassCurve.Affine.Chart.infinity_inertiaDeg_eq_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] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.Chart.infiniteIntegers k K)) : (IsLocalRing.maximalIdeal ↥(FunctionField.Chart.inftyValuationSubring k)).inertiaDeg' v.asIdeal = 1

theorem WeierstrassCurve.Affine.Chart.infinity_heightOne_unique {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] [Algebra.IsSeparable (RatFunc k) K] (v w : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.Chart.infiniteIntegers k K)) : v = w

noncomputable def WeierstrassCurve.Affine.Chart.infinityHeightOne {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (RatFunc k) K] : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.Chart.infiniteIntegers k K)

The unique height-one prime in the integral closure of the infinity valuation ring.

Equations

• WeierstrassCurve.Affine.Chart.infinityHeightOne K = { asIdeal := Classical.choose ⋯, isPrime := ⋯, ne_bot := ⋯ }

noncomputable def WeierstrassCurve.Affine.Chart.infinityPlace {k : Type u_1} [Field k] (K : Type u_2) [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] : FunctionField.Chart.PlaceA k K

The unique place of the elliptic function field above the point at infinity.

Equations

• WeierstrassCurve.Affine.Chart.infinityPlace K = Sum.inr (WeierstrassCurve.Affine.Chart.infinityHeightOne K)

theorem WeierstrassCurve.Affine.Chart.infinityPlace_deg_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] [_root_.FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : FunctionField.Chart.placeDegree k K (infinityPlace K) = 1