mathlib documentation

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 #

source
noncomputable def mv_polynomial.acounit (A : Type u_1) (B : Type u_2) [comm_semiring A] [comm_semiring B] [algebra A B] :
mv_polynomial B A →ₐ[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
source
@[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) :
⇑(mv_polynomial.acounit A B) (mv_polynomial.X b) = b
source
@[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) :
⇑(mv_polynomial.acounit A B) (⇑mv_polynomial.C a) = ⇑(algebra_map A B) a
source
theorem mv_polynomial.acounit_surjective (A : Type u_1) (B : Type u_2) [comm_semiring A] [comm_semiring B] [algebra A B] :
function.surjective ⇑(mv_polynomial.acounit A B)
source
noncomputable def mv_polynomial.counit (R : Type u_3) [comm_ring R] :
mv_polynomial R ℤ →+* 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
source
noncomputable def mv_polynomial.counit_nat (A : Type u_1) [comm_semiring A] :
mv_polynomial A ℕ →+* 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
source
theorem mv_polynomial.counit_surjective (R : Type u_3) [comm_ring R] :
function.surjective ⇑(mv_polynomial.counit R)
source
theorem mv_polynomial.counit_nat_surjective (A : Type u_1) [comm_semiring A] :
function.surjective ⇑(mv_polynomial.counit_nat A)
source
theorem mv_polynomial.counit_C (R : Type u_3) [comm_ring R] (n : ℤ) :
⇑(mv_polynomial.counit R) (⇑mv_polynomial.C n) = ↑n
source
theorem mv_polynomial.counit_nat_C (A : Type u_1) [comm_semiring A] (n : ℕ) :
⇑(mv_polynomial.counit_nat A) (⇑mv_polynomial.C n) = ↑n
source
@[simp]
theorem mv_polynomial.counit_X {R : Type u_3} [comm_ring R] (r : R) :
⇑(mv_polynomial.counit R) (mv_polynomial.X r) = r
source
@[simp]
theorem mv_polynomial.counit_nat_X {A : Type u_1} [comm_semiring A] (a : A) :
⇑(mv_polynomial.counit_nat A) (mv_polynomial.X a) = a