@[reducible, inline]

abbrev CurveDiv (P : Type u_2) : Type u_2

The group of divisors on a curve (with point type P): the free abelian group on P, modeled as P →₀ ℤ. Cf. Definition 23.13 (Sutherland §23.2): a divisor is a finite formal sum D = ∑_P n_P [P] of points with integer coefficients.

noncomputable def CurveDiv.of {P : Type u_1} (p : P) : CurveDiv P

The divisor [p] consisting of a single point with multiplicity 1.

def CurveDiv.coeff {P : Type u_1} (D : CurveDiv P) (p : P) : ℤ

The coefficient (valuation) of D at p: this is v_P(D) in the notation of Definition 23.13.

@[simp]

theorem CurveDiv.coeff_of_same {P : Type u_1} [DecidableEq P] (p : P) : (of p).coeff p = 1

The coefficient of [p] at p is 1.

@[simp]

theorem CurveDiv.coeff_of_ne {P : Type u_1} [DecidableEq P] {p q : P} (h : p ≠ q) : (of p).coeff q = 0

The coefficient of [p] at a different point q is 0.

def CurveDiv.supp {P : Type u_1} (D : CurveDiv P) : Finset P

The support of a divisor D: the finite set of points where its coefficient is nonzero. Cf. Definition 23.13.

@[simp]

theorem CurveDiv.mem_supp_iff {P : Type u_1} (D : CurveDiv P) (p : P) : p ∈ D.supp ↔ D.coeff p ≠ 0

Characterization of the support: p ∈ supp D iff its coefficient is nonzero.

def CurveDiv.deg {P : Type u_1} (D : CurveDiv P) : ℤ

The degree of a divisor: deg D := ∑_P v_P(D) (Definition 23.13).

@[simp]

theorem CurveDiv.deg_zero {P : Type u_1} : deg 0 = 0

The degree of the zero divisor is zero.

@[simp]

theorem CurveDiv.deg_single {P : Type u_1} [DecidableEq P] (p : P) (n : ℤ) : deg (Finsupp.single p n) = n

The degree of a single-point divisor n[p] is n.

@[simp]

theorem CurveDiv.deg_of {P : Type u_1} [DecidableEq P] (p : P) : (of p).deg = 1

The degree of the divisor [p] is 1.

theorem CurveDiv.deg_add {P : Type u_1} (D₁ D₂ : CurveDiv P) : (D₁ + D₂).deg = D₁.deg + D₂.deg

Additivity of the degree: deg(D₁ + D₂) = deg D₁ + deg D₂.

def CurveDiv.degHom (P : Type u_2) : CurveDiv P →+ ℤ

The degree map Div C → ℤ packaged as an additive group homomorphism.

noncomputable def CurveDiv.DivZero (P : Type u_2) : AddSubgroup (CurveDiv P)

The subgroup Div⁰ C of divisors of degree zero, defined as the kernel of the degree map. (Cf. Definition 23.13.)

theorem CurveDiv.mem_divZero_iff {P : Type u_1} (D : CurveDiv P) : D ∈ DivZero P ↔ D.deg = 0

Membership in DivZero P is equivalent to having degree zero.

structure CurveDiv.FunctionFieldDiv (P : Type u_2) : Type (max u_2 (u_3 + 1))

A "function-field-with-divisor-map" structure: a multiplicative group F (intended to be the function field k(C)^×), a subgroup kUnits of constants k^×, and a group homomorphism divMap : (F, ·) → (Div C, +) sending each nonzero function to its principal divisor div f.

• F : Type u_3
• instCommGroup : CommGroup self.F
• kUnits : Subgroup self.F
• divMap : Additive self.F →+ CurveDiv P

theorem CurveDiv.principalDivisor_degree_zero {P : Type u_2} (Φ : FunctionFieldDiv P) (f : Additive Φ.F) : (Φ.divMap f).deg = 0

Every principal divisor has degree zero (Corollary 23.10 / Definition 23.13).

theorem CurveDiv.principalDivisor_kernel_eq_constants {P : Type u_2} (Φ : FunctionFieldDiv P) (f : Φ.F) : Φ.divMap (Additive.ofMul f) = 0 ↔ f ∈ Φ.kUnits

