English
The quotient map from the tensor algebra to the universal enveloping algebra is a morphism of associative algebras.
Русский
Кватернированная карта из тензорной алгебры в универзальную оболочку является однозначно определяемым отображением между ассоциативными алгебрами.
LaTeX
$$def mkAlgHom : TensorAlgebra R L →ₐ[R] UniversalEnvelopingAlgebra R L := RingQuot.mkAlgHom R (Rel R L)$$
Lean4
/-- The universal property of the universal enveloping algebra: Lie algebra morphisms into
associative algebras lift to associative algebra morphisms from the universal enveloping algebra. -/
def lift : (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A)
where
toFun
f :=
RingQuot.liftAlgHom R
⟨TensorAlgebra.lift R (f : L →ₗ[R] A), by
intro a b h; induction h
simp only [LieRing.of_associative_ring_bracket, map_add, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
LieHom.map_lie, map_mul, sub_add_cancel]⟩
invFun F := (F : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R)
left_inv
f :=
by
ext
-- Porting note: was
-- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
-- LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.coe_comp, AlgHom.coe_toLieHom,
-- LieHom.coe_mk, Function.comp_apply, AlgHom.toLinearMap_apply,
-- RingQuot.liftAlgHom_mkAlgHom_apply]
simp only [LieHom.coe_comp, Function.comp_apply, AlgHom.coe_toLieHom, UniversalEnvelopingAlgebra.ι_apply, mkAlgHom]
simp only [UniversalEnvelopingAlgebra, RingQuot.liftAlgHom_mkAlgHom_apply, TensorAlgebra.lift_ι_apply,
LieHom.coe_toLinearMap]
right_inv
F := by
apply RingQuot.ringQuot_ext'
ext
-- Porting note: was
-- simp only [ι, mkAlgHom, TensorAlgebra.lift_ι_apply, LieHom.coe_toLinearMap,
-- LinearMap.toFun_eq_coe, LinearMap.coe_comp, LieHom.toLinearMap_comp,
-- AlgHom.comp_toLinearMap, Function.comp_apply, AlgHom.toLinearMap_apply,
-- RingQuot.liftAlgHom_mkAlgHom_apply, AlgHom.coe_toLieHom, LieHom.coe_mk]
-- extra `rfl` after https://github.com/leanprover/lean4/pull/2644
simp [mkAlgHom]; rfl
