Rational maps attached to rational functions

For an integral scheme X over a field K, a nonzero rational function gives the function-field point [g : 1] of the projective line. This file proves that the point respects the base-field maps and spreads it out to a rational map X ⤏ ℙ¹_K.

The construction is the rational-map input to the geometric proof of the product formula in TauCetiRoadmap/JacobianChallenge/README.md, Layer A, "Divisors on a curve". The subsequent extension across a regular curve and the comparison of the zero and infinity fibres remain separate mathematical steps.

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

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.specMap_baseFieldToFunctionField {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) : AlgebraicGeometry.Spec.map (CommRingCat.ofHom (baseFieldToFunctionField K f)) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) f

On spectra, the base-field map to the function field is the structure morphism restricted to the generic point.

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionGenericMorphism_comp_structureMap {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (g : Additive (↑X.functionField)ˣ) : CategoryTheory.CategoryStruct.comp (rationalFunctionGenericMorphism K f g) (ProjectiveLine.structureMap K) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) f

The function-field point [g : 1] of ℙ¹_K is compatible with the structure morphism of X at its generic point.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMapOver {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (g : Additive (↑X.functionField)ˣ) : { φ : X.RationalMap (ProjectiveLine.scheme K) // φ.compHom (ProjectiveLine.structureMap K) = AlgebraicGeometry.Scheme.Hom.toRationalMap f }

The rational map over K associated to a nonzero rational function, bundled together with its equality over Spec K.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMap {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (g : Additive (↑X.functionField)ˣ) : X.RationalMap (ProjectiveLine.scheme K)

The rational map X ⤏ ℙ¹_K associated to a nonzero rational function.

Equations

• TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMap K f g = ↑(TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMapOver K f g)

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMap_comp_structureMap {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (g : Additive (↑X.functionField)ˣ) : (rationalFunctionMap K f g).compHom (ProjectiveLine.structureMap K) = AlgebraicGeometry.Scheme.Hom.toRationalMap f

The rational-function map is a rational map over K.

@[simp]

theorem TauCeti.AlgebraicGeometry.SchemeWeilDivisor.rationalFunctionMap_fromFunctionField {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] (K : Type u) [Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) (g : Additive (↑X.functionField)ˣ) : (rationalFunctionMap K f g).fromFunctionField = rationalFunctionGenericMorphism K f g

Restricting the rational-function map back to the function field recovers [g : 1].