English
Under the same hypotheses as the previous item, the two-step trace formula holds with the scalar tower data encoded appropriately; i.e., the two traces compose to the single trace from the bottom to the top of the tower.
Русский
При тех же предположениях выполняется формула композиции следа: общий след из нижнего кольца в верхнее равен композиции следов по промежуточному кольцу.
LaTeX
$$$\\operatorname{Tr}_{R}^{T} = \\operatorname{Tr}_{R}^{S} \\circ \\operatorname{Tr}_{S}^{T}$$$
Lean4
/-- Let `T / S / R` be a tower of finite extensions of fields. Then
$\text{Trace}_{T/R} = \text{Trace}_{S/R} \circ \text{Trace}_{T/S}$. -/
@[simp, stacks 0BIJ "Trace"]
theorem trace_comp_trace [Algebra S T] [IsScalarTower R S T] [Module.Free R S] [Module.Finite R S] [Module.Free S T]
[Module.Finite S T] : (trace R S).comp ((trace S T).restrictScalars R) = trace R T :=
LinearMap.ext trace_trace
