English
If A, B, A_m, B_m form a localization diagram with isIntegrallyClosed, the localization preserves the equality of traces along the base-changed maps.
Русский
Если A, B, A_m, B_m образуют диаграмму локализации с изоморфизмом интегрального замыкания, локализация сохраняет равенство следов при преобразовании основания.
LaTeX
$$$\\forall x, algebraMap A A_m (Algebra.intTrace A B x) = Algebra.intTrace A_m B_m (algebraMap B B_m x)$$$
Lean4
/-- The norm of a finite extension of integrally closed domains `B/A` is the restriction of
the norm on `Frac(B)/Frac(A)` onto `B/A`. See `Algebra.algebraMap_intNorm`. -/
noncomputable def intNorm : B →* A :=
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⁰
Algebra.intNormAux A (FractionRing A) (FractionRing B) B
