trace_algebraMap — Mathlib

English

If A and B are linearly disjoint over F inside E and x ∈ B, then the A-trace of the image of x in E equals the F-image of the B-trace of x.

Русский

Если A и B линейно раздельны над F внутри E и x ∈ B, то A-трасса образа x в E равна F-образу трассы x над B.

LaTeX

$$$\\operatorname{tr}_{A}^{E}(\\iota_{B}(x)) = \\iota_{F}(\\operatorname{tr}_{F}^{B}(x)).$$$

Lean4

/-- If `A` and `B` are linearly disjoint, then `trace` and `algebraMap` commutes.
-/
theorem trace_algebraMap [FiniteDimensional F E] (h₁ : A.LinearDisjoint B) (h₂ : A ⊔ B = ⊤) (x : B) :
    Algebra.trace A E (algebraMap B E x) = algebraMap F A (Algebra.trace F B x) :=
  by
  rw [linearDisjoint_iff'] at h₁
  refine h₁.trace_algebraMap ?_ x
  simpa [sup_toSubalgebra_of_isAlgebraic_right] using congr_arg toSubalgebra h₂

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