toNonUnitalAlgHom_injective — Mathlib

English

The map sending a Lie algebra homomorphism to its induced nonunital algebra homomorphism is injective.

Русский

Отображение Ли-гомоморфизма в соответствующий ненуляющий алгоморфизм сохраняет различия между гомоморфизмами, то есть инъективно.

LaTeX

$$$\\forall f,g,\\; (\\mathrm{toNonUnitalAlgHom}\\, f = \\mathrm{toNonUnitalAlgHom}\\, g) \\Rightarrow f = g.$$$

Lean4

theorem toNonUnitalAlgHom_injective :
    Function.Injective (toNonUnitalAlgHom : _ → CommutatorRing L →ₙₐ[R] CommutatorRing L₂) := fun _ _ h =>
  ext <| NonUnitalAlgHom.congr_fun h

Похожие утверждения