Flatness of the rational-function morphism #
A non-global rational function on an integral proper smooth relative curve gives a dominant morphism to the projective line. Its maps on stalks are injective: dominance over the reduced target makes the morphism scheme-theoretically dominant, while integrality of the source makes germs injective. The target stalk is either the function field or a discrete valuation ring, so the source stalk is a torsion-free, hence flat, module over it.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.flat_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)
:
The projective-line morphism associated to a non-global rational function is flat.
theorem
TauCeti.AlgebraicGeometry.SchemeWeilDivisor.finrank_rationalFunctionMorphism_eq_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)
(y z : ↥(ProjectiveLine.scheme K))
:
The finite-flat degree of the projective-line morphism attached to a non-global rational function is independent of the point of the projective line.