English
For rings R, S, T with S × T as a product, the trace from R to S × T of an element x equals the sum of the traces from R to S of x’s S-coordinate and from R to T of x’s T-coordinate: Tr_{R}^{S×T}(x) = Tr_{R}^{S}(x.fst) + Tr_{R}^{T}(x.snd).
Русский
Для колец R, S, T с произведением S × T выполнено Tr_{R}^{S×T}(x) = Tr_{R}^{S}(x.fst) + Tr_{R}^{T}(x.snd).
LaTeX
$$$\\operatorname{trace}_{R}^{S\\times T}(x) = \\operatorname{trace}_{R}^{S}(x_{1}) + \\operatorname{trace}_{R}^{T}(x_{2})$$$
Lean4
@[simp]
theorem trace_prod_apply [Module.Free R S] [Module.Free R T] [Module.Finite R S] [Module.Finite R T] (x : S × T) :
trace R (S × T) x = trace R S x.fst + trace R T x.snd :=
by
nontriviality R
let f := (lmul R S).toLinearMap.prodMap (lmul R T).toLinearMap
have : (lmul R (S × T)).toLinearMap = (prodMapLinear R S T S T R).comp f := LinearMap.ext₂ Prod.mul_def
simp_rw [trace, this]
exact trace_prodMap' _ _
