Degree-one places are rational Weierstrass points

Unlike the all-place dichotomy over an algebraically closed field, this direction only uses that the residue field has dimension one over the base field.

theorem WeierstrassCurve.Affine.Chart.instCoordinateConstantsTowerPic {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 k K] [IsScalarTower k (Polynomial k) K] : IsScalarTower k W.CoordinateRing K

theorem WeierstrassCurve.Affine.Chart.maximal_eq_XYIdeal_of_finrank_one {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (I : Ideal W.CoordinateRing) [I.IsMaximal] (hfin : Module.finrank k (W.CoordinateRing ⧸ I) = 1) : ∃ (x : k) (y : k) (_ : W.Nonsingular x y), I = CoordinateRing.XYIdeal W x (Polynomial.C y)

theorem WeierstrassCurve.Affine.Chart.exists_point_of_place_degree_one {k : Type u_1} [Field k] (W : Affine k) [WeierstrassCurve.IsElliptic W] (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 : FunctionField.Chart.PlaceA k K) (hv : FunctionField.Chart.placeDegree k K v = 1) : ∃ (P : W.Point), v = placeOfPoint W K P