English
The map that assigns to each algebra hom its associated Lie algebra hom preserves Lie brackets: for f : A →ₐ[R] B and g : B →ₐ[R] C, the induced linear map (g ∘ f) to Lie is the composition of the induced Lie maps.
Русский
Пусть f: A →ₐ[R] B и g: B →ₐ[R] C. Приведённое отображение в Lie-гомоморфизм соответствует композиции линейных отображений: (g ∘ f) в Lie-гомоморфизм равен g.toLieHom ∘ f.toLieHom.
LaTeX
$$$$\text{toLieHom}(g\circ f) = \text{toLieHom}(g) \circ \text{toLieHom}(f).$$$$
Lean4
/-- The map `ofAssociativeAlgebra` associating a Lie algebra to an associative algebra is
functorial. -/
def toLieHom : A →ₗ⁅R⁆ B :=
{ f.toLinearMap with map_lie' := fun {_ _} => by simp [LieRing.of_associative_ring_bracket] }
