English
If two algebra homomorphisms g1, g2: U_R(L) →ₐ[R] A agree on the inclusion ι_R of L, then they are equal. Equivalently, homomorphisms from U_R(L) are determined by their values on L.
Русский
Если два гомоморфизма алгебр g1, g2: U_R(L) →ₐ[R] A совпадают на включении ι_R(L), то они равны. Иными словами, гомоморфизмы от U_R(L) определяются значениями на L.
LaTeX
$$$\\text{If } (g_1|_{\\iota_R(L)} = g_2|_{\\iota_R(L)}) \\text{ then } g_1 = g_2$$$
Lean4
/-- See note [partially-applied ext lemmas]. -/
@[ext]
theorem hom_ext {g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A}
(h :
(g₁ : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R) =
(g₂ : UniversalEnvelopingAlgebra R L →ₗ⁅R⁆ A).comp (ι R)) :
g₁ = g₂ :=
have h' : (lift R).symm g₁ = (lift R).symm g₂ := by simp [h]
(lift R).symm.injective h'
