Sums of Galois automorphisms and the trace

Mathlib's trace_eq_sum_automorphisms writes the trace of a finite Galois extension as the sum of its automorphisms. This file records two consequences for a tower K ⊆ L ⊆ M.

Main results

• MonoidHom.sum_fiber_apply_eq_algebraMap_trace: for f : Gal(M/K) → Gal(L/K) compatible with the inclusion L ⊆ M, the automorphisms in the fibre of f over σ sum to σ ∘ Tr_{M/L}, because that fibre is a coset of Gal(M/L).
• Module.Basis.sum_traceDual_mul_apply: for an L-basis m of a finite Galois extension M/L with trace-dual basis m*, ∑ᵢ m*ᵢ · g(mᵢ) is 1 if g = 1 and 0 for every other g ∈ Gal(M/L), by Dedekind's independence of characters.

theorem MonoidHom.sum_fiber_apply_eq_algebraMap_trace {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [FiniteDimensional K M] [IsGalois K M] [DecidableEq Gal(L/K)] (f : Gal(M/K) →* Gal(L/K)) (hf : ∀ (g : Gal(M/K)) (x : L), (algebraMap L M) ((f g) x) = g ((algebraMap L M) x)) (σ : Gal(L/K)) (z : M) : ∑ g : Gal(M/K) with f g = σ, g z = (algebraMap L M) (σ ((Algebra.trace L M) z))

For a finite Galois extension M/K, an intermediate field L and a homomorphism f : Gal(M/K) → Gal(L/K) compatible with the inclusion L ⊆ M, the automorphisms in the fibre of f over σ sum to σ composed with the trace of M/L.

theorem Module.Basis.sum_traceDual_mul_apply {L : Type u_1} {M : Type u_2} [Field L] [Field M] [Algebra L M] [FiniteDimensional L M] [IsGalois L M] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (m : Basis ι L M) (g : Gal(M/L)) : ∑ i : ι, m.traceDual i * g (m i) = if g = 1 then 1 else 0

For an L-basis m of a finite Galois extension M/L and g ∈ Gal(M/L), the sum ∑ᵢ m*ᵢ · g(mᵢ) against the trace-dual basis is 1 if g = 1 and 0 otherwise. This is Dedekind's independence of characters applied to x = ∑ᵢ m*ᵢ · Tr(mᵢ x) = ∑_g (∑ᵢ m*ᵢ · g(mᵢ)) · g(x).