Finite chart maps induced by an extension of function fields

An embedding of function fields over k induces maps between their two normalization charts. Each map is finite: the larger chart is finite over the polynomial ring in the chosen function, and therefore finite over the intermediate normalization chart. These are the affine finiteness statements needed to make the induced morphism of two-chart models finite.

The argument uses finiteness of polynomial normalization, including inseparable extensions, and does not assume that the function-field extension is separable.

See Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.2 and Appendix B.

theorem TauCeti.AlgebraicGeometry.twoChartModel.finiteChartMap_finite {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF' : IsFunctionField k F') {x : F} {x' : F'} (hx : Transcendental k x) (h : (algebraMap F F') x = x') : (finiteChartMap h).Finite

The map of finite charts induced by an embedding of function fields is finite.

theorem TauCeti.AlgebraicGeometry.twoChartModel.infinityChartMap_finite {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF' : IsFunctionField k F') {x : F} {x' : F'} (hx : Transcendental k x) (h : (algebraMap F F') x = x') : (infinityChartMap h).Finite

The map of charts at infinity induced by an embedding of function fields is finite.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isFinite_specMap_finiteChartMap {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF' : IsFunctionField k F') {x : F} {x' : F'} (hx : Transcendental k x) (h : (algebraMap F F') x = x') : AlgebraicGeometry.IsFinite (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (finiteChartMap h)))

The induced map of affine schemes on the finite charts is finite.

theorem TauCeti.AlgebraicGeometry.twoChartModel.isFinite_specMap_infinityChartMap {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF' : IsFunctionField k F') {x : F} {x' : F'} (hx : Transcendental k x) (h : (algebraMap F F') x = x') : AlgebraicGeometry.IsFinite (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (infinityChartMap h)))

The induced map of affine schemes on the charts at infinity is finite.