English
In a localization setting with a maximal ideal, the trace maps respect the induced maps between quotient rings coming from localization.
Русский
В локализационной настройке с максимальной идеалой следы согласованы с соответствующими отображениями между фактор-кольцами, полученными локализацией.
LaTeX
$$$\\operatorname{trace}_{(R/p)}^{(S/pS)} = \\text{... localization-compatible ...}$$$
Lean4
theorem trace_quotient_mk [IsLocalRing R] (x : S) :
Algebra.trace (R ⧸ p) (S ⧸ pS) (Ideal.Quotient.mk pS x) = Ideal.Quotient.mk p (Algebra.trace R S x) := by
classical
let ι := Module.Free.ChooseBasisIndex R S
let b : Module.Basis ι R S := Module.Free.chooseBasis R S
rw [trace_eq_matrix_trace b, trace_eq_matrix_trace (basisQuotient b), AddMonoidHom.map_trace]
congr 1
ext i j
simp only [leftMulMatrix_apply, coe_lmul_eq_mul, LinearMap.toMatrix_apply, basisQuotient_apply, LinearMap.mul_apply',
Matrix.map_apply, ← map_mul, basisQuotient_repr]
