map_intTraceAux — Mathlib

English

The A-linear map intTraceAux composes with algebra maps to recover the K-Trace on L, i.e., the restricted trace equals the full trace after base change.

Русский

Линейное отображение intTraceAux, затем A→K переносит ограниченный след на истинный след после смены основания.

LaTeX

$$$\\mathrm{algebraMap}_{A K}(\\mathrm{intTraceAux}_{A K L B}) = \\mathrm{trace}_{K L} \\circ \\mathrm{algebraMap}_{B L}$$$

Lean4

theorem map_intTraceAux [IsIntegrallyClosed A] (x : B) :
    algebraMap A K (Algebra.intTraceAux A K L B x) = Algebra.trace K L (algebraMap B L x) :=
  IsIntegralClosure.algebraMap_equiv A (integralClosure A K) K A _

Похожие утверждения