English
Conjugation by ω defines a Lie algebra isomorphism on endomorphism algebras: x maps to ω x ω.
Русский
Сопряжение вокруг ω задаёт изоморфизм Ли-алгебр между концевыми алгебрами: x ↦ ω x ω.
LaTeX
$$$\\omega\\_\\mathrm{Conj}: \\mathrm{Matrix} \\rightarrow \\mathrm{Matrix}$ is a Lie algebra isomorphism with $\\omega\\_b(x) = \\omega(b) \\, x \\, \\omega(b)$$$
Lean4
/-- The conjugation `x ↦ ωxω` as an equivalence of Lie algebras. -/
@[simps]
def ωConj : Matrix (b.support ⊕ ι) (b.support ⊕ ι) R ≃ₗ⁅R⁆ Matrix (b.support ⊕ ι) (b.support ⊕ ι) R
where
toFun x := ω b * x * ω b
invFun x := ω b * x * ω b
map_add' x y := by noncomm_ring
map_smul' t x := by simp
map_lie'
{x y} := by
simp only [Ring.lie_def]
nth_rw 1 [← mul_one x]
nth_rw 2 [← one_mul x]
simp only [← ω_mul_ω (b := b)]
noncomm_ring
left_inv
x := by
simp only [← mul_assoc, ω_mul_ω, one_mul]
simp [mul_assoc]
right_inv
x := by
simp only [← mul_assoc, ω_mul_ω, one_mul]
simp [mul_assoc]
