English
If R is a nontrivial commutative semiring, the canonical map ι_R: X → FreeAlgebra R X is injective.
Русский
Пусть R ненулевой коммутативный полукольцо; каноническое отображение ι_R: X → FreeAlgebra R X инъективно.
LaTeX
$$$\ι_R: X \to \mathrm{FreeAlgebra}(R,X)$ is injective when $R$ is nontrivial.$$
Lean4
theorem ι_injective [Nontrivial R] : Function.Injective (ι R : X → FreeAlgebra R X) := fun x y hoxy ↦
by_contradiction <| by
classical
exact fun hxy : x ≠ y ↦
let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
one_ne_zero <| hfy1.symm.trans hfy0
