hom_ext — Mathlib

English

If F1 and F2 are LieHom R (FreeLieAlgebra R X) L, and they agree on all generators, then F1 = F2.

Русский

Если F1 и F2 — гомоморфизмы Ли между FreeLieAlgebra R X и L и они совпадают на всех генераторах, то F1 = F2.

LaTeX

$$$\forall x, F_1(\mathrm{of}(R,x)) = F_2(\mathrm{of}(R,x)) \Rightarrow F_1 = F_2.$$$

Lean4

@[ext]
theorem hom_ext {F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L} (h : ∀ x, F₁ (of R x) = F₂ (of R x)) : F₁ = F₂ :=
  have h' : (lift R).symm F₁ = (lift R).symm F₂ := by ext; simp [h]
  (lift R).symm.injective h'

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