The kernel of the f ↦ div f map consists exactly of the nonzero constants k^× (Corollary 23.10).

noncomputable def CurveDiv.PrincDiv {P : Type u_1} (Φ : FunctionFieldDiv P) : AddSubgroup (CurveDiv P)

The subgroup Princ C ⊆ Div C of principal divisors, defined as the image of the function-field divisor map. (Definition 23.13.)

theorem CurveDiv.princDiv_le_divZero {P : Type u_1} (Φ : FunctionFieldDiv P) : PrincDiv Φ ≤ DivZero P

Principal divisors are divisors of degree zero.

noncomputable def CurveDiv.divMapToDivZero {P : Type u_1} (Φ : FunctionFieldDiv P) : Additive Φ.F →+ ↥(DivZero P)

The corestriction of the function-field divisor map to the subgroup of degree-zero divisors.

@[reducible, inline]

abbrev CurveDiv.PicardGroup {P : Type u_1} (Φ : FunctionFieldDiv P) : Type u_1

The Picard group Pic C := Div C / Princ C of divisor classes.

noncomputable def CurveDiv.degHomPic {P : Type u_1} (Φ : FunctionFieldDiv P) : CurveDiv P ⧸ PrincDiv Φ →+ ℤ

Since principal divisors have degree zero, the degree map descends to a homomorphism Pic C → ℤ from the Picard group.

@[reducible, inline]

abbrev CurveDiv.PicardGroupZero {P : Type u_1} (Φ : FunctionFieldDiv P) : Type u_1

The group Pic⁰ C := Div⁰ C / Princ C of divisor classes of degree zero (Definition 23.13).

noncomputable def CurveDiv.abelJacobiDivAt {P : Type u_2} (O p : P) : ↥(DivZero P)

The degree-zero divisor [p] - [O] for the Abel-Jacobi map with origin O (Definition 23.15).

@[simp]

theorem CurveDiv.abelJacobiDivAt_coe {P : Type u_2} (O p : P) : ↑(abelJacobiDivAt O p) = Finsupp.single p 1 - Finsupp.single O 1

Unfolding: the underlying divisor of abelJacobiDivAt O p is [p] - [O].

theorem CurveDiv.abelJacobiDivAt_self {P : Type u_2} (O : P) : abelJacobiDivAt O O = 0

abelJacobiDivAt O O = 0, since [O] - [O] = 0.

noncomputable def CurveDiv.abelJacobiMapAt {P : Type u_2} (Φ : FunctionFieldDiv P) (O p : P) : PicardGroupZero Φ

The Abel-Jacobi map P ↦ [p] - [O] modulo principal divisors, as a function P → Pic⁰ C (Definition 23.15).

def CurveDiv.pointSum {P : Type u_1} [AddCommGroup P] (D : CurveDiv P) : P

For P an abelian group, the point sum of a divisor ∑ n_P [P] is ∑ n_P · P, interpreted in the group P. For elliptic curves this is the map Div E → E induced by the group law.

def CurveDiv.pointSumHom (P : Type u_2) [AddCommGroup P] : CurveDiv P →+ P

pointSum packaged as an additive group homomorphism Div C → P.

@[simp]

theorem CurveDiv.pointSumHom_apply {P : Type u_1} [AddCommGroup P] (D : CurveDiv P) : (pointSumHom P) D = D.pointSum

Definitional unfolding: pointSumHom P D = pointSum D.

@[simp]

theorem CurveDiv.pointSum_zero {P : Type u_1} [AddCommGroup P] : pointSum 0 = 0

The point sum of the zero divisor is 0.

@[simp]

theorem CurveDiv.pointSum_single {P : Type u_1} [DecidableEq P] [AddCommGroup P] (p : P) (n : ℤ) : pointSum (Finsupp.single p n) = n • p

The point sum of a single-point divisor n[p] is n • p.

theorem CurveDiv.pointSum_sub {P : Type u_1} [AddCommGroup P] (D₁ D₂ : CurveDiv P) : (D₁ - D₂).pointSum = D₁.pointSum - D₂.pointSum

pointSum respects subtraction.

