structure ArithmeticGeometry.SmoothProjectiveCurve (k : Type u_1) [Field k] : Type (max (max (max (max u_1 (u_2 + 1)) (u_3 + 1)) (u_4 + 1)) (u_5 + 1))

An axiomatic structure for a smooth projective curve $C/k$: it bundles the function field, divisor group, degree-zero Picard group $\operatorname{Pic}^0(C)$, set of rational points, principal divisor map, class map, genus, and the basic compatibilities between them.

• FunField : Type u_2
• fieldInst : Field self.FunField
• algebraInst : Algebra k self.FunField
• DivGroup : Type u_3
• divGroupInst : AddCommGroup self.DivGroup
• Pic0 : Type u_4
• pic0Inst : AddCommGroup self.Pic0
• RatPoint : Type u_5
• pointToDivisor : self.RatPoint → self.DivGroup
• degreeMap : self.DivGroup →+ ℤ
• degree_point (P : self.RatPoint) : self.degreeMap (self.pointToDivisor P) = 1
• principalDiv : self.FunField → self.DivGroup
• degree_principalDiv (f : self.FunField) : self.degreeMap (self.principalDiv f) = 0
• classMap : self.DivGroup →+ self.Pic0
• principalDiv_in_kernel (f : self.FunField) : f ≠ 0 → self.classMap (self.principalDiv f) = 0
• classMap_surj (x : self.Pic0) : ∃ (D : self.DivGroup), self.degreeMap D = 0 ∧ self.classMap D = x
• classMap_eq_zero_iff (D : self.DivGroup) : self.degreeMap D = 0 → (self.classMap D = 0 ↔ ∃ (f : self.FunField), f ≠ 0 ∧ self.principalDiv f = D)
• pointToDivisor_injective : Function.Injective self.pointToDivisor
• principalDiv_algebraMap (a : k) : self.principalDiv ((algebraMap k self.FunField) a) = 0
• isAlgebraic_implies_mem_range_algebraMap (f : self.FunField) : IsAlgebraic k f → f ∈ Set.range ⇑(algebraMap k self.FunField)
• genusVal : ℕ
• exists_two_ratPoints_of_algClosed : IsAlgClosed k → ∃ (P : self.RatPoint) (Q : self.RatPoint), P ≠ Q
• principalDiv_mul (f g : self.FunField) : f ≠ 0 → g ≠ 0 → self.principalDiv (f * g) = self.principalDiv f + self.principalDiv g

theorem ArithmeticGeometry.degree_formula_axiom {k : Type u_2} [Field k] (C : SmoothProjectiveCurve k) (f : C.FunField) (P Q : C.RatPoint) (hPQ : P ≠ Q) (hdiv : C.principalDiv f = C.pointToDivisor P + -C.pointToDivisor Q) (φ : RatFunc k →ₐ[k] C.FunField) (hφ : Function.Injective ⇑φ) : Module.finrank (↥φ.fieldRange) C.FunField = 1

Axiom (degree formula): if $f \in k(C)$ has principal divisor $(P) - (Q)$ with $P \neq Q$, then for any injective $k$-algebra homomorphism $\varphi: k(t) \hookrightarrow k(C)$, the extension $k(C)/\varphi(k(t))$ has degree $1$.

theorem ArithmeticGeometry.deg_zero_div_principal_of_iso_ratFunc {k : Type u_2} [Field k] (C : SmoothProjectiveCurve k) (φ : C.FunField ≃ₐ[k] RatFunc k) (D : C.DivGroup) (hdeg : C.degreeMap D = 0) : ∃ (f : C.FunField), f ≠ 0 ∧ C.principalDiv f = D

If $k(C) \cong k(t)$ as $k$-algebras, then every degree-zero divisor on $C$ is principal.

theorem ArithmeticGeometry.SmoothProjectiveCurve.exists_two_ratPoints {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) [IsAlgClosed k] : ∃ (P : C.RatPoint) (Q : C.RatPoint), P ≠ Q

Over an algebraically closed field, a smooth projective curve has at least two distinct rational points.

