English
Under the same hypotheses, the intNorm maps commute with the isLocalization maps, giving coherence of norms under localization.
Русский
При тех же предпосылках нормы intNorm коммутируют с локализационными отображениями, что обеспечивает совместимость норм при локализации.
LaTeX
$$$\\forall x, algebraMap A A_m (Algebra.intNorm A B x) = Algebra.intNorm A_m B_m (algebraMap B B_m x)$$$
Lean4
theorem algebraMap_intNorm (x : B) : algebraMap A K (Algebra.intNorm A B x) = Algebra.norm K (algebraMap B L 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⁰
haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
apply (FractionRing.algEquiv A K).symm.injective
rw [AlgEquiv.commutes, Algebra.intNorm, Algebra.map_intNormAux, ← AlgEquiv.commutes (FractionRing.algEquiv B L)]
apply Algebra.norm_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv (FractionRing.algEquiv B L).toRingEquiv
ext
exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _
