trace_localization — Mathlib

English

For a ∈ S, the trace from R_m to S_m of its localization equals the localization of the trace from R to S of a.

Русский

Для элемента a ∈ S след по локализации R_m на S_m совпадает с локализованной следовой величиной от R к S применительно к a.

LaTeX

$$$\\operatorname{tr}_{R_m/S_m}(\\mathrm{algebraMap}_S^{S_m}(a)) = \\mathrm{algebraMap}_R^{R_m}(\\operatorname{tr}_{R/S}(a)).$$$

Lean4

/-- Let `S` be an extension of `R` and `Rₘ Sₘ` be localizations at `M` of `R S` respectively.
Then the trace of `a : Sₘ` over `Rₘ` is the trace of `a : S` over `R` if `S` is free as `R`-module.
-/
theorem trace_localization [Module.Free R S] [Module.Finite R S] (a : S) :
    Algebra.trace Rₘ Sₘ (algebraMap S Sₘ a) = algebraMap R Rₘ (Algebra.trace R S a) :=
  by
  cases subsingleton_or_nontrivial R
  · haveI : Subsingleton Rₘ := Module.subsingleton R Rₘ
    simp [eq_iff_true_of_subsingleton]
  let b := Module.Free.chooseBasis R S
  letI := Classical.decEq (Module.Free.ChooseBasisIndex R S)
  rw [Algebra.trace_eq_matrix_trace (b.localizationLocalization Rₘ M Sₘ), Algebra.trace_eq_matrix_trace b, ←
    Algebra.map_leftMulMatrix_localization]
  exact (AddMonoidHom.map_trace (algebraMap R Rₘ).toAddMonoidHom _).symm

Похожие утверждения