The differential dx under a constant field extension

Let F' = F · k' be a finite separable constant field extension of an algebraic function field F / k, and let x be a separating element of F / k. Its image in F' is separating for F' / k'. This file proves that the cotrace from F to F' carries the Weil differential dx of F (TauCeti.weilDifferentialOfSeparating) to the Weil differential dx of F'. The key case is the rational function field: the cotrace from k(X) to k'(X) carries the canonical differential η of k(X) to that of k'(X).

Since the cotrace is injective and F-semilinear, identities between Weil differentials of F can be checked after a constant field extension, where more places are rational. This is how the chain rule dy = (dy/dx) · dx is proved over an arbitrary exact constant field (TauCeti.weilDifferentialOfSeparating_eq_derivativeOfSeparating_smul).

Main results

• TauCeti.weilDifferentialCotrace_ratFuncWeilDifferential: the cotrace from k(X) to k'(X) carries η to η'.
• TauCeti.weilDifferentialCotrace_weilDifferentialOfSeparating: the cotrace from F to F · k' carries dx to dx.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 1.7.4, Definition 3.4.5, Proposition 3.4.11 and Theorem 4.3.2.

The rational function field

theorem TauCeti.weilDifferentialCotrace_ratFuncWeilDifferential {k : Type u_1} {k' : Type u_2} [Field k] [Field k'] [Algebra k k'] [FiniteDimensional k k'] [Algebra.IsSeparable k k'] [Algebra (RatFunc k) (RatFunc k')] [IsScalarTower k (RatFunc k) (RatFunc k')] (hX : (algebraMap (RatFunc k) (RatFunc k')) RatFunc.X = RatFunc.X) : (weilDifferentialCotrace k' (RatFunc k') ⋯ ⋯) ⟨ratFuncWeilDifferential k, ⋯⟩ = ⟨ratFuncWeilDifferential k', ⋯⟩

The cotrace of η under a constant field extension is η: for a finite separable extension k' / k, the cotrace from k(X) to k'(X) carries the canonical Weil differential η of k(X) to that of k'(X).

Separating elements under a constant field extension

theorem TauCeti.weilDifferentialCotrace_weilDifferentialOfSeparating {k : Type u_1} {k' : Type u_2} {F : Type u_3} {F' : Type u_4} [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'] [Algebra.IsSeparable k k'] (h : constantCompositum F k' F' = ⊤) (hF : IsFunctionField k F) {x : F} (hx : Transcendental k x) [Algebra.IsSeparable (↥k⟮x⟯) F] : (weilDifferentialCotrace k' F' hF ⋯) (weilDifferentialOfSeparating hF hx) = weilDifferentialOfSeparating ⋯ ⋯

dx is stable under constant field extension: for a finite separable constant field extension F' = F · k' and a separating element x of F / k, whose image in F' is separating over k', the cotrace to F' of the Weil differential dx of F is the Weil differential dx of F'.