structure ClosedPointRes (k : Type u_1) [Field k] : Type (max u_1 (u_2 + 1))

• residueField : Type u_2
• residueFieldField : Field self.residueField
• residueFieldAlgebra : Algebra k self.residueField
• finiteDimensional : FiniteDimensional k self.residueField

noncomputable def ClosedPointRes.degreePoint {k : Type u_1} [Field k] (P : ClosedPointRes k) : ℕ

@[reducible, inline]

abbrev CurveDivisor (C : Type u_1) : Type u_1

noncomputable def CurveDivisor.coeff {C : Type u_1} (D : CurveDivisor C) (P : C) : ℤ

noncomputable def CurveDivisor.divisorSupport {C : Type u_1} (D : CurveDivisor C) : Finset C

noncomputable def CurveDivisor.degree (C : Type u_1) : CurveDivisor C →+ ℤ

@[simp]

theorem CurveDivisor.degree_single {C : Type u_1} (P : C) (n : ℤ) : ((degree C) fun₀ | P => n) = n

@[simp]

theorem CurveDivisor.degree_zero {C : Type u_1} : (degree C) 0 = 0

@[simp]

theorem CurveDivisor.degree_add {C : Type u_1} (D₁ D₂ : CurveDivisor C) : (degree C) (D₁ + D₂) = (degree C) D₁ + (degree C) D₂

@[simp]

theorem CurveDivisor.degree_neg {C : Type u_1} (D : CurveDivisor C) : (degree C) (-D) = -(degree C) D

theorem CurveDivisor.degree_sub {C : Type u_1} (D₁ D₂ : CurveDivisor C) : (degree C) (D₁ - D₂) = (degree C) D₁ - (degree C) D₂

theorem CurveDivisor.degree_eq_sum {C : Type u_1} (D : CurveDivisor C) : (degree C) D = Finsupp.sum D fun (x : C) (n : ℤ) => n

noncomputable def CurveDivisor.degreeWeighted {C : Type u_1} (deg : C → ℕ) : CurveDivisor C →+ ℤ

theorem CurveDivisor.degreeWeighted_sub {C : Type u_1} (deg : C → ℕ) (D₁ D₂ : CurveDivisor C) : (degreeWeighted deg) (D₁ - D₂) = (degreeWeighted deg) D₁ - (degreeWeighted deg) D₂

theorem CurveDivisor.degreeWeighted_eq_sum {C : Type u_1} (deg : C → ℕ) (D : CurveDivisor C) : (degreeWeighted deg) D = Finsupp.sum D fun (p : C) (n : ℤ) => n * ↑(deg p)

@[implicit_reducible]

noncomputable instance CurveDivisor.galoisSMul {C : Type u_1} {G : Type u_2} [Group G] [MulAction G C] : SMul G (CurveDivisor C)

@[implicit_reducible]

noncomputable instance CurveDivisor.galoisMulAction {C : Type u_1} {G : Type u_2} [Group G] [MulAction G C] : MulAction G (CurveDivisor C)

def CurveDivisor.IsDefinedOverK {C : Type u_1} (G : Type u_3) [Group G] [MulAction G C] (D : CurveDivisor C) : Prop

noncomputable def CurveDivisor.divZeros {C : Type u_1} (D : CurveDivisor C) : CurveDivisor C

noncomputable def CurveDivisor.divPoles {C : Type u_1} (D : CurveDivisor C) : CurveDivisor C

@[simp]

theorem CurveDivisor.divZeros_apply {C : Type u_1} (D : CurveDivisor C) (P : C) : D.divZeros P = max (D P) 0

@[simp]

theorem CurveDivisor.divPoles_apply {C : Type u_1} (D : CurveDivisor C) (P : C) : D.divPoles P = max (-D P) 0

theorem CurveDivisor.divZeros_nonneg {C : Type u_1} (D : CurveDivisor C) (P : C) : 0 ≤ D.divZeros P

