mathlib3 documentation

data.mv_polynomial.counit

Counit morphisms for multivariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

noncomputable def mv_polynomial.acounit (A : Type u_1) (B : Type u_2) [comm_semiring A] [comm_semiring B] [algebra A 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} [comm_semiring A] [comm_semiring B] [algebra A B] (b : B) :
@[simp]
theorem mv_polynomial.acounit_C {A : Type u_1} (B : Type u_2) [comm_semiring A] [comm_semiring B] [algebra A B] (a : A) :
noncomputable 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
noncomputable def mv_polynomial.counit_nat (A : Type u_1) [comm_semiring A] :

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
@[simp]
theorem mv_polynomial.counit_X {R : Type u_3} [comm_ring R] (r : R) :