Finite extensions of the constant field

A finite extension of constants yields a finite compositum over the original field, and a separable extension of constants produces a separable compositum. Exactness of the original constant field is needed for neither. The function-field theorem for arbitrary algebraic extensions of constants is in ConstantExtension.Algebraic.

Under the hypotheses that make constant field extensions well behaved — the original constant field k is exact in F and k' / k is separable — the compositum acquires no new separable constants: no element of F · k' outside k' is separable over k'. Perfectness of k' upgrades this to exactness: when k' is perfect — for instance when k is perfect and k' / k is algebraic — every algebraic element is separable over k', so k' is the full field of constants of F · k'. Perfectness cannot simply be dropped: over an imperfect k an inseparable constant field extension can enlarge the field of constants beyond k'. For instance, k = 𝔽_p(t, u) is exact in F = k(x, y) with y ^ p = t * x ^ p + u, but for k' = k(t ^ (1/p)) the element y - t ^ (1/p) * x of F · k' is a p-th root of u, and u ^ (1/p) ∉ k'.

Finite extensions of constants with as many elements as desired always exist, realized as composita inside an algebraic closure of F. Over a finite constant field this is how arguments that need many constants, such as choosing a vector outside finitely many proper subspaces, are carried out after a finite constant field extension.

Main results

• TauCeti.finiteDimensional_of_constantCompositum_eq_top: a compositum with finite constants is finite over the original field.
• TauCeti.finiteDimensional_base_of_constantCompositum_eq_top: conversely, for an exact k and separable k' / k, a compositum finite over the original field has finite constants.
• TauCeti.isSeparable_of_constantCompositum_eq_top: the compositum of a separable constant field extension is separable over the original field.
• TauCeti.separableClosure_eq_bot_of_constantCompositum_eq_top: for a separable constant field extension of an exact constant field, k' is separably closed in F · k'.
• TauCeti.isIntegrallyClosedIn_of_constantCompositum_eq_top: for a separable constant field extension by a perfect k', in particular over a perfect k, k' is the exact constant field of F · k' (Stichtenoth, Proposition 3.6.1(a)).

Reference

H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.6, Proposition 3.6.1.

theorem TauCeti.finiteDimensional_of_constantCompositum_eq_top {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 k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional k k'] (h : constantCompositum F k' F' = ⊤) : FiniteDimensional F F'

A compositum with finite constants is finite over the original field. The ambient field F' is assumed to be precisely the compositum of F and k'.

theorem TauCeti.finiteDimensional_base_of_constantCompositum_eq_top {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 k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [FiniteDimensional F F'] [Algebra.IsSeparable k k'] (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) : FiniteDimensional k k'

Finiteness of the compositum detects finiteness of the constants: if k is exact in F, k' / k is separable and the compositum F · k' is finite over F, then k' / k is finite. This is the converse of TauCeti.finiteDimensional_of_constantCompositum_eq_top, by the degree identity [F · k' : F] = [k' : k] of linear disjointness.

theorem TauCeti.isSeparable_of_constantCompositum_eq_top {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 k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable k k'] (hcomp : constantCompositum F k' F' = ⊤) : Algebra.IsSeparable F F'

A separable extension of the constant field produces a separable compositum over the original field.

The constant field of the compositum

theorem TauCeti.separableClosure_eq_bot_of_constantCompositum_eq_top {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 k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable k k'] (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) : separableClosure k' F' = ⊥

The enlarged constant field is separably closed in the compositum: if k is the exact constant field of F and k' / k is separable algebraic, then every element of F · k' that is separable over k' is already a constant of k'.

This is Stichtenoth, Proposition 3.6.1(a), with perfectness of k replaced by the separability of the constant in question; TauCeti.isIntegrallyClosedIn_of_constantCompositum_eq_top recovers the statement of record over a perfect k.

theorem TauCeti.isIntegrallyClosedIn_of_constantCompositum_eq_top {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 k' F'] [Algebra F F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsSeparable k k'] [PerfectField k'] (hex : IsIntegrallyClosedIn k F) (h : constantCompositum F k' F' = ⊤) : IsIntegrallyClosedIn k' F'

The constant field of a constant field extension (Stichtenoth, Proposition 3.6.1(a)): if k is the exact constant field of F, k' / k is separable and k' is perfect, then the compositum F · k' has exact constant field k'. Stichtenoth's hypotheses — k perfect and k' / k algebraic — are the special case in which Algebra.IsSeparable k k' is inferred and PerfectField k' is Algebra.IsAlgebraic.perfectField k.

Together with TauCeti.IsFunctionField.of_constantCompositum_eq_top from ConstantExtension.Algebraic, this makes F · k' / k' a function field with exact constant field for an algebraic k' / k, so that its genus, its places and their degrees are the ones the theory of constant field extensions compares with those of F / k.

Large finite extensions of constants

theorem TauCeti.exists_finiteDimensional_lt_card_constantCompositum_eq_top (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] (n : ℕ) : ∃ (F' : IntermediateField F (AlgebraicClosure F)) (k' : IntermediateField k ↥F'), FiniteDimensional k ↥k' ∧ ↑n < ENat.card ↥k' ∧ constantCompositum F ↥k' ↥F' = ⊤

Large finite constant field extensions exist: for every n, there is a finite extension k' / k with more than n elements together with a field F', intermediate between F and its algebraic closure, which is the compositum F · k'. The elements of k' are chosen among the infinitely many elements of the algebraic closure of k in that of F.