English
Let R ⊂ S ⊂ T be a tower of finite algebras with compatible scalar multiplication. Then the trace from T to R factors as the composition of the trace from T to S followed by the trace from S to R. In symbols, Tr_{R}^{T} = Tr_{R}^{S} ∘ Tr_{S}^{T}.
Русский
Пусть R ⊂ S ⊂ T образуют цепь конечных расширений с совместимой скалярами. Тогда след из T в R факторизуется через след из T в S и через след из S в R: Tr_{R}^{T} = Tr_{R}^{S} ∘ Tr_{S}^{T}.
LaTeX
$$$\\operatorname{Tr}_{T/R} = \\operatorname{Tr}_{S/R} \\circ \\operatorname{Tr}_{T/S}$$$
Lean4
theorem trace_comp_trace_of_basis [Algebra S T] [IsScalarTower R S T] {ι κ : Type*} [Finite ι] [Finite κ]
(b : Basis ι R S) (c : Basis κ S T) : (trace R S).comp ((trace S T).restrictScalars R) = trace R T :=
by
ext
rw [LinearMap.comp_apply, LinearMap.restrictScalars_apply, trace_trace_of_basis b c]
