Algebraic function fields of one variable

This file defines an algebraic function field intrinsically: no rational parameter is chosen. It proves that every transcendental element is a valid parameter and generates a function field of its own, compares the intrinsic notion with Mathlib's chosen-parameter FunctionField, and characterizes it by finite generation and transcendence degree one.

It then records how the notion behaves along a change of the field on either side: a finite extension of F is again a function field over k, an algebraic descent F / E preserves transcendence degree one and makes E a function field over k, and an intermediate field k' of F / k is a legitimate base for F exactly when k' / k is algebraic (TauCeti.isFunctionField_base_iff_isAlgebraic).

The definition and the independence-of-parameter result follow Stichtenoth, Algebraic Function Fields and Codes, second edition, Definition 1.1.1 and Remark 1.1.2.

def TauCeti.IsFunctionField (k : Type u) (F : Type v) [Field k] [Field F] [Algebra k F] : Prop

A field F is an algebraic function field of one variable over k if it is finite over k(x) for some element x transcendental over k.

Unlike Mathlib's FunctionField, this proposition does not depend on a chosen embedding of the rational function field. It is intentionally an explicit proposition rather than a typeclass.

Equations

• TauCeti.IsFunctionField k F = ∃ (x : F), Transcendental k x ∧ FiniteDimensional (↥k⟮x⟯) F

theorem TauCeti.IsFunctionField.exists_transcendental {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : ∃ (x : F), Transcendental k x

An algebraic function field contains an element transcendental over its base field.

theorem TauCeti.IsFunctionField.finiteDimensional_adjoin {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {y : F} (hy : Transcendental k y) : FiniteDimensional (↥k⟮y⟯) F

Every transcendental element of an algebraic function field is a rational parameter: the field is finite over the intermediate field it generates.

theorem TauCeti.IsFunctionField.essFiniteType {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : Algebra.EssFiniteType k F

An algebraic function field is finitely generated as a field extension.

theorem TauCeti.IsFunctionField.trdeg_eq_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) : Algebra.trdeg k F = 1

An algebraic function field has transcendence degree one.

theorem TauCeti.IsFunctionField.ratFunc (k : Type u) [Field k] : IsFunctionField k (RatFunc k)

The rational function field is an algebraic function field over its coefficient field.

theorem Transcendental.isFunctionField_adjoin {k : Type u} [Field k] {E : Type u_1} [Field E] [Algebra k E] {α : E} (hα : Transcendental k α) : TauCeti.IsFunctionField k ↥k⟮α⟯

The field k(α) generated by an element α transcendental over k is an algebraic function field over k: it is the rational function field in α, presented inside an ambient field.

theorem TauCeti.isFunctionField_iff_functionField {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra (RatFunc k) F] [IsScalarTower k (RatFunc k) F] : IsFunctionField k F ↔ FunctionField k F

With a chosen embedding of the rational function field, the intrinsic predicate agrees with Mathlib's FunctionField.

theorem TauCeti.isFunctionField_iff_trdeg_eq_one {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] [Algebra.EssFiniteType k F] : IsFunctionField k F ↔ Algebra.trdeg k F = 1

For a finitely generated field extension, being an algebraic function field is equivalent to having transcendence degree one.

theorem TauCeti.IsFunctionField.trdeg_eq_one_of_isAlgebraic {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {E : Type u_1} [Field E] [Algebra k E] [Algebra F E] [IsScalarTower k F E] [Algebra.IsAlgebraic F E] (hF : IsFunctionField k F) : Algebra.trdeg k E = 1

An algebraic extension of an algebraic function field still has transcendence degree one over the base field, whether or not it is again finitely generated.

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

A finite extension of an algebraic function field is an algebraic function field over the same base field. No separability hypothesis is needed.

theorem TauCeti.IsFunctionField.trdeg_eq_one_of_isAlgebraic_top {k : Type u} {F : Type v} [Field k] [Field F] [Algebra k F] {E : Type w} [CommRing E] [Algebra k E] [Algebra E F] [IsScalarTower k E F] [FaithfulSMul E F] [Algebra.IsAlgebraic E F] (hF : IsFunctionField k F) : Algebra.trdeg k E = 1

If F / k is a function field and F is algebraic over an embedded commutative k-algebra E, then E / k has transcendence degree one. The algebra E need not be a field.

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

If F / k is a function field and F / E is algebraic, then E / k is a function field. A transcendental element of E is a rational parameter for both F and E.

Change of base field

theorem TauCeti.IsFunctionField.isAlgebraic_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) : Algebra.IsAlgebraic k k'

An intermediate field k' between k and an algebraic function field F / k over which F is again an algebraic function field is algebraic over k.

theorem TauCeti.IsFunctionField.of_isAlgebraic {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) [Algebra.IsAlgebraic k k'] : IsFunctionField k' F

Enlarging the base field of an algebraic function field by an algebraic extension inside it leaves an algebraic function field (Stichtenoth, Corollary 1.1.16 and Definition 3.1.1): the new base contributes no transcendence.

theorem TauCeti.IsFunctionField.of_finiteDimensional {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) [FiniteDimensional k k'] : IsFunctionField k F

Shrinking the base field of an algebraic function field along a finite extension leaves an algebraic function field: if F is a function field over k' and k' is finite over k, then F is a function field over k. This is the converse of TauCeti.IsFunctionField.of_isAlgebraic for the finite extensions that TauCeti.IsFunctionField.finiteDimensional_base produces.

theorem TauCeti.isFunctionField_base_iff_isAlgebraic {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) : IsFunctionField k' F ↔ Algebra.IsAlgebraic k k'

An intermediate field of an algebraic function field F / k is a legitimate base field for F exactly when it is algebraic over k.

Extensions of function fields

theorem TauCeti.IsFunctionField.isAlgebraic_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'] [Algebra.IsAlgebraic F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k' F') : Algebra.IsAlgebraic k k'

The base field of an extension of function fields is algebraic over the base field below (Stichtenoth, Definition 3.1.1 and the remark following it): in the tower of an extension F' / k' of F / k with F' / F algebraic, the algebraicity of k' / k is not an assumption but a theorem.