The constant field of an algebraic function field

The field of constants of an algebraic function field F / k is the relative algebraic closure algebraicClosure k F of k in F: the elements of F that are algebraic over k. This file proves that it is a finite extension of k, records the dictionary for the hypothesis that it is no larger than k (the literature's "k is the full field of constants"), and shows that replacing k by the field of constants normalizes any function field to one whose field of constants is exact.

It then follows the field of constants along a change of the base field. An intermediate base field k' of F / k — one over which F is again a function field, which by TauCeti.isFunctionField_base_iff_isAlgebraic means exactly that k' / k is algebraic — is automatically finite over k, and as soon as k' is its own field of constants it is the field of constants of F / k. In the tower of an extension F' / k' of F / k, the field of constants of F' / k' cuts down along F ⊆ F' to the field of constants of F / k; when both bases are exact this says that k' ∩ F = k, so the tower map k → k' is the induced inclusion of the two fields of constants. The base extension k' / k is always algebraic, and finite once F' / F is — a theorem, not a hypothesis, and the finiteness that makes the factor [k' : k] in the conorm degree identity and in the Hurwitz genus formula meaningful.

Main results

• TauCeti.IsFunctionField.finiteDimensional_of_isAlgebraic: an intermediate extension of a function field F / k which is algebraic over k is finite over k.
• TauCeti.IsFunctionField.finiteDimensional_algebraicClosure: the field of constants of a function field is finite over the base field.
• TauCeti.algebraicClosure_eq_bot_iff_isIntegrallyClosedIn, TauCeti.isIntegrallyClosedIn_iff_forall_isAlgebraic, TauCeti.isIntegrallyClosedIn_iff_finrank_algebraicClosure_eq_one: the three faces of the exactness hypothesis on the field of constants.
• TauCeti.IsFunctionField.algebraicClosure and TauCeti.isIntegrallyClosedIn_algebraicClosure: F is a function field over its field of constants, and there the field of constants is exact; the two are packaged as TauCeti.IsFunctionField.exists_intermediateField_isIntegrallyClosedIn.
• TauCeti.IsFunctionField.finiteDimensional_base and TauCeti.IsFunctionField.algebraicClosure_eq_restrictScalars_bot: an intermediate base field of F / k is finite over k, and is the field of constants of F / k as soon as it is its own; TauCeti.IsFunctionField.isAlgebraic_iff_mem_range_algebraMap is the elementwise form.
• TauCeti.IsFunctionField.isAlgebraic_baseExtension and TauCeti.IsFunctionField.finiteDimensional_baseExtension: in an extension F' / k' of F / k, the base extension k' / k is algebraic, and finite once F' / F is (Stichtenoth, Definition 3.1.1).
• TauCeti.IsFunctionField.isAlgebraic_algebraMap_iff_isAlgebraic: the field of constants of F' / k' cuts down along F ⊆ F' to the field of constants of F / k; for exact bases TauCeti.IsFunctionField.algebraMap_mem_range_algebraMap_iff reads this as k' ∩ F = k.
• TauCeti.algebraicClosure_ratFunc: k is the field of constants of k(x).

References

The statements follow Stichtenoth, Algebraic Function Fields and Codes, second edition: Corollary 1.1.16 for the finiteness of the field of constants, the standing hypothesis of Section 1.4 for its exactness, Proposition 1.2.1(d) for the rational function field, and Definition 3.1.1 for an extension of function fields.

Finiteness of the field of constants

theorem TauCeti.IsFunctionField.finiteDimensional_of_isAlgebraic {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (E : Type u_1) [Field E] [Algebra k E] [Algebra E F] [IsScalarTower k E F] [Algebra.IsAlgebraic k E] : FiniteDimensional k E

An intermediate extension of an algebraic function field F / k which is algebraic over k is a finite extension of k (Stichtenoth, Corollary 1.1.16).

theorem TauCeti.IsFunctionField.finiteDimensional_algebraicClosure {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : FiniteDimensional k ↥(_root_.algebraicClosure k F)

The field of constants of an algebraic function field is a finite extension of the base field (Stichtenoth, Corollary 1.1.16).

Exactness of the field of constants

theorem TauCeti.algebraicClosure_eq_bot_iff_isIntegrallyClosedIn {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] : algebraicClosure k F = ⊥ ↔ IsIntegrallyClosedIn k F

k is integrally closed in F exactly when no element of F outside k is algebraic over k, that is, when the field of constants of F / k is k itself.

theorem TauCeti.isIntegrallyClosedIn_iff_forall_isAlgebraic {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] : IsIntegrallyClosedIn k F ↔ ∀ (x : F), IsAlgebraic k x → ∃ (c : k), (algebraMap k F) c = x

The elementwise form of the exactness hypothesis on the field of constants: every element of F algebraic over k is already a constant. This is the field-extension reading of Mathlib's isIntegrallyClosedIn_iff, whose injectivity clause is automatic here.

theorem TauCeti.isIntegrallyClosedIn_iff_finrank_algebraicClosure_eq_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] : IsIntegrallyClosedIn k F ↔ Module.finrank k ↥(algebraicClosure k F) = 1

The exactness hypothesis on the field of constants, read off its degree.

instance TauCeti.isIntegrallyClosedIn_algebraicClosure {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] : IsIntegrallyClosedIn (↥(algebraicClosure k F)) F

The field of constants is exact in itself: nothing in F outside algebraicClosure k F is algebraic over algebraicClosure k F.

The normalization device

theorem TauCeti.IsFunctionField.algebraicClosure {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : IsFunctionField (↥(_root_.algebraicClosure k F)) F

An algebraic function field is a function field over its own field of constants, and by TauCeti.isIntegrallyClosedIn_algebraicClosure the field of constants is exact there.

This is the device that lets a statement needing an exact field of constants be applied to an arbitrary function field.

theorem TauCeti.IsFunctionField.exists_intermediateField_isIntegrallyClosedIn {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : ∃ (k' : IntermediateField k F), FiniteDimensional k ↥k' ∧ IsFunctionField (↥k') F ∧ IsIntegrallyClosedIn (↥k') F

The normalization device: every algebraic function field is, over a finite extension of its base field, an algebraic function field with an exact field of constants. Results stated under the exactness hypothesis can therefore be applied to a general function field through this.

Intermediate base fields

theorem TauCeti.IsFunctionField.finiteDimensional_base {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {k' : Type u_1} [Field k'] [Algebra k k'] [Algebra k' F] [IsScalarTower k k' F] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F) : FiniteDimensional k k'

An intermediate base field of an algebraic function field is a finite extension of the original base field (Stichtenoth, Corollary 1.1.16).

theorem TauCeti.IsFunctionField.algebraicClosure_eq_restrictScalars_bot {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {k' : Type u_1} [Field k'] [Algebra k k'] [Algebra k' F] [IsScalarTower k k' F] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F) (hex : IsIntegrallyClosedIn k' F) : _root_.algebraicClosure k F = IntermediateField.restrictScalars k ⊥

The field of constants of F / k is the intermediate base field k', whenever k' is its own field of constants in F.

theorem TauCeti.IsFunctionField.isAlgebraic_iff_mem_range_algebraMap {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {k' : Type u_1} [Field k'] [Algebra k k'] [Algebra k' F] [IsScalarTower k k' F] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F) (hex : IsIntegrallyClosedIn k' F) {x : F} : IsAlgebraic k x ↔ x ∈ Set.range ⇑(algebraMap k' F)

The elementwise form of TauCeti.IsFunctionField.algebraicClosure_eq_restrictScalars_bot: an element of F is algebraic over k exactly when it is one of the constants k'.

Extensions of function fields

theorem TauCeti.IsFunctionField.isAlgebraic_algebraMap_iff_isAlgebraic {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {k' : Type u_1} {F' : Type u_2} [Field k'] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsAlgebraic F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') {a : F} : IsAlgebraic k' ((algebraMap F F') a) ↔ IsAlgebraic k a

The field of constants of F' / k' cuts down along F ⊆ F' to the field of constants of F / k: a function of F is algebraic over k' exactly when it is algebraic over k. The bases need not be exact, since either field of constants is a relative algebraic closure and not a base field.

theorem TauCeti.IsFunctionField.algebraMap_mem_range_algebraMap_iff {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {k' : Type u_1} {F' : Type u_2} [Field k'] [Field F'] [Algebra k k'] [Algebra k' F'] [Algebra F F'] [Algebra k F'] [IsScalarTower k k' F'] [IsScalarTower k F F'] [Algebra.IsAlgebraic F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') (hk : IsIntegrallyClosedIn k F) (hk' : IsIntegrallyClosedIn k' F') {a : F} : (algebraMap F F') a ∈ Set.range ⇑(algebraMap k' F') ↔ a ∈ Set.range ⇑(algebraMap k F)

The fields of constants of an extension of function fields are identified along the tower map k → k' (Stichtenoth, Definition 3.1.1 and the remark following it). Once k is the full field of constants of F / k and k' the full field of constants of F' / k', a function of F is a constant of F' / k' exactly when it is already a constant of F / k: inside F' the two fields of constants meet in k, so k → k' is the induced inclusion of fields of constants.

theorem TauCeti.IsFunctionField.finiteDimensional_baseExtension {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {k' : Type u_1} {F' : Type u_2} [Field k'] [Field F'] [Algebra k k'] [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') : FiniteDimensional k k'

The base field of an extension of function fields is a finite extension of the base field below (Stichtenoth, Corollary 1.1.16 applied in the tower of Definition 3.1.1). This is the finiteness that makes the factor [k' : k] of the conorm degree identity and of the Hurwitz genus formula meaningful.

Unlike TauCeti.IsFunctionField.isAlgebraic_baseExtension, this does need F' / F to be finite and not merely algebraic: for an algebraic closure k' of a finite field k, the extension k'(x) / k(x) is algebraic while k' / k is infinite.

The rational function field

theorem TauCeti.algebraicClosure_ratFunc (K : Type u_1) [Field K] : algebraicClosure K (RatFunc K) = ⊥

The field of constants of the rational function field k(x) is k (Stichtenoth, Proposition 1.2.1(d)).

instance TauCeti.isIntegrallyClosedIn_ratFunc {k : Type u} [Field k] : IsIntegrallyClosedIn k (RatFunc k)

k is integrally closed in the rational function field k(x).

theorem TauCeti.isIntegrallyClosedIn_intermediateField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hex : IsIntegrallyClosedIn k F) (E : IntermediateField k F) : IsIntegrallyClosedIn k ↥E

Exactness passes to intermediate fields: if k is integrally closed in F, it is integrally closed in every intermediate field of F / k.