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 #

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

Equations
Instances For
    @[simp]
    theorem MvPolynomial.ACounit_X (A : Type u_1) {B : Type u_2} [CommSemiring A] [CommSemiring B] [Algebra A B] (b : B) :
    @[simp]
    theorem MvPolynomial.ACounit_C {A : Type u_1} (B : Type u_2) [CommSemiring A] [CommSemiring B] [Algebra A B] (a : A) :
    (MvPolynomial.ACounit A B) (MvPolynomial.C a) = (algebraMap A B) a
    noncomputable def MvPolynomial.counit (R : Type u_3) [CommRing 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 = ℕ.

    Equations
    Instances For
      noncomputable def MvPolynomial.counitNat (A : Type u_1) [CommSemiring 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 = ℤ.

      Equations
      Instances For
        theorem MvPolynomial.counit_C (R : Type u_3) [CommRing R] (n : ) :
        (MvPolynomial.counit R) (MvPolynomial.C n) = n
        theorem MvPolynomial.counitNat_C (A : Type u_1) [CommSemiring A] (n : ) :
        (MvPolynomial.counitNat A) (MvPolynomial.C n) = n
        @[simp]
        theorem MvPolynomial.counit_X {R : Type u_3} [CommRing R] (r : R) :