The affine coordinate ring of an elliptic curve is Dedekind #
The Weierstrass equation is monic in both affine coordinates. At every prime of its coordinate ring, nonsingularity says that one of the two partial derivatives is a unit. Using the corresponding coordinate realizes the local algebra as unramified over a localization of a polynomial PID, so its maximal ideal is principal and the local ring is a DVR.
The main result is the IsDedekindDomain W.CoordinateRing instance.
noncomputable def
WeierstrassCurve.Affine.xPolynomial
{k : Type u_1}
[Field k]
(W : Affine k)
:
Polynomial (Polynomial k)
The Weierstrass equation viewed as a monic cubic in the X-coordinate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
WeierstrassCurve.Affine.xAdjoinRootEquiv
{k : Type u_1}
[Field k]
(W : Affine k)
:
Swapping the two polynomial variables identifies the monic X-presentation with the
affine coordinate ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
WeierstrassCurve.Affine.xAdjoinRootEquiv_mk
{k : Type u_1}
[Field k]
(W : Affine k)
(q : Polynomial (Polynomial k))
:
W.xAdjoinRootEquiv ((AdjoinRoot.mk W.xPolynomial) q) = (CoordinateRing.mk W) (Polynomial.Bivariate.swap q)
theorem
WeierstrassCurve.Affine.coordinate_mk_eq_eval₂
{k : Type u_1}
[Field k]
(W : Affine k)
(q : Polynomial (Polynomial k))
:
(CoordinateRing.mk W) q = Polynomial.eval₂
(Polynomial.eval₂RingHom (algebraMap k W.CoordinateRing) ((CoordinateRing.mk W) (Polynomial.C Polynomial.X)))
((CoordinateRing.mk W) Polynomial.X) q
theorem
WeierstrassCurve.Affine.coordinate_polynomialX_eval
{k : Type u_1}
[Field k]
(W : Affine k)
:
theorem
WeierstrassCurve.Affine.coordinate_polynomialY_eval
{k : Type u_1}
[Field k]
(W : Affine k)
:
theorem
WeierstrassCurve.Affine.coordinate_equation
{k : Type u_1}
[Field k]
(W : Affine k)
:
(W.baseChange W.CoordinateRing).Equation ((CoordinateRing.mk W) (Polynomial.C Polynomial.X))
((CoordinateRing.mk W) Polynomial.X)
theorem
WeierstrassCurve.Affine.xAdjoinRootEquiv_neg_swap_polynomialX
{k : Type u_1}
[Field k]
(W : Affine k)
:
theorem
WeierstrassCurve.Affine.coordinate_derivatives_not_both_mem
{k : Type u_1}
[Field k]
(W : Affine k)
[WeierstrassCurve.IsElliptic W]
(P : Ideal W.CoordinateRing)
[P.IsPrime]
:
theorem
AdjoinRoot.isUnramifiedAt_of_monic_derivative_not_mem
{R : Type u_1}
[CommRing R]
(f : Polynomial R)
(hf : f.Monic)
(P : Ideal (AdjoinRoot f))
[P.IsPrime]
(hP : (mk f) (Polynomial.derivative f) ∉ P)
:
theorem
AdjoinRoot.isDiscreteValuationRing_atPrime_of_derivative_not_mem
{R : Type u_1}
[CommRing R]
[IsNoetherianRing R]
[IsPrincipalIdealRing R]
(f : Polynomial R)
(hf : f.Monic)
[IsDomain (AdjoinRoot f)]
(P : Ideal (AdjoinRoot f))
[P.IsPrime]
(hP0 : P ≠ ⊥)
(hP : (mk f) (Polynomial.derivative f) ∉ P)
:
theorem
AdjoinRoot.isDiscreteValuationRing_atPrime_of_derivative_eq_not_mem
{R : Type u_1}
[CommRing R]
[IsNoetherianRing R]
[IsPrincipalIdealRing R]
(f : Polynomial R)
(hf : f.Monic)
[IsDomain (AdjoinRoot f)]
(q : Polynomial R)
(hder : Polynomial.derivative f = q)
(P : Ideal (AdjoinRoot f))
[P.IsPrime]
(hP0 : P ≠ ⊥)
(hP : (mk f) q ∉ P)
:
theorem
IsDiscreteValuationRing.of_ringEquiv_of_not_isField
{A : Type u_1}
{B : Type u_2}
[CommRing A]
[CommRing B]
[IsDomain A]
[IsDomain B]
[IsDiscreteValuationRing A]
[IsLocalRing B]
(e : A ≃+* B)
(hB : ¬IsField B)
:
theorem
IsDiscreteValuationRing.atPrime_of_comap_ringEquiv
{A : Type u_1}
{B : Type u_2}
[CommRing A]
[CommRing B]
[IsDomain A]
[IsDomain B]
(e : A ≃+* B)
(P : Ideal B)
[P.IsPrime]
(hP0 : P ≠ ⊥)
[IsDiscreteValuationRing (Localization.AtPrime (Ideal.comap e.toRingHom P))]
:
theorem
WeierstrassCurve.Affine.CoordinateRing.isDiscreteValuationRing_atPrime_of_polynomialY_not_mem
{k : Type u_1}
[Field k]
(W : Affine k)
(P : Ideal W.CoordinateRing)
[P.IsPrime]
(hP0 : P ≠ ⊥)
(hY : (mk W) W.polynomialY ∉ P)
:
theorem
WeierstrassCurve.Affine.CoordinateRing.x_comap_ne_bot
{k : Type u_1}
[Field k]
(W : Affine k)
(P : Ideal W.CoordinateRing)
(hP0 : P ≠ ⊥)
:
theorem
WeierstrassCurve.Affine.CoordinateRing.isDiscreteValuationRing_atPrime_x_comap
{k : Type u_1}
[Field k]
(W : Affine k)
(P : Ideal W.CoordinateRing)
[P.IsPrime]
(hP0 : P ≠ ⊥)
(hX : (mk W) W.polynomialX ∉ P)
:
theorem
WeierstrassCurve.Affine.CoordinateRing.isDiscreteValuationRing_atPrime_of_polynomialX_not_mem
{k : Type u_1}
[Field k]
(W : Affine k)
(P : Ideal W.CoordinateRing)
[P.IsPrime]
(hP0 : P ≠ ⊥)
(hX : (mk W) W.polynomialX ∉ P)
:
theorem
WeierstrassCurve.Affine.CoordinateRing.isDedekindDomain
{k : Type u_1}
[Field k]
(W : Affine k)
[WeierstrassCurve.IsElliptic W]
:
instance
WeierstrassCurve.Affine.CoordinateRing.instIsDedekindDomainCoordinateRing
{k : Type u_1}
[Field k]
(W : Affine k)
[WeierstrassCurve.IsElliptic W]
: