English
Let R be a commutative semiring and X a type. In the free algebra FreeAlgebra R X, the image of every generator ι_R(x) is never equal to any scalar from R via algebraMap. Equivalently, for all x : X and all r : R, ι_R x ≠ algebraMap R (FreeAlgebra R X) r.
Русский
Пусть R — коммутативная полукольца и X — множество. В свободной алгебре FreeAlgebra R X образ каждого генератора ι_R(x) не равен скаляру, получаемому через отображение алгебраMap из R в FreeAlgebra R X. То есть для любых x : X и r : R верно ι_R x ≠ algebraMap R (FreeAlgebra R X) r.
LaTeX
$$$ \\forall x : X, \\forall r : R, ι_R x \\neq algebraMap R (FreeAlgebra R X) r $$$
Lean4
@[simp]
theorem ι_ne_algebraMap [Nontrivial R] (x : X) (r : R) : ι R x ≠ algebraMap R _ r := fun h ↦
by
let f0 : FreeAlgebra R X →ₐ[R] R := lift R 0
let f1 : FreeAlgebra R X →ₐ[R] R := lift R 1
have hf0 : f0 (ι R x) = 0 := lift_ι_apply _ _
have hf1 : f1 (ι R x) = 1 := lift_ι_apply _ _
rw [h, f0.commutes, Algebra.algebraMap_self_apply] at hf0
rw [h, f1.commutes, Algebra.algebraMap_self_apply] at hf1
exact zero_ne_one (hf0.symm.trans hf1)
