English
Let A be an R-algebra and f, g be algebra homomorphisms from the Tensor algebra TensorAlgebra R M to A. If f and g agree on the canonical map ι_R: M → TensorAlgebra R M, i.e. f ∘ ι_R = g ∘ ι_R, then f = g.
Русский
Пусть A — R-алгебра, а f, g — алгебра-гомоморфизмы из TensorAlgebra R M в A. Если они совпадают на каноническом отображении ι_R: M → TensorAlgebra R M, то f = g.
LaTeX
$$$\\forall A\\, [\\mathrm{Semiring}\\ A]\\, [\\mathrm{Algebra}\\ R\\ A],\\ f,g:\\ TensorAlgebra\\ R\\ M \\to_E_R A,\\ f\\circ \\iota_R = g\\circ \\iota_R \\Rightarrow f = g$$$
Lean4
/-- See note [partially-applied ext lemmas]. -/
@[ext]
theorem hom_ext {A : Type*} [Semiring A] [Algebra R A] {f g : TensorAlgebra R M →ₐ[R] A}
(w : f.toLinearMap.comp (ι R) = g.toLinearMap.comp (ι R)) : f = g :=
by
rw [← lift_symm_apply, ← lift_symm_apply] at w
exact (lift R).symm.injective w
