English
A linear equivalence e between modules induces a Lie algebra equivalence between their endomorphism algebras, via conjugation.
Русский
Линейное эквивалентное отображение между модулями индуцирует эквивалентность Ли между их пространствами эндоморфизмов через сопряжение.
LaTeX
$$$\mathrm{lieConj} : \mathrm{End}_R(M_1) \simeq_{\text{Lie}} \mathrm{End}_R(M_2)$ with the Lie bracket compatibility$$
Lean4
/-- A linear equivalence of two modules induces a Lie algebra equivalence of their endomorphisms. -/
def lieConj : Module.End R M₁ ≃ₗ⁅R⁆ Module.End R M₂ :=
{ e.conj with
map_lie' := fun {f g} =>
show e.conj ⁅f, g⁆ = ⁅e.conj f, e.conj g⁆ by
simp only [LieRing.of_associative_ring_bracket, Module.End.mul_eq_comp, e.conj_comp, map_sub] }
