English
A restatement: if the extension is not separable, the trace vanishes.
Русский
Повторное утверждение: если расширение нераспадаемое, след обнулён.
LaTeX
$$Same content as 185528$$
Lean4
theorem trace_eq_sum_automorphisms (x : L) [FiniteDimensional K L] [IsGalois K L] :
algebraMap K L (Algebra.trace K L x) = ∑ σ : L ≃ₐ[K] L, σ x :=
by
apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)
rw [_root_.map_sum (algebraMap L (AlgebraicClosure L))]
rw [← Fintype.sum_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
· rw [← trace_eq_sum_embeddings (AlgebraicClosure L) (x := x)]
simp only [algebraMap_eq_smul_one, smul_one_smul]
· intro σ
simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk, AlgEquiv.coe_ofBijective,
AlgHom.restrictNormal_commutes, algebraMap_self, RingHom.id_apply]
