English
The operation join₁ collapses a polynomial whose coefficients live in polynomials into a polynomial in the outer variables, and this map is an algebra homomorphism.
Русский
Операция join₁ сворачивает полином, коэффициенты которого лежат в полиномах, в полином по внешним переменным, и этот отображение — гомоморфизм алгебр.
LaTeX
$$$\\text{join}_1 : MvPolynomial( MvPolynomial\\ σ\\ R)\\ R \\to_{\\mathbb{R}} MvPolynomial\\ σ\\ R$ is an algebra homomorphism$$
Lean4
/-- `join₁` is the monadic join operation corresponding to `MvPolynomial.bind₁`. Given a polynomial `p`
with coefficients in `R` whose variables are polynomials in `σ` with coefficients in `R`,
`join₁ p` collapses `p` to a polynomial with variables in `σ` and coefficients in `R`.
This operation is an algebra hom.
-/
def join₁ : MvPolynomial (MvPolynomial σ R) R →ₐ[R] MvPolynomial σ R :=
aeval id
