Finite morphisms between two-chart models

An extension of algebraic function fields induces a morphism of their two-chart models. The normalization maps on both affine charts are finite. The model over the larger field is proper over the constant field, while the target model is separated. Thus the induced morphism is proper. It is locally quasi-finite on the two source charts, and therefore finite.

This is the global finiteness assertion for the normalization morphism. It applies to inseparable extensions as well. The chart finiteness comes from finite normalization of polynomial rings; the passage from proper and locally quasi-finite to finite is Mathlib's Zariski main theorem.

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

theorem TauCeti.AlgebraicGeometry.twoChartModel.isFinite_map {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) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) : AlgebraicGeometry.IsFinite (map hF hF' hx hx' h)

The morphism of two-chart models induced by a finite function-field extension is finite. This includes inseparable extensions.