English
There is a canonical A-linear map from B to A constructed by composing the integral-closure isomorphism with the trace, yielding an A-linear map representing the restricted trace.
Русский
Существует каноническое A-линейное отображение B → A, полученное как композиция изоморфизма интегрального замыкания с следом, представляющее ограниченный след.
LaTeX
$$$[IsIntegrallyClosed A]\\;: \\;\\text{linear map } B \\to_A A\\;:=\\; (IsIntegralClosure.equiv A (integralClosure A K) K A).toLinearMap\\circ\\Bigl((\\mathcal{Algebra}.trace K L\\Bigr)\\;\\text{restricted to } B\\B$$$
Lean4
/-- The restriction of the trace on `L/K` restricted onto `B/A` in an AKLB setup.
See `Algebra.intTrace` instead. -/
noncomputable def intTraceAux [IsIntegrallyClosed A] : B →ₗ[A] A :=
(IsIntegralClosure.equiv A (integralClosure A K) K A).toLinearMap.comp
((((Algebra.trace K L).restrictScalars A).comp (IsScalarTower.toAlgHom A B L).toLinearMap).codRestrict
(Subalgebra.toSubmodule <| integralClosure A K)
(fun x ↦ isIntegral_trace (IsIntegral.algebraMap (IsIntegralClosure.isIntegral A L x))))
