English
If M defines a localization, then the comparison of intTrace before and after localization holds, i.e., algebraMap A A_m (intTrace A B x) equals intTrace A_m B_m (algebraMap B B_m x).
Русский
При локализации по M утверждается: algebraMap_A_A_m(intTrace_A_B(x)) = intTrace_{A_m B_m}(algebraMap_B B_m x).
LaTeX
$$$\\forall x\\in B,\\ algebraMap A A_m (Algebra.intTrace A B x) = Algebra.intTrace A_m B_m (algebraMap B B_m x)$$$
Lean4
theorem intTrace_eq_trace [Module.Free A B] : Algebra.intTrace A B = Algebra.trace A B :=
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_intTrace_fractionRing, Algebra.trace_localization A A⁰]
