Linear forms over a separable extension, through the trace

Let L / K be a finite separable field extension and V a vector space over L. Composing an L-linear form on V with the trace Tr_{L/K} : L → K gives a K-linear form on V, and every K-linear form on V arises this way from exactly one L-linear form. This is the nondegeneracy of the trace form, traceForm_nondegenerate, applied pointwise: the L-linear form attached to μ sends v to the element of L which the trace form pairs with b ↦ μ (b • v).

This is how Weil differentials of a function field are transported along an extension of the constant field: they are linear forms over the constant field, and the trace form of the constant-field extension converts linear forms over the larger constant field to linear forms over the smaller one.

Main definitions

• Module.Dual.traceCompEquiv: the K-linear equivalence Module.Dual L V ≃ₗ[K] Module.Dual K V, φ ↦ Tr_{L/K} ∘ φ.

Main results

• Module.Dual.traceCompEquiv_apply: the equivalence composes with the trace.
• Module.Dual.apply_eq_zero_iff_forall_trace_eq_zero: an L-linear form vanishes at v exactly when the traces of its values on the L-line through v all vanish.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, proof of Theorem 3.4.6, where this identification converts the trace of a Weil differential into a Weil differential over the larger constant field.

noncomputable def Module.Dual.traceCompEquiv (K : Type u_1) (L : Type u_2) (V : Type u_3) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] : Dual L V ≃ₗ[K] Dual K V

Linear forms over a finite separable extension, through the trace: composition with Tr_{L/K} identifies the L-linear forms on an L-vector space with its K-linear forms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.Dual.traceCompEquiv_apply {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] (φ : Dual L V) (v : V) : ((traceCompEquiv K L V) φ) v = (Algebra.trace K L) (φ v)

The equivalence traceCompEquiv composes a linear form with the trace.

@[simp]

theorem Module.Dual.trace_traceCompEquiv_symm_apply {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] (μ : Dual K V) (v : V) : (Algebra.trace K L) (((traceCompEquiv K L V).symm μ) v) = μ v

The L-linear form attached to a K-linear form μ has trace μ.

theorem Module.Dual.apply_eq_zero_iff_forall_trace_eq_zero {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [AddCommGroup V] [Module L V] (φ : Dual L V) (v : V) : φ v = 0 ↔ ∀ (b : L), (Algebra.trace K L) (φ (b • v)) = 0

An L-linear form vanishes at v exactly when the traces of its values at the multiples b • v all vanish.