English
The explicit recursive definition of liftFun is given by cases on the Pre R X structure.
Русский
Явное рекурсивное определение liftFun задаётся по случаям на структуру Pre R X.
LaTeX
$$liftFun {R} {X} {A} f$$
Lean4
/-- If `α` is a type, and `R` is a commutative semiring, then `FreeAlgebra R α` is the
free (unital, associative) `R`-algebra generated by `α`.
This is an `R`-algebra equipped with a function `FreeAlgebra.ι R : α → FreeAlgebra 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 `FreeAlgebra.ι R` and a unique `R`-algebra homomorphism
`FreeAlgebra.lift R f : FreeAlgebra R α →ₐ[R] A`.
A typical element of `FreeAlgebra R α` is an `R`-linear
combination of formal 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) + (a * b * b + 3)` is a
"typical" element of `FreeAlgebra R α`. In particular if `α` is empty
then `FreeAlgebra R α` is isomorphic to `R`, and if `α` has one term `t`
then `FreeAlgebra R α` is isomorphic to the polynomial ring `R[t]`.
If `α` has two or more terms then `FreeAlgebra R α` is not commutative.
One can think of `FreeAlgebra R α` as the free non-commutative polynomial ring
with coefficients in `R` and variables indexed by `α`.
-/
def FreeAlgebra :=
Quot (FreeAlgebra.Rel R X)
