Local integral bases of extensions of algebraic function fields

Let F' / F be a finite separable extension and let P be a place of F / k. Its local integral closure

𝒪'_P = integralClosure 𝒪_P F'

is a finite free module over the discrete valuation ring 𝒪_P, of rank [F' : F]. Choosing a basis of that module and extending scalars from 𝒪_P to its fraction field F gives a basis of F' / F consisting of elements integral over 𝒪_P. This is the local integral basis of Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Corollary 3.3.5.

The local model 𝒪_P ⊆ 𝒪'_P and its fraction-field, localization, Dedekind, finiteness, and separability infrastructure are supplied by TauCeti/FieldTheory/FunctionField/Place/Extension/Basic.lean.

The freeness and rank calculation are specializations of Mathlib's generic integral-closure theorems IsIntegralClosure.module_free and IsIntegralClosure.rank. The point of this file is the function-field interface: the basis is indexed by Fin [F' : F], its vectors are visibly integral, and their 𝒪_P-span inside F' is exactly 𝒪'_P. These are the forms used by the subsequent constructions of the complementary module and different.

The basis material is the place-local analogue of Mathlib's NumberField.integralBasis API in Mathlib.NumberTheory.NumberField.Basic, and is built the same way: TauCeti.Place.finrank_integralClosure matches NumberField.RingOfIntegers.rank, TauCeti.Place.localIntegralBasis matches NumberField.integralBasis, TauCeti.Place.localIntegralBasis_apply and TauCeti.Place.localIntegralBasis_repr_algebraMap match NumberField.integralBasis_apply and NumberField.integralBasis_repr_apply, and TauCeti.Place.isIntegralBasis_localizationLocalization plays the role of NumberField.mem_span_integralBasis.

Main definitions

• TauCeti.Place.IsIntegralBasis: the property that an F-basis of F' is an integral basis at P.
• TauCeti.Place.integralClosureFinBasis: an 𝒪_P-basis of 𝒪'_P, indexed by Fin [F' : F].
• TauCeti.Place.localIntegralBasis: the resulting F-basis of F'.

Main results

• TauCeti.Place.IsIntegralBasis.isIntegral and TauCeti.Place.IsIntegralBasis.mem_span_iff_isIntegral: what an integral basis at P gives — integral vectors, and an integral span that detects integrality.
• TauCeti.Place.isIntegralBasis_iff_isIntegral_iff_repr_mem: an arbitrary basis is integral exactly when integrality is detected coordinatewise over 𝒪_P.
• TauCeti.Place.IsIntegralBasis.of_isIntegral_of_isIntegral_traceDual: a basis and its trace dual being integral at a place is sufficient for the basis to be an integral basis there.
• TauCeti.Place.finrank_integralClosure: rank_{𝒪_P} 𝒪'_P = [F' : F].
• TauCeti.Place.isIntegralBasis_localizationLocalization: extending any 𝒪_P-basis of 𝒪'_P to the fraction fields gives an integral basis at P.
• TauCeti.Place.isIntegralBasis_localIntegralBasis: the chosen basis TauCeti.Place.localIntegralBasis is one; this is the existence statement of Stichtenoth, Corollary 3.3.5.
• TauCeti.Place.localIntegralBasis_repr_algebraMap: the coordinates of an integral element in the local integral basis are the images of its coordinates in the 𝒪_P-basis of 𝒪'_P.
• TauCeti.Place.isIntegral_iff_repr_mem: an element of F' is integral over 𝒪_P exactly when all its coordinates in the local integral basis lie in 𝒪_P.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Corollary 3.3.5.

Integral bases at a place

def TauCeti.Place.IsIntegralBasis {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) {ι : Type u_1} (b : Module.Basis ι F F') : Prop

An F-basis of F' is an integral basis at P when its 𝒪_P-span is exactly the integral closure 𝒪'_P inside F' (Stichtenoth, Section III.3).

Equations

• TauCeti.Place.IsIntegralBasis F' P b = (Submodule.span (↥P.integers) (Set.range ⇑b) = Subalgebra.toSubmodule (integralClosure (↥P.integers) F'))

