class SmoothProjectiveCurve (C : AlgebraicGeometry.Scheme) : Prop

A smooth projective curve: an integral nonempty scheme of topological Krull dimension $1$ such that every morphism out of it is universally closed (encoding properness/completeness).

• isIntegral : AlgebraicGeometry.IsIntegral C
• krullDim_eq : topologicalKrullDim ↥C = 1
• nonempty : Nonempty ↥C
• morphism_universallyClosed {Y : AlgebraicGeometry.Scheme} (f : C ⟶ Y) : AlgebraicGeometry.UniversallyClosed f

theorem SmoothProjectiveCurve.morphism_isClosedMap {C : AlgebraicGeometry.Scheme} [SmoothProjectiveCurve C] {Y : AlgebraicGeometry.Scheme} (f : C ⟶ Y) : IsClosedMap ⇑f

The underlying continuous map of a morphism out of a smooth projective curve is closed.

theorem SmoothProjectiveCurve.rationalMap_extends_to_morphism {C V : AlgebraicGeometry.Scheme} [SmoothProjectiveCurve C] (φ : C.RationalMap V) : ∃! f : C ⟶ V, AlgebraicGeometry.Scheme.Hom.toRationalMap f = φ

Extension theorem: every rational map from a smooth projective curve $C$ to a variety $V$ extends uniquely to a morphism $C \to V$.

def IsConstantMorphism {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

A morphism of schemes is constant if its underlying map factors through a single point of the target.

noncomputable def SmoothProjectiveCurve.liftRationalMap {C V : AlgebraicGeometry.Scheme} [SmoothProjectiveCurve C] (φ : C.RationalMap V) : C ⟶ V

The unique morphism $C \to V$ extending a rational map $\varphi : C \dashrightarrow V$ from a smooth projective curve.

theorem irreducible_closed_eq_univ_of_not_subsingleton {Y : Type u_1} [TopologicalSpace Y] [T0Space Y] [IrreducibleSpace Y] (hdim : topologicalKrullDim Y ≤ 1) {S : Set Y} (hS_irred : IsIrreducible S) (hS_closed : IsClosed S) (hS_not_sub : ¬S.Subsingleton) : S = Set.univ

In an irreducible T0 space of Krull dimension at most $1$, any irreducible closed subset that is not a singleton must be the whole space.

theorem SmoothProjectiveCurve.morphism_constant_or_surjective {C₁ C₂ : AlgebraicGeometry.Scheme} [SmoothProjectiveCurve C₁] [SmoothProjectiveCurve C₂] (φ : C₁ ⟶ C₂) : IsConstantMorphism φ ∨ Function.Surjective ⇑φ

A morphism between smooth projective curves is either constant or surjective.

theorem SmoothProjectiveCurve.rationalMap_constant_or_surjective {C₁ C₂ : AlgebraicGeometry.Scheme} [SmoothProjectiveCurve C₁] [SmoothProjectiveCurve C₂] (φ : C₁.RationalMap C₂) (f : C₁ ⟶ C₂) (_hf : AlgebraicGeometry.Scheme.Hom.toRationalMap f = φ) : IsConstantMorphism f ∨ Function.Surjective ⇑f

A rational map between smooth projective curves (or rather, its unique extending morphism) is either constant or surjective.

theorem SmoothProjectiveCurve.corollary_18_7 {C₁ C₂ : AlgebraicGeometry.Scheme} [SmoothProjectiveCurve C₁] [SmoothProjectiveCurve C₂] (φ : C₁.RationalMap C₂) : IsConstantMorphism (liftRationalMap φ) ∨ Function.Surjective ⇑(liftRationalMap φ)

(Corollary 18.7) The unique morphism extending a rational map between smooth projective curves is either constant or surjective.