English
For Lie algebras L and L2 over R and a Lie homomorphism f: L → L2, one obtains a nonunital algebra homomorphism between the commutator rings: CommutatorRing L →ₙₐ[R] CommutatorRing L2, with the same underlying map and with map_zero' = f.map_zero and map_mul' = f.map_lie.
Русский
Для Ли-алгебр L и L2 над R и Ли-гомоморфизма f: L → L2 имеется ненулевой алгоморфизм между коммутатор-кольцами: CommutatorRing L →ₙₐ[R] CommutatorRing L2, который совпадает с f на L и сохраняет ноль и произведение по Ли-скобке.
LaTeX
$$$\\exists \\hat f: \\mathrm{CommutatorRing}(L) \\to_{\\mathrm{NonUnitalAlg}}[R] \\mathrm{CommutatorRing}(L_2)\\text{ with } \\hat f|_L = f. $$$
Lean4
/-- Regarding the `LieRing` of a `LieAlgebra` as a `NonUnitalNonAssocRing`, we can
regard a `LieHom` as a `NonUnitalAlgHom`. -/
@[simps]
def toNonUnitalAlgHom (f : L →ₗ⁅R⁆ L₂) : CommutatorRing L →ₙₐ[R] CommutatorRing L₂ :=
{ f with
toFun := f
map_zero' := f.map_zero
map_mul' := f.map_lie }
