English
If S is a finite free module over R, and S_m is the localization of S at M while R_m is the localization of R at M, then for every a in S, the norm of a computed over R_m against its localization equals the localization of the norm of a computed over R.
Русский
Пусть S является сквозным модулем над R, являющимся конечным свободным модулем. Тогда норма элемента a ∈ S, вычисленная над локализацией R_m и S_m, совпадает с локализованной нормой нормального отображения над R.
LaTeX
$$$\\operatorname{N}_{S_m/R_m}(a) = \\operatorname{algebraMap}_R^{R_m}(\\operatorname{N}_{S/R}(a))$$$
Lean4
/-- Let `S` be an extension of `R` and `Rₘ Sₘ` be localizations at `M` of `R S` respectively.
Then the norm of `a : Sₘ` over `Rₘ` is the norm of `a : S` over `R` if `S` is free as `R`-module.
-/
theorem norm_localization [Module.Free R S] [Module.Finite R S] (a : S) :
Algebra.norm Rₘ (algebraMap S Sₘ a) = algebraMap R Rₘ (Algebra.norm R 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.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ), Algebra.norm_eq_matrix_det b, RingHom.map_det, ←
Algebra.map_leftMulMatrix_localization]
