English
In a suitable AKLB setting, the restricted norm intNorm coincides with the global norm on B, i.e., intNorm = norm after identifying the bases.
Русский
В подходящей конфигурации AKLB ограниченная норма intNorm совпадает с глобальной нормой на B.
LaTeX
$$$[Module.Free A B] \\Rightarrow algebraMap A B (intNorm A B x) = norm A B x$$$
Lean4
@[simp]
theorem algebraMap_intNorm_fractionRing (x : B) :
algebraMap A (FractionRing A) (Algebra.intNorm A B x) =
Algebra.norm (FractionRing A) (algebraMap B (FractionRing B) x) :=
by
haveI : IsIntegralClosure B A (FractionRing B) := IsIntegralClosure.of_isIntegrallyClosed _ _ _
haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
IsIntegralClosure.isLocalization _ (FractionRing A) _ _
haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
exact Algebra.map_intNormAux x
