UniversalEnvelopingAlgebra.hom_ext

theorem UniversalEnvelopingAlgebra.hom_ext : ∀ (R : Type u₁) {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u₃} [inst_3 : Ring A] [inst_4 : Algebra R A] {g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A}, g₁.toLieHom.comp (UniversalEnvelopingAlgebra.ι R) = g₂.toLieHom.comp (UniversalEnvelopingAlgebra.ι R) → g₁ = g₂

The theorem `UniversalEnvelopingAlgebra.hom_ext` states that for any commutative ring `R`, Lie ring `L`, Lie algebra `L` over `R`, another ring `A` and algebra `A` over `R`, if `g₁` and `g₂` are algebra homomorphisms from the universal enveloping algebra of `L` over `R` to `A`, and they share the same composite with the natural Lie algebra morphism from `L` to its universal enveloping algebra, then `g₁` and `g₂` are equal. This theorem is a type of uniqueness condition for algebra homomorphisms in the context of universal enveloping algebras.

More concisely: Given commutative rings R, Lie rings L over R, Lie algebras L over R, rings A, and algebra homomorphisms g₁ and g₂ from the universal enveloping algebra of L over R to A with the same composite with the natural Lie algebra morphism, g₁ equals g₂.