English
Two nonunital algebra homomorphisms F1, F2 from FreeNonUnitalNonAssocAlgebra R X to A are equal iff they agree on the generators; i.e., F1(of x) = F2(of x) for all x ∈ X.
Русский
Два гомоморфизма неединичного типа без ассоциаций из FreeNonUnitalNonAssocAlgebra R X в A равны тогда и только тогда, когда они совпадают на генераторах: F1(of x) = F2(of x) для всех x ∈ X.
LaTeX
$$$\\forall F_1 F_2 : FreeNonUnitalNonAssocAlgebra\\ R\\ X \\to A,\\; (F_1 = F_2) \\iff (\\forall x \\in X, F_1(\\mathrm{of}\\ x) = F_2(\\mathrm{of}\\ x)).$$$
Lean4
/-- If `α` is a type, and `R` is a semiring, then `FreeNonUnitalNonAssocAlgebra R α` is the free
non-unital non-associative `R`-algebra generated by `α`.
This is an `R`-algebra equipped with a function
`FreeNonUnitalNonAssocAlgebra.of R : α → FreeNonUnitalNonAssocAlgebra R α` which has
the following universal property: if `A` is any `R`-algebra, and `f : α → A` is any function,
then this function is the composite of `FreeNonUnitalNonAssocAlgebra.of R`
and a unique non-unital `R`-algebra homomorphism
`FreeNonUnitalNonAssocAlgebra.lift R f : FreeNonUnitalNonAssocAlgebra R α →ₙₐ[R] A`.
A typical element of `FreeNonUnitalNonAssocAlgebra R α` is an `R`-linear combination of
nonempty formal (non-commutative, non-associative) products of elements of `α`.
For example if `x` and `y` are terms of type `α` and
`a`, `b` are terms of type `R` then `(3 * a * a) • (x * (y * x)) + (2 * b + 1) • (y * x)` is a
"typical" element of `FreeNonUnitalNonAssocAlgebra R α`.
-/
abbrev FreeNonUnitalNonAssocAlgebra :=
MonoidAlgebra R (FreeMagma X)
