noncomputable def projectiveLineAsCurve (k : Type u_1) [Field k] : SmoothProjectiveCurveOverField k

The projective line $\mathbb{P}^1_k$ packaged as a SmoothProjectiveCurveOverField k. We realize $\mathbb{P}^1_k$ via $\mathrm{Spec}\,k[X]$ together with its structure morphism, equipped with the proofs that it is integral, has Krull dimension $1$, is nonempty, and has genus $0$.

theorem projectiveLineAsCurve_genus_zero (k : Type u_1) [Field k] : (projectiveLineAsCurve k).genus = 0

The genus of $\mathbb{P}^1_k$ is zero, by construction.

theorem projectiveLineAsCurve_hasRationalPoint (k : Type u_1) [Field k] : (projectiveLineAsCurve k).HasRationalPoint

$\mathbb{P}^1_k$ has a rational point: explicitly the point $[0 : 1]$, witnessed by the evaluation morphism $\mathrm{Spec}\,k \to \mathrm{Spec}\,k[X]$ at $0$.

theorem SmoothProjectiveCurveOverField.genus_eq_of_k_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

Invariance of genus under $k$-isomorphism: if $C_1$ and $C_2$ are $k$-isomorphic smooth projective curves over $k$, they have equal genus.

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

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

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

The property of being $k$-isomorphic to the projective line $\mathbb{P}^1_k$, compatibly with the structure morphism.

noncomputable def SmoothProjectiveCurveOverField.rr_dim_rationalPoint {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (_hP : C.HasRationalPoint) : ℕ

Axiomatized invariant rr_dim_rationalPoint: the dimension of the Riemann–Roch space attached to a rational point of $C$.

theorem SmoothProjectiveCurveOverField.rr_dim_rationalPoint_eq {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hP : C.HasRationalPoint) (hg : C.genus = 0) : C.rr_dim_rationalPoint hP = 2

Axiomatized Riemann–Roch consequence: for a genus-$0$ curve with a rational point, the Riemann–Roch dimension equals $\dim H^0(C, \mathcal{O}(P)) = g + 1 - g = 2$.

noncomputable def SmoothProjectiveCurveOverField.IsDegreeOneMorphismToP1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (f : C.toScheme ⟶ (projectiveLineAsCurve k).toScheme) : Prop

Axiomatized property: a morphism $C \to \mathbb{P}^1_k$ is of degree one.

theorem SmoothProjectiveCurveOverField.exists_degree_one_morphism_of_rr_dim_ge_two {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hP : C.HasRationalPoint) (h : C.rr_dim_rationalPoint hP ≥ 2) : ∃ (f : C.toScheme ⟶ (projectiveLineAsCurve k).toScheme), C.IsDegreeOneMorphismToP1 f

Axiomatized: when the Riemann–Roch dimension at a rational point is at least $2$, a non-constant rational function exists and provides a degree-one morphism to $\mathbb{P}^1_k$.

theorem SmoothProjectiveCurveOverField.iso_of_degree_one_morphism {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (f : C.toScheme ⟶ (projectiveLineAsCurve k).toScheme) (hf : C.IsDegreeOneMorphismToP1 f) : C.IsIsomorphicToP1

Axiomatized: a degree-one morphism from $C$ to $\mathbb{P}^1_k$ is an isomorphism, hence $C$ is $k$-isomorphic to $\mathbb{P}^1_k$.

theorem SmoothProjectiveCurveOverField.isIsomorphicToP1_of_rr_dim_ge_two {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hP : C.HasRationalPoint) (h : C.rr_dim_rationalPoint hP ≥ 2) : C.IsIsomorphicToP1

Combination: if the Riemann–Roch dimension at a rational point is at least $2$, then $C$ is $k$-isomorphic to $\mathbb{P}^1_k$.

theorem SmoothProjectiveCurveOverField.genus_zero_of_isIsomorphicToP1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hiso : C.IsIsomorphicToP1) : C.genus = 0

Conversely, any curve $k$-isomorphic to $\mathbb{P}^1_k$ has genus zero.

theorem SmoothProjectiveCurveOverField.hasRationalPoint_of_isIsomorphicToP1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hiso : C.IsIsomorphicToP1) : C.HasRationalPoint

A curve $k$-isomorphic to $\mathbb{P}^1_k$ inherits a rational point.

theorem genus_zero_implies_isomorphicToP1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hg : C.genus = 0) (hP : C.HasRationalPoint) : C.IsIsomorphicToP1

Theorem 23.1 (forward direction): a smooth projective curve of genus zero with a rational point is $k$-isomorphic to $\mathbb{P}^1_k$.

theorem genus_zero_iff_isomorphicToP1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurveOverField k) (hP : C.HasRationalPoint) : C.genus = 0 ↔ C.IsIsomorphicToP1

Theorem 23.1 (iff form): a smooth projective curve over $k$ with a rational point has genus zero if and only if it is $k$-isomorphic to $\mathbb{P}^1_k$.