English
Under finite-free hypothesis, for any a ∈ S and b ∈ R, and given the M-suitable non-zero divisor condition, the equality of norms in R is equivalent to the equality of corresponding localized norms in R_m.
Русский
При конечной свободности модуля S над R, для любого a ∈ S и b ∈ R, при условии, что M локализация не нарушает делимость, равенство нормы в R эквивалентно равенству локализованных норм после локализации.
LaTeX
$$$\\operatorname{norm}_{R} (a) = b \\quad\\iff\\quad \\operatorname{norm}_{R_m}(\\mathrm{algebraMap}_S^{S_m}(a)) = \\mathrm{algebraMap}_R^{R_m}(b).$$$
Lean4
/-- The norm of `a : S` in `R` can be computed in `Sₘ`. -/
theorem norm_eq_iff [Module.Free R S] [Module.Finite R S] {a : S} {b : R} (hM : M ≤ nonZeroDivisors R) :
Algebra.norm R a = b ↔ (Algebra.norm Rₘ) ((algebraMap S Sₘ) a) = algebraMap R Rₘ b :=
⟨fun h ↦ h.symm ▸ Algebra.norm_localization _ M _, fun h ↦
IsLocalization.injective Rₘ hM <| h.symm ▸ (Algebra.norm_localization R M a).symm⟩
