English
An explicit formula for the trace map: for x ∈ L, algebraMap K L (trace_K L(x)) = ∑ i in range(rank_K L) x^{(|K|)^{i}}.
Русский
Явная формула следа: для x ∈ L, отображение алгебраMap от trace_K L(x) равно сумме по i до rank_K L: x^{(|K|)^i}.
LaTeX
$$$$ \\mathrm{algebraMap}(K,L)(\\mathrm{trace}(K,L,x)) = \\sum_{i=0}^{\\mathrm{finrank}_K L - 1} x^{(|K|)^i}. $$$$
Lean4
/-- An explicit formula for the trace map: `trace[L/K](x) = ∑ i < [L:K], x ^ ((#K) ^ i)`. -/
theorem algebraMap_trace_eq_sum_pow :
algebraMap K L (Algebra.trace K L x) = ∑ i ∈ Finset.range (Module.finrank K L), x ^ (Nat.card K ^ i) :=
by
have := Finite.of_injective _ (FaithfulSMul.algebraMap_injective K L)
have := ofFinite K
rw [trace_eq_sum_automorphisms, Finset.sum_range]
exact
Eq.symm <|
sum_bijective _ (bijective_frobeniusAlgEquivOfAlgebraic_pow K L) _ _ <| fun i ↦ by
rw [AlgEquiv.coe_pow, coe_frobeniusAlgEquivOfAlgebraic_iterate, card_eq_nat_card]
