English
Under suitable hypotheses, the algebra map commutes with intTrace, i.e., algebraMap_A_K (intTrace_A_B x) = trace_{K L}(algebraMap_B_L x).
Русский
При подходящих гипотезах отображение по базису коммутирует с intTrace: algebraMap_A_K(intTrace_A_B(x)) = trace_{K L}(algebraMap_B_L(x)).
LaTeX
$$$[IsIntegrallyClosed A]\\;[IsDomain A]\\[IsDomain B] \\Rightarrow algebraMap A K (Algebra.intTrace A B x) = Algebra.trace K L (algebraMap B L x)$$$
Lean4
theorem algebraMap_intTrace (x : B) : algebraMap A K (Algebra.intTrace A B x) = Algebra.trace K L (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.intTrace, Algebra.map_intTraceAux, ← AlgEquiv.commutes (FractionRing.algEquiv B L)]
apply Algebra.trace_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) _