theorem TauCeti.Place.isIntegralBasis_iff_isIntegral_iff_repr_mem {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) {ι : Type u_1} (b : Module.Basis ι F F') : IsIntegralBasis F' P b ↔ ∀ (x : F'), IsIntegral (↥P.integers) x ↔ ∀ (i : ι), (b.repr x) i ∈ P.integers

A basis is an integral basis at P exactly when integrality over 𝒪_P is equivalent to all of its coordinates lying in 𝒪_P.

theorem TauCeti.Place.IsIntegralBasis.isIntegral {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) {ι : Type u_1} {b : Module.Basis ι F F'} (hb : IsIntegralBasis F' P b) (i : ι) : IsIntegral (↥P.integers) (b i)

Every vector of an integral basis at P is integral over 𝒪_P.

theorem TauCeti.Place.IsIntegralBasis.mem_span_iff_isIntegral {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) {ι : Type u_1} {b : Module.Basis ι F F'} (hb : IsIntegralBasis F' P b) {x : F'} : x ∈ Submodule.span (↥P.integers) (Set.range ⇑b) ↔ IsIntegral (↥P.integers) x

Membership in the integral span of an integral basis at P is the same as integrality over 𝒪_P.

theorem TauCeti.Place.IsIntegralBasis.isIntegral_iff_repr_mem {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) {ι : Type u_1} {b : Module.Basis ι F F'} (hb : IsIntegralBasis F' P b) {x : F'} : IsIntegral (↥P.integers) x ↔ ∀ (i : ι), (b.repr x) i ∈ P.integers

Integrality over 𝒪_P, expressed in the coordinate normal form supplied by an integral basis at P.

theorem TauCeti.Place.IsIntegralBasis.of_isIntegral_of_isIntegral_traceDual {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] {ι : Type u_1} [Finite ι] [DecidableEq ι] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (P : Place k F) (b : Module.Basis ι F F') (hb : ∀ (i : ι), IsIntegral (↥P.integers) (b i)) (hbdual : ∀ (i : ι), IsIntegral (↥P.integers) (b.traceDual i)) : IsIntegralBasis F' P b

If an F-basis of F' and its trace-dual basis are integral over 𝒪_P, then the basis is an integral basis at P.

The local integral closure

theorem TauCeti.Place.isIntegralBasis_localizationLocalization {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure (↥P.integers) F')) (nonZeroDivisors ↥P.integers)) F'] {ι : Type u_1} (c : Module.Basis ι ↥P.integers ↥(integralClosure (↥P.integers) F')) : IsIntegralBasis F' P (Module.Basis.localizationLocalization F (nonZeroDivisors ↥P.integers) F' c)

Extending any 𝒪_P-basis of the local integral closure 𝒪'_P to the fraction fields gives an integral basis at P. This is Stichtenoth, Corollary 3.3.5.

theorem TauCeti.Place.finrank_integralClosure {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] : Module.finrank ↥P.integers ↥(integralClosure (↥P.integers) F') = Module.finrank F F'

The rank of the local integral closure is the degree of the field extension: rank_{𝒪_P} 𝒪'_P = [F' : F].

A local integral basis

noncomputable def TauCeti.Place.integralClosureFinBasis {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] : Module.Basis (Fin (Module.finrank F F')) ↥P.integers ↥(integralClosure (↥P.integers) F')

An 𝒪_P-basis of the local integral closure 𝒪'_P, indexed by the degree [F' : F].

Equations

• TauCeti.Place.integralClosureFinBasis F' P = Module.finBasisOfFinrankEq ↥P.integers ↥(integralClosure (↥P.integers) F') ⋯

noncomputable def TauCeti.Place.localIntegralBasis {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] : Module.Basis (Fin (Module.finrank F F')) F F'

A local integral basis at P (Stichtenoth, Corollary 3.3.5): extend an 𝒪_P-basis of the local integral closure 𝒪'_P to the fraction fields. The resulting F-basis of F' is indexed by Fin [F' : F], and its 𝒪_P-span is exactly 𝒪'_P.

Equations

• TauCeti.Place.localIntegralBasis F' P = Module.Basis.localizationLocalization F (nonZeroDivisors ↥P.integers) F' (TauCeti.Place.integralClosureFinBasis F' P)

@[simp]

theorem TauCeti.Place.localIntegralBasis_apply {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (i : Fin (Module.finrank F F')) : (localIntegralBasis F' P) i = (algebraMap (↥(integralClosure (↥P.integers) F')) F') ((integralClosureFinBasis F' P) i)

A vector of the local integral basis is the image in F' of the corresponding vector of the 𝒪_P-basis of 𝒪'_P.

@[simp]

theorem TauCeti.Place.localIntegralBasis_repr_algebraMap {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] (x : ↥(integralClosure (↥P.integers) F')) (i : Fin (Module.finrank F F')) : ((localIntegralBasis F' P).repr ↑x) i = (algebraMap (↥P.integers) F) (((integralClosureFinBasis F' P).repr x) i)

The coordinates of an integral element in the local integral basis are the images in F of its coordinates in the 𝒪_P-basis of 𝒪'_P.

theorem TauCeti.Place.isIntegralBasis_localIntegralBasis {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] : IsIntegralBasis F' P (localIntegralBasis F' P)

The chosen localIntegralBasis is an integral basis at P: its 𝒪_P-span is exactly the local integral closure 𝒪'_P. This is the existence statement of Stichtenoth, Corollary 3.3.5.

@[simp]

theorem TauCeti.Place.isIntegral_iff_repr_mem {k : Type u} {F : Type v} (F' : Type v') [Field k] [Field F] [Field F'] [Algebra k F] [Algebra F F'] (P : Place k F) [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {x : F'} : IsIntegral (↥P.integers) x ↔ ∀ (i : Fin (Module.finrank F F')), ((localIntegralBasis F' P).repr x) i ∈ P.integers

An element of F' is integral over 𝒪_P exactly when all of its coordinates in the local integral basis lie in 𝒪_P (Stichtenoth, Corollary 3.3.5).