English
The algebra map from A to FractionRing A of intTrace applied to x agrees with the trace on FractionRing A to FractionRing B after mapping x into B via the fraction ring.
Русский
След в FractionRing_A согласуется с следом на FractionRing_B после отображения x через дробно-ромовое кольцо.
LaTeX
$$$\\forall x\\in B,\\ algebraMap A (FractionRing A) (Algebra.intTrace A B x) = Algebra.trace (FractionRing A) (FractionRing B) (algebraMap B (FractionRing B) x)$$$
Lean4
theorem algebraMap_intTrace_fractionRing (x : B) :
algebraMap A (FractionRing A) (Algebra.intTrace A B x) =
Algebra.trace (FractionRing A) (FractionRing B) (algebraMap 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_intTraceAux x
