Existence of extensions of places

Every place of an algebraic function field extends across an integral field extension. More generally, the base field may also grow by an integral extension: a valuation trivial on the smaller base field is automatically trivial on the larger one. For an extension of algebraic function fields with F' / F finite, both integrality hypotheses are automatic, the one on the base fields because the base extension is then finite. The same argument shows that the places above a place P see the whole integral closure of its valuation ring: an element regular at all of them is integral over 𝒪_P.

The proof dominates the local valuation ring of the original place by a valuation subring of the larger function field. Locality ensures that the resulting valuation subring is proper. Since valuation subrings are integrally closed, it contains the enlarged base field, so it defines a place whose restriction is the original place.

Main results

• TauCeti.Place.restrict_surjective: every place downstairs is the restriction of a place upstairs (Stichtenoth, Proposition 3.1.7).
• TauCeti.Place.restrict_surjective_of_finiteDimensional: the same statement for an extension of algebraic function fields, where both integrality hypotheses are theorems rather than hypotheses.
• TauCeti.Place.isIntegral_integers_algebraMap: constants are integral over 𝒪_P.
• TauCeti.Place.isIntegral_iff_forall_restrict_eq_mem_integers: the integral closure of the valuation ring 𝒪_P in the larger field is the intersection of the valuation rings of the places above P (Stichtenoth, Section III.2).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.1.7 and Section III.2.

theorem TauCeti.Place.restrict_surjective {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral k k'] [Algebra.IsIntegral F F'] (hF' : IsFunctionField k' F') : Function.Surjective fun (P' : Place k' F') => restrict k F P'

Existence of extensions of places (Stichtenoth, Proposition 3.1.7): if both the field extension and the base-field extension are integral, every place of F / k is the restriction of a place of F' / k'.

theorem TauCeti.Place.isIntegral_integers_algebraMap {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral k k'] (P : Place k F) (c : k') : IsIntegral (↥P.integers) ((algebraMap k' F') c)

Constants of F' are integral over the valuation ring of every place of F / k: they are integral over k, which lies in 𝒪_P.

theorem TauCeti.Place.isIntegral_iff_forall_restrict_eq_mem_integers {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsIntegral k k'] [Algebra.IsIntegral F F'] (hF' : IsFunctionField k' F') (P : Place k F) {x : F'} : IsIntegral (↥P.integers) x ↔ ∀ (P' : Place k' F'), restrict k F P' = P → x ∈ P'.integers

The integral closure of 𝒪_P is the intersection of the valuation rings above P (Stichtenoth, Section III.2): an element of F' is integral over the valuation ring of a place P of F / k exactly when it is regular at every place of F' / k' lying over P.

An element outside the integral closure is separated from it by a valuation subring of F'; that subring contains the base field k', whose elements are integral over k, and it contains 𝒪_P, so it is the valuation ring of a place lying over P.

theorem TauCeti.Place.restrict_surjective_of_finiteDimensional {k : Type u} {k' : Type u'} {F : Type v} {F' : Type v'} [Field k] [Field k'] [Field F] [Field F'] [Algebra k k'] [Algebra k F] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') : Function.Surjective fun (P' : Place k' F') => restrict k F P'

Existence of extensions of places for an extension of function fields (Stichtenoth, Proposition 3.1.7): every place of F / k is the restriction of a place of F' / k'.

This is a convenience corollary of TauCeti.Place.restrict_surjective, which replaces both explicit integrality hypotheses by the function-field hypotheses together with finiteness of F' / F: it asks nothing of the base extension, since k' / k is then finite by TauCeti.IsFunctionField.finiteDimensional_baseExtension. The general statement TauCeti.Place.restrict_surjective stays available for an infinite algebraic extension F' / F.