A rational place forces exact constants

A constant algebraic over the base field is regular at every place. At a rational place its residue is the residue of a base-field element. Their difference is algebraic and has valuation less than one, so it must vanish. Thus the existence of a rational place certifies exactness of the constant field, including for composita with a completely split rational place.

Conversely, a place of a finite extension over a larger constant field forces that field to be algebraic over the base.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.1 and Corollary 3.9.7.

theorem TauCeti.Place.finrank_algebraicClosure_dvd_degree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : Module.finrank k ↥(algebraicClosure k F) ∣ P.degree

The degree of every place is divisible by the degree of the field of constants: the residue field is an algebra over algebraicClosure k F, which is regular at every place.

theorem TauCeti.Place.isIntegrallyClosedIn_of_degree_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (hP : P.degree = 1) : IsIntegrallyClosedIn k F

If F / k has a rational place, every element of F algebraic over k belongs to k. No function-field or separability hypothesis is needed.

theorem TauCeti.Place.isFunctionField_of_place {k : Type u} {k' : Type u'} {F' : Type v'} [Field k] [Field k'] [Field F'] [Algebra k k'] [Algebra k F'] [Algebra k' F'] [IsScalarTower k k' F'] (hFk : IsFunctionField k F') (P' : Place k' F') : IsFunctionField k' F'

If F' / k is a function field and F' has a place over k', then it is a function field over k': the existence of a place forces k' to be algebraic over k.