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) [CommSemiring A] [CommSemiring B] [Algebra A B] : MvPolynomial B A →ₐ[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 = ℕ.

@[simp]

theorem MvPolynomial.ACounit_X (A : Type u_1) {B : Type u_2} [CommSemiring A] [CommSemiring B] [Algebra A B] (b : B) : (ACounit A B) (X b) = b

theorem MvPolynomial.ACounit_C {A : Type u_1} (B : Type u_2) [CommSemiring A] [CommSemiring B] [Algebra A B] (a : A) : (ACounit A B) (C a) = (algebraMap A B) a

theorem MvPolynomial.ACounit_surjective (A : Type u_1) (B : Type u_2) [CommSemiring A] [CommSemiring B] [Algebra A B] : Function.Surjective ⇑(ACounit A B)

noncomputable def MvPolynomial.counit (R : Type u_3) [CommRing R] : MvPolynomial R ℤ →+* R

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

noncomputable def MvPolynomial.counitNat (A : Type u_1) [CommSemiring A] : MvPolynomial A ℕ →+* A

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

theorem MvPolynomial.counit_surjective (R : Type u_3) [CommRing R] : Function.Surjective ⇑(counit R)

theorem MvPolynomial.counitNat_surjective (A : Type u_1) [CommSemiring A] : Function.Surjective ⇑(counitNat A)

theorem MvPolynomial.counit_C (R : Type u_3) [CommRing R] (n : ℤ) : (counit R) (C n) = ↑n

theorem MvPolynomial.counitNat_C (A : Type u_1) [CommSemiring A] (n : ℕ) : (counitNat A) (C n) = ↑n

@[simp]

theorem MvPolynomial.counit_X {R : Type u_3} [CommRing R] (r : R) : (counit R) (X r) = r

@[simp]

theorem MvPolynomial.counitNat_X {A : Type u_1} [CommSemiring A] (a : A) : (counitNat A) (X a) = a