lift_unique — Mathlib

English

Let g be an algebra homomorphism g: U_R(L) →ₐ[R] A. Then g ∘ ι_R = f if and only if g = lift R f. In words, the lift is the unique extension of f to the universal enveloping algebra.

Русский

Пусть g: U_R(L) →ₐ[R] A — гомоморфизм алгебр. Тогда g ∘ ι_R = f тогда и только тогда, когда g = lift R f. Иными словами, lift является единственным продолжением f на U_R(L).

LaTeX

$$$ (g \\circ \\iota_R) = f \\,\\;\\; \\Longleftrightarrow \\;\\; g = \\mathrm{lift}\\;R\\;f $$$

Lean4

theorem lift_unique (g : UniversalEnvelopingAlgebra R L →ₐ[R] A) : g ∘ ι R = f ↔ g = lift R f :=
  by
  refine Iff.trans ?_ (lift R).symm_apply_eq
  constructor <;> · intro h; ext; simp [← h]

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