English
Conjugation by a unit on the left also preserves the spectrum: spectrum_R(u⁻¹ a u) = spectrum_R(a).
Русский
С другой стороны конъюгация слева также сохраняет спектр.
LaTeX
$$$\operatorname{spectrum}_R(u^{-1} a u) = \operatorname{spectrum}_R(a)$$$
Lean4
/-- Conjugation by a unit preserves the spectrum, inverse on right. -/
@[simp]
theorem units_conjugate {a : A} {u : Aˣ} : spectrum R (u * a * u⁻¹) = spectrum R a :=
by
suffices ∀ (b : A) (v : Aˣ), spectrum R (v * b * v⁻¹) ⊆ spectrum R b
by
refine le_antisymm (this a u) ?_
apply le_of_eq_of_le ?_ <| this (u * a * u⁻¹) u⁻¹
simp [mul_assoc]
intro a u μ hμ
rw [spectrum.mem_iff] at hμ ⊢
contrapose! hμ
simpa [mul_sub, sub_mul, Algebra.right_comm] using u.isUnit.mul hμ |>.mul u⁻¹.isUnit
