## Counit morphisms for multivariate polynomials #

One may consider the ring of multivariate polynomials `MvPolynomial A R`

with coefficients in `R`

and variables indexed by `A`

. If `A`

is not just a type, but an algebra over `R`

,
then there is a natural surjective algebra homomorphism `MvPolynomial A R →ₐ[R] A`

obtained by `X a ↦ a`

.

### Main declarations #

`MvPolynomial.ACounit R A`

is the natural surjective algebra homomorphism`MvPolynomial A R →ₐ[R] A`

obtained by`X a ↦ a`

`MvPolynomial.counit`

is an “absolute” variant with`R = ℤ`

`MvPolynomial.counitNat`

is an “absolute” variant with`R = ℕ`

`MvPolynomial.ACounit A B`

is the natural surjective algebra homomorphism
`MvPolynomial B A →ₐ[A] B`

obtained by `X a ↦ a`

.

See `MvPolynomial.counit`

for the “absolute” variant with `A = ℤ`

,
and `MvPolynomial.counitNat`

for the “absolute” variant with `A = ℕ`

.

## Equations

## Instances For

`MvPolynomial.counit R`

is the natural surjective ring homomorphism
`MvPolynomial R ℤ →+* R`

obtained by `X r ↦ r`

.

See `MvPolynomial.ACounit`

for a “relative” variant for algebras over a base ring,
and `MvPolynomial.counitNat`

for the “absolute” variant with `R = ℕ`

.

## Equations

- MvPolynomial.counit R = (MvPolynomial.ACounit ℤ R).toRingHom

## Instances For

`MvPolynomial.counitNat A`

is the natural surjective ring homomorphism
`MvPolynomial A ℕ →+* A`

obtained by `X a ↦ a`

.

See `MvPolynomial.ACounit`

for a “relative” variant for algebras over a base ring
and `MvPolynomial.counit`

for the “absolute” variant with `A = ℤ`

.