English
The simplified version of the coherence of intNorm_MOD-NLS with the fraction ring, i.e., the fractional normalization aligns with the base case.
Русский
Упрощённая версия согласованности intNorm с дробно-ромовым кольцом: нормализация через дробную оболочку согласуется с базовым случаем.
LaTeX
$$$[IsIntegrallyClosed A]\\;[IsDomain A]\\Rightarrow algebraMap A (FractionRing A) (Algebra.intNorm A B x) = Algebra.norm (FractionRing A) (algebraMap B (FractionRing B) x)$$$
Lean4
theorem intNorm_eq_norm [Module.Free A B] : Algebra.intNorm A B = Algebra.norm A :=
by
ext x
haveI : IsIntegralClosure B A (FractionRing B) := IsIntegralClosure.of_isIntegrallyClosed _ _ _
haveI : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B) :=
IsIntegralClosure.isLocalization _ (FractionRing A) _ _
apply IsFractionRing.injective A (FractionRing A)
rw [Algebra.algebraMap_intNorm_fractionRing, Algebra.norm_localization A A⁰]