@[simp]

theorem CurveDiv.pointSum_of {P : Type u_1} [DecidableEq P] [AddCommGroup P] (p : P) : (of p).pointSum = p

The point sum of [p] is p.

theorem CurveDiv.pointSum_principal_eq_zero {P : Type u_2} [AddCommGroup P] (Φ : FunctionFieldDiv P) (f : Additive Φ.F) : (Φ.divMap f).pointSum = 0

A principal divisor sums (under the group law of P) to 0. This is one direction of the Abel-Jacobi isomorphism (Theorem 23.17) for elliptic curves.

theorem CurveDiv.abelJacobi_surj {P : Type u_2} [AddCommGroup P] (Φ : FunctionFieldDiv P) (D : CurveDiv P) (hdeg : D.deg = 0) : D - (Finsupp.single D.pointSum 1 - Finsupp.single 0 1) ∈ PrincDiv Φ

Surjectivity content of Abel-Jacobi (Theorem 23.17): every divisor D of degree zero is equivalent modulo principal divisors to [D.pointSum] - [0].

theorem CurveDiv.principal_iff_deg_zero_and_pointSum_zero {P : Type u_2} [AddCommGroup P] (Φ' : FunctionFieldDiv P) (D : CurveDiv P) : D ∈ PrincDiv Φ' ↔ D.deg = 0 ∧ D.pointSum = 0

A divisor on an elliptic curve (group P) is principal iff it has degree zero and its point-sum vanishes. This is the standard "sum-to-zero" criterion for principal divisors (cf. Theorem 23.17).

noncomputable def CurveDiv.abelJacobiDiv {P : Type u_2} [AddCommGroup P] (p : P) : ↥(DivZero P)

The Abel-Jacobi divisor with origin 0 : P: [p] - [0].

@[simp]

theorem CurveDiv.abelJacobiDiv_coe {P : Type u_2} [AddCommGroup P] (p : P) : ↑(abelJacobiDiv p) = Finsupp.single p 1 - Finsupp.single 0 1

The underlying divisor of abelJacobiDiv p is [p] - [0].

theorem CurveDiv.abelJacobiDiv_zero {P : Type u_2} [AddCommGroup P] : abelJacobiDiv 0 = 0

abelJacobiDiv 0 = 0.

noncomputable def CurveDiv.pointSumHomDivZero {P : Type u_2} [AddCommGroup P] : ↥(DivZero P) →+ P

The point-sum map restricted to degree-zero divisors, as an additive group homomorphism Div⁰ C → P.

noncomputable def CurveDiv.pointSumHomPic {P : Type u_2} [AddCommGroup P] (Φ' : FunctionFieldDiv P) : PicardGroupZero Φ' →+ P

The point-sum map descends to Pic⁰ C → P since principal divisors have zero point-sum; this is the inverse of the Abel-Jacobi isomorphism.

noncomputable def CurveDiv.abelJacobiHom {P : Type u_2} [AddCommGroup P] (Φ' : FunctionFieldDiv P) : P →+ PicardGroupZero Φ'

The Abel-Jacobi map p ↦ [[p] - [0]] as an additive group homomorphism P → Pic⁰ C (Theorem 23.17 for elliptic curves).

theorem CurveDiv.pointSumHomPic_abelJacobiHom {P : Type u_2} [AddCommGroup P] (Φ' : FunctionFieldDiv P) (p : P) : (pointSumHomPic Φ') ((abelJacobiHom Φ') p) = p

One half of the Abel-Jacobi isomorphism: composing abelJacobiHom with the inverse pointSumHomPic recovers the identity on points.

theorem CurveDiv.abelJacobiHom_pointSumHomPic {P : Type u_2} [AddCommGroup P] (Φ' : FunctionFieldDiv P) (x : PicardGroupZero Φ') : (abelJacobiHom Φ') ((pointSumHomPic Φ') x) = x

Other half of the Abel-Jacobi isomorphism: composing in the other order recovers the identity on Pic⁰ C.

noncomputable def CurveDiv.picZeroEquivEC {P : Type u_2} [AddCommGroup P] (Φ' : FunctionFieldDiv P) : P ≃+ PicardGroupZero Φ'

The Abel-Jacobi isomorphism P ≃+ Pic⁰ C for an elliptic curve, packaged as an AddEquiv (Theorem 23.17 of Sutherland).

structure SmoothProjectiveCurve : Type (max (u_2 + 1) (u_3 + 1))

A smooth projective curve, represented abstractly by a type of points Point, a function field FunctionField (a field), and a discrete-valuation map val P : FunctionField → WithTop ℤ at each point P satisfying the standard axioms of a normalized valuation: val P 0 = ⊤, val P 1 = 0, val P (fg) = val P f + val P g, val P (f+g) ≥ min (val P f) (val P g), finiteness at nonzero elements, and surjectivity onto ℤ.

• Point : Type u_2
• FunctionField : Type u_3
• fieldInst : Field self.FunctionField
• val : self.Point → self.FunctionField → WithTop ℤ
• val_zero (P : self.Point) : self.val P 0 = ⊤
• val_one (P : self.Point) : self.val P 1 = 0
• val_mul (P : self.Point) (f g : self.FunctionField) : self.val P (f * g) = self.val P f + self.val P g
• val_add (P : self.Point) (f g : self.FunctionField) : min (self.val P f) (self.val P g) ≤ self.val P (f + g)
• val_ne_top (P : self.Point) (f : self.FunctionField) : f ≠ 0 → self.val P f ≠ ⊤
• val_surj (P : self.Point) (n : ℤ) : ∃ (f : self.FunctionField), f ≠ 0 ∧ self.val P f = ↑n

structure MorphismToP1 (C : SmoothProjectiveCurve) : Type (max (max (u_2 + 1) u_3) u_4)

A morphism C → ℙ¹ from a smooth projective curve, recorded via a chosen function f, its degree, and the (finite) fiber over each point of ℙ¹. The uniformizerComp Q represents the uniformizer at Q ∈ ℙ¹ pulled back to a function on C.

• f : C.FunctionField
• f_ne_zero : self.f ≠ 0
• deg : ℤ
• deg_pos : 0 < self.deg
• P1Point : Type u_2
• uniformizerComp : self.P1Point → C.FunctionField
• uniformizerComp_ne_zero (Q : self.P1Point) : self.uniformizerComp Q ≠ 0
• fiber : self.P1Point → Finset C.Point
• mem_fiber_iff (Q : self.P1Point) (P : C.Point) : P ∈ self.fiber Q ↔ 0 < C.val P (self.uniformizerComp Q)

theorem deg_eq_sum_fiber_val (C : SmoothProjectiveCurve) (φ : MorphismToP1 C) (Q : φ.P1Point) : φ.deg = ∑ P ∈ φ.fiber Q, WithTop.untopD 0 (C.val P (φ.uniformizerComp Q))

The degree of a morphism φ : C → ℙ¹ equals the sum, over the points P in the fiber over Q, of the valuation v_P(uniformizerComp Q). This is the content of the degree-fiber formula for morphisms to ℙ¹.

structure RationalMap (C : SmoothProjectiveCurve) (m : ℕ) : Type u_3

A rational map C → ℙ^{m-1} represented by m rational functions on C, not all of which are identically zero.

• coords : Fin m → C.FunctionField
• not_all_zero : ∃ (i : Fin m), self.coords i ≠ 0

def RationalMap.isDefinedAt {C : SmoothProjectiveCurve} {m : ℕ} (φ : RationalMap C m) (P : C.Point) : Prop

A rational map is defined at a point P if there exists a rescaling c ∈ k(C)^× so that every coordinate c · coords i has nonnegative valuation at P and at least one has valuation zero.

def RationalMap.isMorphism {C : SmoothProjectiveCurve} {m : ℕ} (φ : RationalMap C m) : Prop

A rational map is a morphism if it is defined at every point.

theorem rational_map_is_morphism (C : SmoothProjectiveCurve) {m : ℕ} (hm : 0 < m) (φ : RationalMap C m) : φ.isMorphism

Every rational map from a smooth projective curve to projective space is in fact a morphism: at any point one can scale by a uniformizer chosen with the correct order to clear poles and avoid common zeros.