# mathlibdocumentation

data.mv_polynomial.counit

## Counit morphisms for multivariate polynomials #

One may consider the ring of multivariate polynomials mv_polynomial 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 mv_polynomial A R →ₐ[R] A obtained by X a ↦ a.

### Main declarations #

• mv_polynomial.acounit R A is the natural surjective algebra homomorphism mv_polynomial A R →ₐ[R] A obtained by X a ↦ a
• mv_polynomial.counit is an “absolute” variant with R = ℤ
• mv_polynomial.counit_nat is an “absolute” variant with R = ℕ
def mv_polynomial.acounit (A : Type u_1) (B : Type u_2) [ B] :

mv_polynomial.acounit A B is the natural surjective algebra homomorphism mv_polynomial B A →ₐ[A] B obtained by X a ↦ a.

See mv_polynomial.counit for the “absolute” variant with A = ℤ, and mv_polynomial.counit_nat for the “absolute” variant with A = ℕ.

Equations
@[simp]
theorem mv_polynomial.acounit_X (A : Type u_1) {B : Type u_2} [ B] (b : B) :
= b
@[simp]
theorem mv_polynomial.acounit_C {A : Type u_1} (B : Type u_2) [ B] (a : A) :
= B) a
theorem mv_polynomial.acounit_surjective (A : Type u_1) (B : Type u_2) [ B] :
def mv_polynomial.counit (R : Type u_3) [comm_ring R] :

mv_polynomial.counit R is the natural surjective ring homomorphism mv_polynomial R ℤ →+* R obtained by X r ↦ r.

See mv_polynomial.acounit for a “relative” variant for algebras over a base ring, and mv_polynomial.counit_nat for the “absolute” variant with R = ℕ.

Equations
def mv_polynomial.counit_nat (A : Type u_1)  :

mv_polynomial.counit_nat A is the natural surjective ring homomorphism mv_polynomial A ℕ →+* A obtained by X a ↦ a.

See mv_polynomial.acounit for a “relative” variant for algebras over a base ring and mv_polynomial.counit for the “absolute” variant with A = ℤ.

Equations
theorem mv_polynomial.counit_surjective (R : Type u_3) [comm_ring R] :
theorem mv_polynomial.counit_nat_surjective (A : Type u_1)  :
theorem mv_polynomial.counit_C (R : Type u_3) [comm_ring R] (n : ) :
= n
theorem mv_polynomial.counit_nat_C (A : Type u_1) (n : ) :
@[simp]
theorem mv_polynomial.counit_X {R : Type u_3} [comm_ring R] (r : R) :
= r
@[simp]
theorem mv_polynomial.counit_nat_X {A : Type u_1} (a : A) :