trace_eq_of_algEquiv — Mathlib

English

If e is an A-algebra equivalence between B and C, then trace_A C (e x) equals trace_A B x for all x ∈ B.

Русский

Если e — алгебра-эквивариант между B и C над A, то след примененный к e x в C равен следу от x в B.

LaTeX

$$$\\operatorname{trace}_{A,C}(e x) = \\operatorname{trace}_{A,B}(x)$$$

Lean4

theorem trace_eq_of_algEquiv {A B C : Type*} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra A C]
    (e : B ≃ₐ[A] C) (x) : Algebra.trace A C (e x) = Algebra.trace A B x :=
  by
  simp_rw [Algebra.trace_apply, ← LinearMap.trace_conj' _ e.toLinearEquiv]
  congr; ext; simp [LinearEquiv.conj_apply]

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