structure SmoothProjectiveCurveOverField (k : Type u_1) [Field k] : Type (u_1 + 1)

A smooth projective curve over a field $k$ packaged as: an underlying scheme (with proofs of integrality, Krull dimension one, nonemptiness), a structure morphism to $\mathrm{Spec}\,k$, and a (declared) genus value. The smoothness is left implicit.

• toScheme : AlgebraicGeometry.Scheme
• isIntegral : AlgebraicGeometry.IsIntegral self.toScheme
• krullDim_eq : topologicalKrullDim ↥self.toScheme = 1
• nonempty : Nonempty ↥self.toScheme
• structureMorphism : self.toScheme ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)
• genusVal : ℕ

def SmoothProjectiveCurveOverField.genus {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) : ℕ

The genus of a smooth projective curve, given by the structural field genusVal.

def SmoothProjectiveCurveOverField.HasRationalPoint {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) : Prop

A smooth projective curve has a rational point if its structure morphism admits a section, i.e. a morphism $\mathrm{Spec}\,k \to C$ that composes to the identity.

structure PlaneCubic (k : Type u_1) [Field k] : Type u_1

A plane cubic over $k$: a nonzero homogeneous polynomial of degree $3$ in three variables.

• poly : MvPolynomial (Fin 3) k
• isHomogeneous : self.poly.IsHomogeneous 3
• ne_zero : self.poly ≠ 0

def PlaneCubic.HasRationalPoint {k : Type u_1} [Field k] (F : PlaneCubic k) : Prop

A plane cubic has a rational point if there is a nonzero $k$-tuple $p \in k^3$ with $F(p) = 0$.

noncomputable def PlaneCubic.toScheme_ax {k : Type u_1} [Field k] (C : PlaneCubic k) : AlgebraicGeometry.Scheme

Axiomatized: the scheme attached to a plane cubic, namely $\mathrm{Proj}$ of $k[X, Y, Z] / (F)$.

noncomputable def PlaneCubic.toStructureMorphism_ax {k : Type u_1} [Field k] (C : PlaneCubic k) : C.toScheme_ax ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)

Axiomatized: the structure morphism of the scheme attached to a plane cubic.

noncomputable def PlaneCubic.toScheme {k : Type u_1} [Field k] (F : PlaneCubic k) : AlgebraicGeometry.Scheme

The scheme associated to a plane cubic, wrapping toScheme_ax.

noncomputable def PlaneCubic.toSchemeStructureMorphism {k : Type u_1} [Field k] (F : PlaneCubic k) : F.toScheme ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)

The structure morphism of PlaneCubic.toScheme, wrapping toStructureMorphism_ax.

theorem PlaneCubic.hasRationalPoint_iff_section {k : Type u_1} [Field k] (F : PlaneCubic k) : F.HasRationalPoint ↔ ∃ (s : AlgebraicGeometry.Spec (CommRingCat.of k) ⟶ F.toScheme), CategoryTheory.CategoryStruct.comp s F.toSchemeStructureMorphism = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (CommRingCat.of k))

Axiomatized: a plane cubic has a rational point in the polynomial sense if and only if its scheme admits a $k$-section.

def PlaneCubic.genus {k : Type u_1} [Field k] (_F : PlaneCubic k) : ℕ

The (declared) genus of a plane cubic, set to be $1$ in agreement with the genus formula for a smooth plane curve of degree $3$.

theorem PlaneCubic.toScheme_isIntegral {k : Type u_1} [Field k] (F : PlaneCubic k) : AlgebraicGeometry.IsIntegral F.toScheme

Axiomatized: the scheme of a plane cubic is integral.

theorem PlaneCubic.toScheme_krullDim {k : Type u_1} [Field k] (F : PlaneCubic k) : topologicalKrullDim ↥F.toScheme = 1

Axiomatized: the scheme of a plane cubic has Krull dimension one.

theorem PlaneCubic.toScheme_nonempty {k : Type u_1} [Field k] (F : PlaneCubic k) : Nonempty ↥F.toScheme

Axiomatized: the scheme of a plane cubic is nonempty.

noncomputable def PlaneCubic.toSmoothProjectiveCurveOverField {k : Type u_1} [Field k] (F : PlaneCubic k) : SmoothProjectiveCurveOverField k

Bundling a plane cubic into a SmoothProjectiveCurveOverField, combining the integrality, Krull-dimension, nonemptiness, structure-morphism, and genus data.

theorem PlaneCubic.toSmoothProjectiveCurveOverField_genus {k : Type u_1} [Field k] (F : PlaneCubic k) : F.toSmoothProjectiveCurveOverField.genus = F.genus

