hom_ext — Mathlib

English

If two algebra homomorphisms agree on the generators ι_R(X), they are equal.

Русский

Если два гомоморфизма алгебр совпадают на образах генераторов ι_R(X), они равны.

LaTeX

$$$\forall f,g: FreeAlgebra(R,X) \to_A A,\; (f\circ \iota_R = g\circ \iota_R) \Rightarrow f=g$$$

Lean4

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem hom_ext {f g : FreeAlgebra R X →ₐ[R] A}
    (w : (f : FreeAlgebra R X → A) ∘ ι R = (g : FreeAlgebra R X → A) ∘ ι R) : f = g :=
  by
  rw [← lift_symm_apply, ← lift_symm_apply] at w
  exact (lift R).symm.injective w

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