Trace-dual families of a projective extension

Let A be a domain with fraction field K, let L / K be a finite separable extension, and let B be the integral closure of A in L. Every A-linear form B → A is the restriction of a trace pairing x ↦ Tr_{L/K}(y x), and the element y then lies in the trace dual Bᵛ = {y ∈ L | Tr_{L/K}(y B) ⊆ A}.

When B is moreover a finite projective A-module, as it is over a Dedekind domain, there is a finite trace-dual family bᵢ ∈ B and yᵢ ∈ Bᵛ satisfying

x = ∑ᵢ Tr_{L/K}(x bᵢ) yᵢ for every x ∈ L.

This identity is used to compare trace duals after extending scalars, in particular when comparing a number-field different with the different of a completed extension.

Main results

• TauCeti.exists_trace_mul_algebraMap_eq: every A-linear form on B is a trace pairing.
• TauCeti.exists_sum_trace_mul_smul_eq: a projective integral closure has a finite trace-dual family (bᵢ, yᵢ) with bᵢ ∈ B, yᵢ ∈ Bᵛ and x = ∑ᵢ Tr(x bᵢ) yᵢ.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter III, §2.

theorem TauCeti.exists_trace_mul_algebraMap_eq {A : Type u_1} (K : Type u_2) {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] (f : B →ₗ[A] A) : ∃ (y : L), ∀ (x : B), (Algebra.trace K L) (y * (algebraMap B L) x) = (algebraMap A K) (f x)

Linear forms are trace pairings. Every A-linear form f : B → A on the integral closure of A in a finite separable extension L / K is x ↦ Tr_{L/K}(y x) for some y ∈ L.

theorem TauCeti.exists_sum_trace_mul_smul_eq (A : Type u_1) (K : Type u_2) {L : Type u_3} {B : Type u_4} [CommRing A] [Field K] [CommRing B] [Field L] [Algebra A K] [Algebra B L] [Algebra A B] [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsDomain A] [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [Module.Finite A B] [Module.Projective A B] : ∃ (n : ℕ) (b : Fin n → B) (y : Fin n → L), (∀ (i : Fin n), y i ∈ Submodule.traceDual A K 1) ∧ ∀ (x : L), ∑ i : Fin n, (Algebra.trace K L) (x * (algebraMap B L) (b i)) • y i = x

A finite trace-dual family. If the integral closure B of A in a finite separable extension L / K is a finite projective A-module, there are finitely many bᵢ ∈ B and yᵢ ∈ Bᵛ such that x = ∑ᵢ Tr_{L/K}(x bᵢ) yᵢ for every x ∈ L.