# Documentation

Mathlib.Data.MvPolynomial.Counit

## 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 = ℕ
noncomputable def MvPolynomial.ACounit (A : Type u_1) (B : Type u_2) [] [] [Algebra A B] :

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 = ℕ.

Instances For
@[simp]
theorem MvPolynomial.ACounit_X (A : Type u_1) {B : Type u_2} [] [] [Algebra A B] (b : B) :
↑() () = b
@[simp]
theorem MvPolynomial.ACounit_C {A : Type u_1} (B : Type u_2) [] [] [Algebra A B] (a : A) :
↑() (MvPolynomial.C a) = ↑() a
theorem MvPolynomial.ACounit_surjective (A : Type u_1) (B : Type u_2) [] [] [Algebra A B] :
noncomputable def MvPolynomial.counit (R : Type u_3) [] :

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 = ℕ.

Instances For
noncomputable def MvPolynomial.counitNat (A : Type u_1) [] :

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 = ℤ.

Instances For
theorem MvPolynomial.counit_C (R : Type u_3) [] (n : ) :
↑() (MvPolynomial.C n) = n
theorem MvPolynomial.counitNat_C (A : Type u_1) [] (n : ) :
↑() (MvPolynomial.C n) = n
@[simp]
theorem MvPolynomial.counit_X {R : Type u_3} [] (r : R) :
↑() () = r
@[simp]
theorem MvPolynomial.counitNat_X {A : Type u_1} [] (a : A) :
↑() () = a