Finiteness of nonconstant morphisms from smooth proper curves

A proper morphism from an integral Noetherian smooth relative curve is locally quasi-finite as soon as no fibre is the whole curve. Indeed, a fibre over a closed point is a proper closed subset and hence finite. A fibre over a non-closed point contains no closed point, because proper morphisms are closed, and therefore contains at most the generic point. Zariski's main theorem then upgrades the morphism to a finite morphism.

Applied to the projective-line-valued morphism [g : 1], this isolates the remaining nonconstancy obligation in the geometric product-formula proof.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.instNonemptyCarrierCarrierCommRingCatToSchemeTopOpensOfIsIntegral {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : Nonempty ↥↑⊤

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isProper_rationalFunctionMorphism (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) : AlgebraicGeometry.IsProper (rationalFunctionMorphism K X f g)

The global projective-line-valued morphism attached to a rational function on a proper smooth relative curve is proper.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_genericPoint_mem_standardAffineOpen (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) : (rationalFunctionMorphism K X f g) (genericPoint ↥X) ∈ ProjectiveLine.standardAffineOpen K

The generic point of a smooth relative curve is mapped into the standard affine chart D₊(X₁) by its rational-function morphism. On that chart the map has coordinate g.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.exists_eq_germToFunctionField_top_of_universal_fiber (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (y : ↥(ProjectiveLine.scheme K)) (hyall : ⇑(rationalFunctionMorphism K X f g) ⁻¹' {y} = Set.univ) : ∃ (a : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a

If one fibre of the rational-function morphism is the whole curve, then the rational function is represented by a global section.

Indeed, the common image lies in D₊(X₁) because the generic point does. Pulling the affine coordinate X₀ / X₁ back to the curve gives the required global section, and its generic germ is g by ProjectiveLine.ofElement_appLE_affineCoordinate.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.locallyQuasiFinite_of_isProper_of_no_universal_fiber_smoothRelativeDimension_one (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] {Y : AlgebraicGeometry.Scheme} (φ : X ⟶ Y) [AlgebraicGeometry.IsProper φ] (hfiber : ∀ (y : ↥Y), ⇑φ ⁻¹' {y} ≠ Set.univ) : AlgebraicGeometry.LocallyQuasiFinite φ

A proper morphism from an integral Noetherian smooth relative curve is locally quasi-finite if none of its point fibres is the whole curve.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isFinite_rationalFunctionMorphism_of_no_universal_fiber (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hfiber : ∀ (y : ↥(ProjectiveLine.scheme K)), ⇑(rationalFunctionMorphism K X f g) ⁻¹' {y} ≠ Set.univ) : AlgebraicGeometry.IsFinite (rationalFunctionMorphism K X f g)

The rational-function morphism on a proper smooth curve is finite once no point fibre is the whole curve. This is the exact finiteness adapter needed before comparing the zero and infinity fibres.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_no_universal_fiber_of_nonGlobal (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (a : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) (y : ↥(ProjectiveLine.scheme K)) : ⇑(rationalFunctionMorphism K X f g) ⁻¹' {y} ≠ Set.univ

A rational function which is not represented by a global section has no universal point fibre under its projective-line-valued morphism.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isFinite_rationalFunctionMorphism_of_nonGlobal (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (a : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) : AlgebraicGeometry.IsFinite (rationalFunctionMorphism K X f g)

The rational-function morphism of a non-global rational function on a proper smooth curve is finite. This is the premise-free nonconstancy consumer needed for the geometric product formula; the remaining work is to compare the zero and infinity fibres.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMorphism_genericPoint_eq_genericPoint_of_nonGlobal (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (a : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) : (rationalFunctionMorphism K X f g) (genericPoint ↥X) = genericPoint ↥(ProjectiveLine.scheme K)

A non-global rational function maps the generic point of its source curve to the generic point of the projective line. If the image were closed, its closed preimage would contain the generic point of the source and hence would be the whole curve, contradicting non-globality.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.isDominant_rationalFunctionMorphism_of_nonGlobal (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (a : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) : AlgebraicGeometry.IsDominant (rationalFunctionMorphism K X f g)

The projective-line morphism of a non-global rational function is dominant.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.surjective_rationalFunctionMorphism_of_nonGlobal (K : Type u) [Field K] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [AlgebraicGeometry.SmoothOfRelativeDimension 1 f] [AlgebraicGeometry.IsProper f] (g : Additive (↑X.functionField)ˣ) (hg : ¬∃ (a : ↑(X.presheaf.obj (Opposite.op ⊤))), ↑(Additive.toMul g) = (CategoryTheory.ConcreteCategory.hom (X.germToFunctionField ⊤)) a) : AlgebraicGeometry.Surjective (rationalFunctionMorphism K X f g)

The projective-line morphism of a non-global rational function is surjective.