Compatibility: the genus of the bundled curve equals the genus of the plane cubic.

theorem genus_eq_of_scheme_iso {k : Type u_1} [Field k] (C₁ C₂ : SmoothProjectiveCurveOverField k) (φ : C₁.toScheme ≅ C₂.toScheme) (hφ : CategoryTheory.CategoryStruct.comp φ.hom C₂.structureMorphism = C₁.structureMorphism) : C₁.genus = C₂.genus

Axiomatized: the genus is invariant under $k$-isomorphism of schemes that are compatible with the structure morphisms.

def SmoothProjectiveCurveOverField.IsIsomorphicTo {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (F : PlaneCubic k) : Prop

The property that the smooth projective curve $C$ is $k$-isomorphic to (the scheme attached to) a plane cubic $F$, compatibly with the structure morphisms to $\mathrm{Spec}\,k$.

theorem SmoothProjectiveCurveOverField.hasRationalPoint_of_isIsomorphicTo {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (F : PlaneCubic k) (hiso : C.IsIsomorphicTo F) (hpt : F.HasRationalPoint) : C.HasRationalPoint

Transport of rational points along a $k$-isomorphism: if $F$ has a rational point and $C \simeq F$ over $k$, then $C$ has a rational point.

theorem SmoothProjectiveCurveOverField.hasRationalPoint_iff_of_isIsomorphicTo {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (F : PlaneCubic k) (hiso : C.IsIsomorphicTo F) : C.HasRationalPoint ↔ F.HasRationalPoint

Two-way invariance: under a $k$-isomorphism $C \simeq F$, the existence of a rational point is preserved in both directions.

theorem SmoothProjectiveCurveOverField.genus_eq_of_isIsomorphicTo {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (F : PlaneCubic k) (hiso : C.IsIsomorphicTo F) : C.genus = F.genus

The genus of $C$ equals the genus of $F$ whenever $C$ is $k$-isomorphic to the plane cubic $F$.

noncomputable def WeierstrassCurve.toPlaneCubic {k : Type u_1} [Field k] (W : WeierstrassCurve k) : PlaneCubic k

The plane cubic given by the (general) Weierstrass equation $Y^2Z + a_1 XYZ + a_3 YZ^2 = X^3 + a_2 X^2 Z + a_4 XZ^2 + a_6 Z^3$, encoded as a homogeneous polynomial of degree $3$ in three variables.

theorem WeierstrassCurve.toPlaneCubic_hasRationalPoint {k : Type u_1} [Field k] (W : WeierstrassCurve k) : W.toPlaneCubic.HasRationalPoint

The point at infinity $[0 : 1 : 0]$ provides a rational point on the Weierstrass plane cubic.

theorem WeierstrassCurve.toPlaneCubic_genus {k : Type u_1} [Field k] (W : WeierstrassCurve k) (_hW : W.IsElliptic) : W.toPlaneCubic.genus = 1

The genus of an elliptic Weierstrass curve, viewed as a plane cubic, is one.

theorem weierstrass_model_of_genus_one {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hg : C.genus = 1) (hP : C.HasRationalPoint) : ∃ (W : WeierstrassCurve k), W.IsElliptic ∧ C.IsIsomorphicTo W.toPlaneCubic

Axiomatized: a smooth projective curve of genus one with a rational point is $k$-isomorphic to the plane cubic of some elliptic Weierstrass curve.

theorem genus_one_of_weierstrass_model {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (W : WeierstrassCurve k) (hW : W.IsElliptic) (hiso : C.IsIsomorphicTo W.toPlaneCubic) : C.genus = 1 ∧ C.HasRationalPoint

Converse to weierstrass_model_of_genus_one: a curve $k$-isomorphic to an elliptic Weierstrass plane cubic has genus one and a rational point.

theorem weierstrass_model_iff_genus_one {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hP : C.HasRationalPoint) : C.genus = 1 ↔ ∃ (W : WeierstrassCurve k), W.IsElliptic ∧ C.IsIsomorphicTo W.toPlaneCubic

Iff form: assuming a rational point, $C$ has genus one if and only if $C$ admits a Weierstrass elliptic model.

theorem genus_one_isomorphic_to_plane_cubic {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hg : C.genus = 1) (hP : C.HasRationalPoint) : ∃ (W : WeierstrassCurve k), W.IsElliptic ∧ W.toPlaneCubic.HasRationalPoint ∧ C.IsIsomorphicTo W.toPlaneCubic

Strengthened statement: a smooth projective curve of genus one with a rational point is $k$-isomorphic to an elliptic Weierstrass plane cubic that, in turn, has a rational point.