English
Under finiteness and separability, the trace map is surjective.
Русский
При конечности и разделяемости следовая карта сюрьективна.
LaTeX
$$$\\operatorname{trace}: L \\to K \\text{ is surjective}$$$
Lean4
/-- If `x` is in the base field `K`, then the trace is `[L : K] * x`.
(If `L` is not finite-dimensional over `K`, then `trace` and `finrank` return `0`.)
-/
@[simp]
theorem trace_algebraMap [StrongRankCondition R] [Module.Free R S] (x : R) :
trace R S (algebraMap R S x) = finrank R S • x :=
by
by_cases H : ∃ s : Finset S, Nonempty (Basis s R S)
· rw [trace_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]
· simp [trace_eq_zero_of_not_exists_basis R H, finrank_eq_zero_of_not_exists_basis_finset H]
