Bases of constants in a constant field extension

Let F' = F · k' be the compositum of a field F with a separable extension k' of a field k that is relatively algebraically closed in F; the case of interest is a constant field extension of an algebraic function field F / k with exact constant field k. Linear disjointness of F and k' over k makes F' behave like F ⊗[k] k': the image in F' of a k-basis of k' is an F-basis of F', the coordinates of a constant in this basis are the images of its coordinates over k, the trace from F' to F of a constant is the image of its trace from k' to k, and the trace dual of a basis of constants is the basis of constants attached to the trace dual over k.

These are the linear-algebraic inputs to the local theory of constant field extensions: at every place P of F / k a basis of constants is an integral basis, which is what identifies the functions of F' = F · k' with bounded poles in terms of those of F.

Main definitions and results

• TauCeti.constantBasis: the F-basis of F' = F · k' given by a k-basis of k'.
• TauCeti.constantBasis_repr_algebraMap: the coordinates of a constant in a basis of constants are the images of its coordinates over k.
• TauCeti.trace_algebraMap_of_constantCompositum_eq_top: the trace of a constant is the image of its trace over k. This is Mathlib's Subalgebra.LinearDisjoint.trace_algebraMap for the linearly disjoint pair F, k', stated for the trace over the field F itself rather than over its image in F'.
• TauCeti.traceDual_constantBasis: the trace dual of a basis of constants.

Reference

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

theorem TauCeti.adjoin_range_algebraMap_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.IsIntegral k k'] (h : constantCompositum F k' F' = ⊤) : Algebra.adjoin F (Set.range ⇑(algebraMap k' F')) = ⊤

The constants generate the compositum F · k' as an F-algebra: for an algebraic extension of constants, the intermediate field they generate is already the subalgebra they generate.

theorem TauCeti.span_range_algebraMap_comp_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.IsIntegral k k'] (h : constantCompositum F k' F' = ⊤) {ι : Type u_1} (b : Module.Basis ι k k') : Submodule.span F (Set.range (⇑(algebraMap k' F') ∘ ⇑b)) = ⊤

The image of a k-basis of k' spans the compositum F' = F · k' over F, for an algebraic extension of constants.

noncomputable def TauCeti.constantBasis {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' = ⊤) {ι : Type u_1} (b : Module.Basis ι k k') : Module.Basis ι F F'

A basis of constants: the F-basis of the compositum F' = F · k' given by the image of a k-basis of k'. Linear independence is the linear disjointness of F and k' over k (Stichtenoth, Proposition 3.6.1(b)), which needs k exact in F and k' / k separable; spanning is the definition of the compositum.

Equations

• TauCeti.constantBasis hex h b = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.constantBasis_apply {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' = ⊤) {ι : Type u_1} (b : Module.Basis ι k k') (i : ι) : (constantBasis hex h b) i = (algebraMap k' F') (b i)

theorem TauCeti.coe_constantBasis {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' = ⊤) {ι : Type u_1} (b : Module.Basis ι k k') : ⇑(constantBasis hex h b) = ⇑(algebraMap k' F') ∘ ⇑b

@[simp]

theorem TauCeti.constantBasis_repr_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 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' = ⊤) {ι : Type u_1} (b : Module.Basis ι k k') (c : k') (i : ι) : ((constantBasis hex h b).repr ((algebraMap k' F') c)) i = (algebraMap k F) ((b.repr c) i)

The coordinates of a constant in a basis of constants are the images of its coordinates over k.

theorem TauCeti.trace_algebraMap_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' = ⊤) [FiniteDimensional k k'] (c : k') : (Algebra.trace F F') ((algebraMap k' F') c) = (algebraMap k F) ((Algebra.trace k k') c)

The trace of a constant is a constant: for a finite separable extension of constants, the trace from F' = F · k' to F of a constant is the image of its trace from k' to k.

This is not a simp lemma: the base field k does not occur in the left-hand side, so simp cannot infer it (the simpNF linter rejects the lemma); use rw.

@[simp]

theorem TauCeti.traceDual_constantBasis {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' = ⊤) [FiniteDimensional k k'] [FiniteDimensional F F'] [Algebra.IsSeparable F F'] {ι : Type u_1} [Finite ι] [DecidableEq ι] (b : Module.Basis ι k k') : (constantBasis hex h b).traceDual = constantBasis hex h b.traceDual

The trace dual of a basis of constants is the basis of constants attached to the trace dual over k: the trace form of F' / F restricts on constants to the trace form of k' / k.