structure ArithmeticGeometry.Curve_k (k : Type u) [Field k] : Type (u + 1)

A curve over a field $k$: an integral scheme equipped with a smooth proper structure morphism to $\mathrm{Spec}(k)$ of relative dimension $1$.

• toScheme : AlgebraicGeometry.Scheme
• structureMorphism : self.toScheme ⟶ AlgebraicGeometry.Spec (CommRingCat.of k)
• isIntegral : AlgebraicGeometry.IsIntegral self.toScheme
• isProper : AlgebraicGeometry.IsProper self.structureMorphism
• isSmooth : AlgebraicGeometry.SmoothOfRelativeDimension 1 self.structureMorphism

class ArithmeticGeometry.FunctionField_k (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] : Prop

A function field of one variable over $k$: a finitely generated extension $F/k$ of transcendence degree $1$ in which $k$ is algebraically closed in $F$.

• finitelyGenerated : ⊤.FG
• transcendenceDegreeOne : ∃ (x : F), Transcendental k x ∧ Algebra.IsAlgebraic (↥k⟮x⟯) F
• algClosedInF (x : F) : IsAlgebraic k x → x ∈ ⊥

noncomputable def ArithmeticGeometry.FunctionField_k.Morphism.degree {F₁ : Type u_2} {F₂ : Type u_3} [Field F₁] [Field F₂] (φ : F₂ →+* F₁) : ℕ

The degree of a morphism of function fields $\varphi : F_2 \to F_1$: the degree $[F_1 : \varphi(F_2)]$ of $F_1$ over the image.