theorem CurveDivisor.divPoles_nonneg {C : Type u_1} (D : CurveDivisor C) (P : C) : 0 ≤ D.divPoles P

theorem CurveDivisor.eq_divZeros_sub_divPoles {C : Type u_1} (D : CurveDivisor C) : D = D.divZeros - D.divPoles

@[reducible, inline]

abbrev ClosedPoint (G : Type u_1) (C : Type u_2) [Group G] [MulAction G C] : Type u_2

def ClosedPoint.mk {G : Type u_1} {C : Type u_2} [Group G] [MulAction G C] (P : C) : ClosedPoint G C

def ClosedPoint.toOrbit {G : Type u_1} {C : Type u_2} [Group G] [MulAction G C] (P : ClosedPoint G C) : Set C

theorem ClosedPoint.mk_eq_mk_iff {G : Type u_1} {C : Type u_2} [Group G] [MulAction G C] (P Q : C) : mk P = mk Q ↔ P ∈ MulAction.orbit G Q

noncomputable def degreeClosedPoint (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : ℕ

@[reducible, inline]

abbrev RationalDivisor (G : Type u_1) (C : Type u_2) [Group G] [MulAction G C] : Type u_2

noncomputable def RationalDivisor.coeff {G : Type u_1} {C : Type u_2} [Group G] [MulAction G C] (D : RationalDivisor G C) (P : ClosedPoint G C) : ℤ

noncomputable def RationalDivisor.rationalDivisorSupport {G : Type u_1} {C : Type u_2} [Group G] [MulAction G C] (D : RationalDivisor G C) : Finset (ClosedPoint G C)

class CurveWithOrd (C : Type u_1) (F : Type u_2) [Field F] : Type (max u_1 u_2)

• ord : C → Fˣ → ℤ
• ord_mul (P : C) (f g : Fˣ) : ord P (f * g) = ord P f + ord P g
• ord_add (P : C) (f g : Fˣ) (hfg : ↑f + ↑g ≠ 0) : ord P (Units.mk0 (↑f + ↑g) hfg) ≥ min (ord P f) (ord P g)
• uniformizer_exists (P : C) : ∃ (π : Fˣ), ord P π = 1

class FunctionFieldCurve (C : Type u_1) (F : Type u_2) [Field F] extends CurveWithOrd C F : Type (max u_1 u_2)

• ord : C → Fˣ → ℤ
• ord_mul (P : C) (f g : Fˣ) : ord P (f * g) = ord P f + ord P g
• ord_add (P : C) (f g : Fˣ) (hfg : ↑f + ↑g ≠ 0) : ord P (Units.mk0 (↑f + ↑g) hfg) ≥ min (ord P f) (ord P g)
• uniformizer_exists (P : C) : ∃ (π : Fˣ), ord P π = 1
• isCoordRingElem : Fˣ → Prop
• fraction_rep (f : Fˣ) : ∃ (g : Fˣ) (h : Fˣ), isCoordRingElem C g ∧ isCoordRingElem C h ∧ f = g * h⁻¹
• ord_nonneg_of_coordRingElem (f : Fˣ) : isCoordRingElem C f → ∀ (P : C), 0 ≤ CurveWithOrd.ord P f
• zeroLocus_finite (f : Fˣ) : isCoordRingElem C f → {P : C | 0 < CurveWithOrd.ord P f}.Finite

theorem FunctionFieldCurve.coordRing_finite_support {C : Type u_1} {F : Type u_2} [Field F] [inst : FunctionFieldCurve C F] (f : Fˣ) (hf : isCoordRingElem C f) : (Function.support fun (P : C) => CurveWithOrd.ord P f).Finite

theorem CurveWithOrd.ord_one {C : Type u_1} {F : Type u_2} [Field F] [CurveWithOrd C F] (P : C) : ord P 1 = 0

theorem CurveWithOrd.ord_inv {C : Type u_1} {F : Type u_2} [Field F] [CurveWithOrd C F] (P : C) (f : Fˣ) : ord P f⁻¹ = -ord P f

theorem ord_finite_support {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] (f : Fˣ) : (Function.support fun (P : C) => CurveWithOrd.ord P f).Finite

noncomputable def CurveWithOrd.principalDivisor {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] (f : Fˣ) : CurveDivisor C

@[simp]

theorem CurveWithOrd.principalDivisor_apply {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] (f : Fˣ) (P : C) : (principalDivisor f) P = ord P f

@[simp]

theorem CurveWithOrd.principalDivisor_one {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] : principalDivisor 1 = 0

theorem CurveWithOrd.principalDivisor_mul {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] (f g : Fˣ) : principalDivisor (f * g) = principalDivisor f + principalDivisor g

theorem CurveWithOrd.principalDivisor_inv {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] (f : Fˣ) : principalDivisor f⁻¹ = -principalDivisor f

noncomputable def CurveWithOrd.principalDivisorHom {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] : Fˣ →* Multiplicative (CurveDivisor C)

noncomputable def CurveWithOrd.principalDivisors {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] : AddSubgroup (CurveDivisor C)

def CurveWithOrd.IsPrincipal {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] (D : CurveDivisor C) : Prop

theorem CurveWithOrd.isPrincipal_iff {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] (D : CurveDivisor C) : IsPrincipal D ↔ ∃ (f : Fˣ), principalDivisor f = D

noncomputable def CurveWithOrd.divAddHom {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] : Additive Fˣ →+ CurveDivisor C

@[reducible, inline]

abbrev CurveWithOrd.PicardGroup (C : Type u_3) (F : Type u_4) [Field F] [FunctionFieldCurve C F] : Type u_3

noncomputable def CurveWithOrd.toPicardGroup {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] : CurveDivisor C →+ PicardGroup C F

theorem CurveWithOrd.exact_at_divisors {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] : divAddHom.range = toPicardGroup.ker

theorem CurveWithOrd.ker_toPicardGroup {C : Type u_1} {F : Type u_2} [Field F] [FunctionFieldCurve C F] : toPicardGroup.ker = principalDivisors

class CurveWithConstants (C : Type u_1) (k : Type u_2) (F : Type u_3) [Field k] [Field F] [Algebra k F] extends FunctionFieldCurve C F : Type (max u_1 u_3)

• ord : C → Fˣ → ℤ
• ord_mul (P : C) (f g : Fˣ) : ord P (f * g) = ord P f + ord P g
• ord_add (P : C) (f g : Fˣ) (hfg : ↑f + ↑g ≠ 0) : ord P (Units.mk0 (↑f + ↑g) hfg) ≥ min (ord P f) (ord P g)
• uniformizer_exists (P : C) : ∃ (π : Fˣ), ord P π = 1
• isCoordRingElem : Fˣ → Prop
• fraction_rep (f : Fˣ) : ∃ (g : Fˣ) (h : Fˣ), isCoordRingElem C g ∧ isCoordRingElem C h ∧ f = g * h⁻¹
• ord_nonneg_of_coordRingElem (f : Fˣ) : isCoordRingElem C f → ∀ (P : C), 0 ≤ CurveWithOrd.ord P f
• zeroLocus_finite (f : Fˣ) : isCoordRingElem C f → {P : C | 0 < CurveWithOrd.ord P f}.Finite
• const_isCoordRingElem (a : kˣ) : FunctionFieldCurve.isCoordRingElem C ((Units.map ↑(algebraMap k F)) a)
• const_inv_isCoordRingElem (a : kˣ) : FunctionFieldCurve.isCoordRingElem C ((Units.map ↑(algebraMap k F)) a)⁻¹
• algClosed_in_extension (x : F) : IsAlgebraic k x → x ∈ (algebraMap k F).range
• ord_zero_algebraic (f : Fˣ) : (∀ (P : C), CurveWithOrd.ord P f = 0) → IsAlgebraic k ↑f
• residue_eval (P : C) : ∃ (evalP : F →ₗ[k] k), ∀ (f : Fˣ), CurveWithOrd.ord P f ≥ 0 → evalP ↑f = 0 → CurveWithOrd.ord P f ≥ 1

theorem CurveWithConstants.ord_constant {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [inst : CurveWithConstants C k F] (P : C) (a : kˣ) : CurveWithOrd.ord P ((Units.map ↑(algebraMap k F)) a) = 0

theorem CurveWithConstants.ker_div_eq_constants {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [inst : CurveWithConstants C k F] (f : Fˣ) (hf : ∀ (P : C), CurveWithOrd.ord P f = 0) : ∃ (a : kˣ), (Units.map ↑(algebraMap k F)) a = f

noncomputable def CurveWithConstants.constantsEmb {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] : kˣ →* Fˣ

@[simp]

theorem CurveWithConstants.constantsEmb_def {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] (a : kˣ) : constantsEmb a = (Units.map ↑(algebraMap k F)) a

theorem CurveWithConstants.constantsEmb_injective {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] : Function.Injective ⇑constantsEmb

theorem CurveWithConstants.principalDivisor_constant {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (a : kˣ) : CurveWithOrd.principalDivisor (constantsEmb a) = 0

theorem CurveWithConstants.exact_at_functionField {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) : CurveWithOrd.principalDivisor f = 0 ↔ ∃ (a : kˣ), constantsEmb a = f

theorem triangle_equality_valuation {F : Type u_1} [Field F] {Γ₀ : Type u_2} [LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation F Γ₀) {x y : F} (h : v x ≠ v y) : v (x + y) = min (v x) (v y)

structure FunctionFieldPlace (F : Type u_1) [Field F] (k : Type u_2) [Field k] : Type (max u_1 u_2)

• valuationSubring : ValuationSubring F
• isPrincipalIdealRing : IsPrincipalIdealRing ↥self.valuationSubring
• notIsField : ¬IsField ↥self.valuationSubring
• residueFieldEquiv : IsLocalRing.ResidueField ↥self.valuationSubring ≃+* k

instance FunctionFieldPlace.instIsPrincipalIdealRingSubtypeMemValuationSubringValuationSubring {F : Type u_1} [Field F] {k : Type u_2} [Field k] (P : FunctionFieldPlace F k) : IsPrincipalIdealRing ↥P.valuationSubring

instance FunctionFieldPlace.instIsFractionRingSubtypeMemValuationSubringValuationSubring {F : Type u_1} [Field F] {k : Type u_2} [Field k] (P : FunctionFieldPlace F k) : IsFractionRing (↥P.valuationSubring) F

@[reducible, inline]

abbrev FunctionFieldDivisor (F : Type u_1) [Field F] (k : Type u_2) [Field k] : Type (max u_2 u_1)

noncomputable def FunctionFieldDivisor.coeff {F : Type u_1} [Field F] {k : Type u_2} [Field k] (D : FunctionFieldDivisor F k) (P : FunctionFieldPlace F k) : ℤ

noncomputable def FunctionFieldDivisor.divisorSupport {F : Type u_1} [Field F] {k : Type u_2} [Field k] (D : FunctionFieldDivisor F k) : Finset (FunctionFieldPlace F k)

def ArithmeticGeometry.FunctionField_k.Morphism.ramificationIndex {F₁ : Type u_2} {F₂ : Type u_3} [Field F₁] [Field F₂] (φ : F₂ →+* F₁) (ordP : F₁ˣ → ℤ) (tQ : F₂ˣ) : ℤ

def ArithmeticGeometry.FunctionField_k.Morphism.IsUnramifiedAt {F₁ : Type u_2} {F₂ : Type u_3} [Field F₁] [Field F₂] (φ : F₂ →+* F₁) (ordP : F₁ˣ → ℤ) (tQ : F₂ˣ) : Prop

def ArithmeticGeometry.FunctionField_k.Morphism.IsUnramified {F₁ : Type u_2} {F₂ : Type u_3} [Field F₁] [Field F₂] (φ : F₂ →+* F₁) (places : Type u_4) (ordAt : places → F₁ˣ → ℤ) (uniformizerAt : places → F₂ˣ) : Prop

theorem CurveWithConstants.divZeros_principalDivisor_constant {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (a : kˣ) : (CurveWithOrd.principalDivisor (constantsEmb a)).divZeros = 0

theorem CurveWithConstants.divPoles_principalDivisor_constant {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (a : kˣ) : (CurveWithOrd.principalDivisor (constantsEmb a)).divPoles = 0

theorem CurveWithConstants.degree_divZeros_principalDivisor_constant {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (a : kˣ) : (CurveDivisor.degree C) (CurveWithOrd.principalDivisor (constantsEmb a)).divZeros = 0

theorem CurveWithConstants.degree_divPoles_principalDivisor_constant {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (a : kˣ) : (CurveDivisor.degree C) (CurveWithOrd.principalDivisor (constantsEmb a)).divPoles = 0

theorem CurveWithConstants.degree_divZeros_principalDivisor_eq_sum_ord {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) : (CurveDivisor.degree C) (CurveWithOrd.principalDivisor f).divZeros = ∑ P ∈ (CurveWithOrd.principalDivisor f).divZeros.support, CurveWithOrd.ord P f

theorem CurveWithConstants.nonconstant_transcendental {C : Type u_4} {k : Type u_5} {F : Type u_6} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) (hf : ¬∃ (a : kˣ), constantsEmb a = f) : Transcendental k ↑f

theorem CurveWithConstants.dedekind_realization_bridge_ax {C : Type u_4} {k : Type u_5} {F : Type u_6} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) (hf_trans : Transcendental k ↑f) : ∑ P ∈ (CurveWithOrd.principalDivisor f).divZeros.support, CurveWithOrd.ord P f = ↑(Module.finrank (↥k⟮↑f⟯) F)

theorem CurveWithConstants.sum_pos_ord_eq_degree_morphism {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) (hf_trans : Transcendental k ↑f) : ∑ P ∈ (CurveWithOrd.principalDivisor f).divZeros.support, CurveWithOrd.ord P f = ↑(Module.finrank (↥k⟮↑f⟯) F)

theorem CurveWithConstants.sum_pos_ord_eq_finrank {C : Type u_4} {k : Type u_5} {F : Type u_6} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) (hf : ¬∃ (a : kˣ), constantsEmb a = f) : ∑ P ∈ (CurveWithOrd.principalDivisor f).divZeros.support, CurveWithOrd.ord P f = ↑(Module.finrank (↥k⟮↑f⟯) F)

theorem CurveWithConstants.theorem_19_22_divZeros {C : Type u_4} {k : Type u_5} {F : Type u_6} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) (hf : ¬∃ (a : kˣ), constantsEmb a = f) : (CurveDivisor.degree C) (CurveWithOrd.principalDivisor f).divZeros = ↑(Module.finrank (↥k⟮↑f⟯) F)

theorem CurveWithConstants.divPoles_eq_divZeros_inv {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) : (CurveWithOrd.principalDivisor f).divPoles = (CurveWithOrd.principalDivisor f⁻¹).divZeros

theorem CurveWithConstants.not_constant_inv {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] (f : Fˣ) (hf : ¬∃ (a : kˣ), constantsEmb a = f) : ¬∃ (a : kˣ), constantsEmb a = f⁻¹

theorem CurveWithConstants.adjoin_inv_eq {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] (f : Fˣ) : k⟮↑f⁻¹⟯ = k⟮↑f⟯

theorem CurveWithConstants.degree_divZeros_principalDivisor_eq_extensionDegree {C : Type u_4} {k : Type u_5} {F : Type u_6} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) (hf : ¬∃ (a : kˣ), constantsEmb a = f) : (CurveDivisor.degree C) (CurveWithOrd.principalDivisor f).divZeros = ↑(Module.finrank (↥k⟮↑f⟯) F)

theorem CurveWithConstants.degree_divPoles_principalDivisor_eq_extensionDegree {C : Type u_4} {k : Type u_5} {F : Type u_6} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) (hf : ¬∃ (a : kˣ), constantsEmb a = f) : (CurveDivisor.degree C) (CurveWithOrd.principalDivisor f).divPoles = ↑(Module.finrank (↥k⟮↑f⟯) F)

theorem CurveWithConstants.degree_divZeros_eq_degree_divPoles {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) : (CurveDivisor.degree C) (CurveWithOrd.principalDivisor f).divZeros = (CurveDivisor.degree C) (CurveWithOrd.principalDivisor f).divPoles

theorem CurveWithConstants.degree_principalDivisor_eq_zero {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) : (CurveDivisor.degree C) (CurveWithOrd.principalDivisor f) = 0

theorem CurveWithOrd.degree_divZeros_eq_degree_divPoles {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) : (CurveDivisor.degree C) (principalDivisor f).divZeros = (CurveDivisor.degree C) (principalDivisor f).divPoles

theorem CurveWithOrd.degree_principalDivisor_eq_zero {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) : (CurveDivisor.degree C) (principalDivisor f) = 0

theorem CurveWithOrd.corollary_19_23_deg_div_eq_zero {C : Type u_1} {k : Type u_2} {F : Type u_3} [Field k] [Field F] [Algebra k F] [CurveWithConstants C k F] (f : Fˣ) : (CurveDivisor.degree C) (principalDivisor f) = 0

structure CurveMorphismData (C₁ : Type u_1) (C₂ : Type u_2) : Type (max u_1 u_2)

• toFun : C₁ → C₂
• ramificationIndex : C₁ → ℤ

  The local ramification index e_P = d_P at a height-one prime P of the target ring, the multiplicity with which f^*(f(P)) contains P.

• ramificationIndex : C₁ → ℤ
• fiber : C₂ → Finset C₁
• fiber_maps_to (Q : C₂) (P : C₁) : P ∈ self.fiber Q → self.toFun P = Q
• fiber_complete (Q : C₂) (P : C₁) : self.toFun P = Q → P ∈ self.fiber Q
• residueFieldDegreeRatio : C₁ → ℤ

noncomputable def CurveMorphismData.pullbackPoint {C₁ : Type u_1} {C₂ : Type u_2} (φ : CurveMorphismData C₁ C₂) (Q : C₂) : CurveDivisor C₁

noncomputable def CurveMorphismData.pullback {C₁ : Type u_1} {C₂ : Type u_2} (φ : CurveMorphismData C₁ C₂) : CurveDivisor C₂ →+ CurveDivisor C₁

noncomputable def CurveMorphismData.pushforward {C₁ : Type u_1} {C₂ : Type u_2} (φ : CurveMorphismData C₁ C₂) : CurveDivisor C₁ →+ CurveDivisor C₂

@[simp]

theorem CurveMorphismData.pushforward_single {C₁ : Type u_1} {C₂ : Type u_2} (φ : CurveMorphismData C₁ C₂) (P : C₁) (n : ℤ) : (φ.pushforward fun₀ | P => n) = fun₀ | φ.toFun P => n

noncomputable def CurveMorphismData.pushforwardGeneral {C₁ : Type u_1} {C₂ : Type u_2} (φ : CurveMorphismData C₁ C₂) : CurveDivisor C₁ →+ CurveDivisor C₂

theorem ArithmeticGeometry.Pic0_trivial_imp_iso_P1_of_two_rational_points {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (htriv : C.Pic0IsTrivial) {P Q : C.RatPoint} (hPQ : P ≠ Q) : C.IsIsomorphicToP1

theorem ArithmeticGeometry.iso_P1_iff_Pic0_trivial_of_two_rational_points {k : Type u_1} [Field k] (C : SmoothProjectiveCurve k) (hpts : ∃ (P : C.RatPoint) (Q : C.RatPoint), P ≠ Q) : C.IsIsomorphicToP1 ↔ C.Pic0IsTrivial