theorem ArithmeticGeometry.SmoothProjectiveCurve.transcendental_of_principalDiv_ne_zero {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (f : C.FunField) (hf : C.principalDiv f ≠ 0) : Transcendental k f

If $f \in k(C)$ has a nonzero principal divisor, then $f$ is transcendental over $k$ (an algebraic element would lie in $k \subseteq k(C)$ and have trivial divisor).

theorem ArithmeticGeometry.finrank_eq_one_of_subfield_eq_top {F : Type u_2} [Field F] (K : Subfield F) (h : K = ⊤) : Module.finrank (↥K) F = 1

Helper lemma: if a subfield $K \subseteq F$ equals all of $F$, then $F$ has dimension $1$ as a $K$-vector space.

theorem ArithmeticGeometry.SmoothProjectiveCurve.pullback_surjective {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) {f : C.FunField} (_hf : f ≠ 0) {P Q : C.RatPoint} (hPQ : P ≠ Q) (hdiv : C.principalDiv f = C.pointToDivisor P + -C.pointToDivisor Q) (φ : RatFunc k →ₐ[k] C.FunField) (hφ : Function.Injective ⇑φ) : Function.Surjective ⇑φ

If there is a function $f \in k(C)$ with divisor $(P) - (Q)$ for distinct rational points $P, Q$, then any injective $k$-algebra map $\varphi: k(t) \to k(C)$ is automatically surjective.

theorem ArithmeticGeometry.SmoothProjectiveCurve.fieldExtension_degree_one {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) {f : C.FunField} (hf : f ≠ 0) {P Q : C.RatPoint} (hPQ : P ≠ Q) (hdiv : C.principalDiv f = C.pointToDivisor P + -C.pointToDivisor Q) (φ : RatFunc k →ₐ[k] C.FunField) (hφ : Function.Injective ⇑φ) : Module.finrank (↥φ.fieldRange) C.FunField = 1

The field extension $k(C)/\varphi(k(t))$ has degree one whenever there is a function with divisor $(P) - (Q)$ and $\varphi: k(t) \hookrightarrow k(C)$ is injective.

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

A smooth projective curve $C/k$ is isomorphic to $\mathbb{P}^1_k$ iff its function field $k(C)$ is $k$-algebra isomorphic to the rational function field $k(t)$.

def ArithmeticGeometry.SmoothProjectiveCurve.Pic0IsTrivial {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) : Prop

The Picard group $\operatorname{Pic}^0(C)$ is trivial iff every degree-zero divisor class is the identity.

theorem ArithmeticGeometry.Pic0_injective_to_classGroup_of_iso {k : Type u_2} [Field k] (C : SmoothProjectiveCurve k) (φ : C.FunField ≃ₐ[k] RatFunc k) : ∃ (ι : C.Pic0 →+ Additive (ClassGroup (Polynomial k))), Function.Injective ⇑ι

If $k(C) \cong k(t)$, then $\operatorname{Pic}^0(C)$ embeds (injectively) into the class group of $k[t]$. Used as a stepping stone to show $\operatorname{Pic}^0(C)$ is trivial.

theorem ArithmeticGeometry.Pic0_trivial_of_funField_iso_ratFunc {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (φ : C.FunField ≃ₐ[k] RatFunc k) : C.Pic0IsTrivial

If $k(C) \cong k(t)$ as $k$-algebras, then $\operatorname{Pic}^0(C)$ is trivial.

theorem ArithmeticGeometry.every_deg0_div_principal_of_iso_P1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (φ : C.FunField ≃ₐ[k] RatFunc k) (D : C.DivGroup) (hdeg : C.degreeMap D = 0) : ∃ (f : C.FunField), f ≠ 0 ∧ C.principalDiv f = D

If $k(C) \cong k(t)$, then every degree-zero divisor $D$ on $C$ is principal: $D = \operatorname{div}(f)$ for some nonzero $f \in k(C)$.

theorem ArithmeticGeometry.Pic0_injective_to_classGroup_axiom {k : Type u_2} [Field k] (C : SmoothProjectiveCurve k) (φ : C.FunField ≃ₐ[k] RatFunc k) : ∃ (ι : C.Pic0 →+ Additive (ClassGroup (Polynomial k))), Function.Injective ⇑ι

Re-export of Pic0_injective_to_classGroup_of_iso: an injective additive map $\operatorname{Pic}^0(C) \hookrightarrow \operatorname{Cl}(k[t])$ exists whenever $k(C) \cong k(t)$.

theorem ArithmeticGeometry.principalDiv_of_iso_P1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (hiso : C.IsIsomorphicToP1) (D : C.DivGroup) (hdeg : C.degreeMap D = 0) : ∃ (f : C.FunField), f ≠ 0 ∧ C.principalDiv f = D

If $C \cong \mathbb{P}^1_k$, then every degree-zero divisor on $C$ is principal.

theorem ArithmeticGeometry.classMap_zero_of_iso_P1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (hiso : C.IsIsomorphicToP1) (D : C.DivGroup) (hdeg : C.degreeMap D = 0) : C.classMap D = 0

If $C \cong \mathbb{P}^1_k$, then the divisor-class image of any degree-zero divisor $D$ vanishes in $\operatorname{Pic}^0(C)$.

theorem ArithmeticGeometry.degree_zero_divisor_principal_of_iso_P1 {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (hiso : C.IsIsomorphicToP1) (D : C.DivGroup) (hdeg : C.degreeMap D = 0) : ∃ (f : C.FunField), f ≠ 0 ∧ C.principalDiv f = D

Same statement as principalDiv_of_iso_P1, packaged as a lemma: every degree-zero divisor on $C \cong \mathbb{P}^1$ is principal.

theorem ArithmeticGeometry.P1_Pic0_trivial {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (hiso : C.IsIsomorphicToP1) : C.Pic0IsTrivial

If $C \cong \mathbb{P}^1_k$ then $\operatorname{Pic}^0(C) = 0$.

noncomputable def ArithmeticGeometry.SmoothProjectiveCurve.pic0_to_classGroup {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (φ : C.FunField ≃ₐ[k] RatFunc k) : { f : C.Pic0 →+ Additive (ClassGroup (Polynomial k)) // Function.Injective ⇑f }

Bundles the injective embedding $\operatorname{Pic}^0(C) \hookrightarrow \operatorname{Cl}(k[t])$ provided by an isomorphism $k(C) \cong k(t)$. Since the target is trivial, this concretely produces the zero map.

theorem ArithmeticGeometry.exists_distinct_rational_points {k : Type u_1} [Field k] [IsAlgClosed k] (C : SmoothProjectiveCurve k) : ∃ (P : C.RatPoint) (Q : C.RatPoint), P ≠ Q

Over an algebraically closed field, a smooth projective curve has two distinct rational points.

theorem ArithmeticGeometry.exists_injective_algHom_of_nontrivial_div {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) {P Q : C.RatPoint} (hPQ : P ≠ Q) {f : C.FunField} (_hf : f ≠ 0) (hdiv : C.principalDiv f = C.pointToDivisor P + -C.pointToDivisor Q) : ∃ (φ : RatFunc k →ₐ[k] C.FunField), Function.Injective ⇑φ

If $f \in k(C)$ has divisor $(P) - (Q)$ with $P \neq Q$, then $f$ is transcendental and induces an injective $k$-algebra homomorphism $k(t) \hookrightarrow k(C)$ by $t \mapsto f$.

theorem ArithmeticGeometry.morphism_surjective_of_deg_one_div {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) {P Q : C.RatPoint} (hPQ : P ≠ Q) {f : C.FunField} (hf : f ≠ 0) (hdiv : C.principalDiv f = C.pointToDivisor P + -C.pointToDivisor Q) (φ : RatFunc k →ₐ[k] C.FunField) (hφ_inj : Function.Injective ⇑φ) : Function.Surjective ⇑φ

Any injective $\varphi: k(t) \to k(C)$ is automatically surjective if there is a function on $C$ with divisor $(P) - (Q)$: the field extension $k(C)/\varphi(k(t))$ has degree one.

theorem ArithmeticGeometry.iso_of_bijective_algHom {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (φ : RatFunc k →ₐ[k] C.FunField) (hφ : Function.Bijective ⇑φ) : C.IsIsomorphicToP1

A bijective $k$-algebra homomorphism $k(t) \to k(C)$ gives the isomorphism $C \cong \mathbb{P}^1_k$.

theorem ArithmeticGeometry.degree_one_morphism_is_iso {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) {P Q : C.RatPoint} (hPQ : P ≠ Q) {f : C.FunField} (hf : f ≠ 0) (hdiv : C.principalDiv f = C.pointToDivisor P + -C.pointToDivisor Q) : C.IsIsomorphicToP1

If $C$ admits a function with divisor $(P) - (Q)$ for distinct rational points, then $C \cong \mathbb{P}^1_k$.

theorem ArithmeticGeometry.principal_of_Pic0_trivial {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (htriv : C.Pic0IsTrivial) (P Q : C.RatPoint) : ∃ (f : C.FunField), f ≠ 0 ∧ C.principalDiv f = C.pointToDivisor P + -C.pointToDivisor Q

If $\operatorname{Pic}^0(C) = 0$, then for any two rational points $P, Q$, the degree-zero divisor $(P) - (Q)$ is principal: there is a function $f \in k(C)$ with $\operatorname{div}(f) = (P) - (Q)$.

theorem ArithmeticGeometry.Pic0_trivial_imp_iso_P1 {k : Type u_1} [Field k] [IsAlgClosed k] (C : SmoothProjectiveCurve k) (htriv : C.Pic0IsTrivial) : C.IsIsomorphicToP1

Over an algebraically closed field, if $\operatorname{Pic}^0(C) = 0$ then $C \cong \mathbb{P}^1_k$.

theorem ArithmeticGeometry.iso_P1_iff_Pic0_trivial {k : Type u_1} [Field k] [IsAlgClosed k] (C : SmoothProjectiveCurve k) : C.IsIsomorphicToP1 ↔ C.Pic0IsTrivial

Main result: over an algebraically closed field, a smooth projective curve $C$ is isomorphic to $\mathbb{P}^1_k$ iff $\operatorname{Pic}^0(C)$ is trivial.