Documentation

Mathlib.Data.MvPolynomial.Equiv

Equivalences between polynomial rings #

This file establishes a number of equivalences between polynomial rings, based on equivalences between the underlying types.

Notation #

As in other polynomial files, we typically use the notation:

Tags #

equivalence, isomorphism, morphism, ring hom, hom

@[simp]
theorem MvPolynomial.pUnitAlgEquiv_apply (R : Type u) [CommSemiring R] (p : MvPolynomial PUnit.{u_2 + 1} R) :
↑(MvPolynomial.pUnitAlgEquiv R) p = MvPolynomial.eval₂ Polynomial.C (fun x => Polynomial.X) p

The ring isomorphism between multivariable polynomials in a single variable and polynomials over the ground ring.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem MvPolynomial.mapEquiv_apply {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) (a : MvPolynomial σ S₁) :
    ↑(MvPolynomial.mapEquiv σ e) a = ↑(MvPolynomial.map e) a
    def MvPolynomial.mapEquiv {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) :

    If e : A ≃+* B is an isomorphism of rings, then so is map e.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem MvPolynomial.mapEquiv_symm {S₁ : Type v} {S₂ : Type w} (σ : Type u_1) [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) :
      @[simp]
      theorem MvPolynomial.mapEquiv_trans {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} (σ : Type u_1) [CommSemiring S₁] [CommSemiring S₂] [CommSemiring S₃] (e : S₁ ≃+* S₂) (f : S₂ ≃+* S₃) :
      @[simp]
      theorem MvPolynomial.mapAlgEquiv_apply {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring A₁] [CommSemiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (a : MvPolynomial σ A₁) :
      def MvPolynomial.mapAlgEquiv {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring A₁] [CommSemiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :

      If e : A ≃ₐ[R] B is an isomorphism of R-algebras, then so is map e.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem MvPolynomial.mapAlgEquiv_refl {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} [CommSemiring A₁] [Algebra R A₁] :
        MvPolynomial.mapAlgEquiv σ AlgEquiv.refl = AlgEquiv.refl
        @[simp]
        theorem MvPolynomial.mapAlgEquiv_symm {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring A₁] [CommSemiring A₂] [Algebra R A₁] [Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
        @[simp]
        theorem MvPolynomial.mapAlgEquiv_trans {R : Type u} (σ : Type u_1) [CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [CommSemiring A₁] [CommSemiring A₂] [CommSemiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃) :
        def MvPolynomial.sumToIter (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
        MvPolynomial (S₁ S₂) R →+* MvPolynomial S₁ (MvPolynomial S₂ R)

        The function from multivariable polynomials in a sum of two types, to multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.

        See sumRingEquiv for the ring isomorphism.

        Equations
        Instances For
          @[simp]
          theorem MvPolynomial.sumToIter_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (a : R) :
          ↑(MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.C a) = MvPolynomial.C (MvPolynomial.C a)
          @[simp]
          theorem MvPolynomial.sumToIter_Xl (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (b : S₁) :
          @[simp]
          theorem MvPolynomial.sumToIter_Xr (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (c : S₂) :
          ↑(MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.X (Sum.inr c)) = MvPolynomial.C (MvPolynomial.X c)
          def MvPolynomial.iterToSum (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
          MvPolynomial S₁ (MvPolynomial S₂ R) →+* MvPolynomial (S₁ S₂) R

          The function from multivariable polynomials in one type, with coefficients in multivariable polynomials in another type, to multivariable polynomials in the sum of the two types.

          See sumRingEquiv for the ring isomorphism.

          Equations
          Instances For
            theorem MvPolynomial.iterToSum_C_C (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (a : R) :
            ↑(MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.C (MvPolynomial.C a)) = MvPolynomial.C a
            theorem MvPolynomial.iterToSum_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (b : S₁) :
            theorem MvPolynomial.iterToSum_C_X (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] (c : S₂) :
            ↑(MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.C (MvPolynomial.X c)) = MvPolynomial.X (Sum.inr c)
            @[simp]
            theorem MvPolynomial.isEmptyAlgEquiv_symm_apply_toFun (R : Type u) (σ : Type u_1) [CommSemiring R] [he : IsEmpty σ] (a : R) (j : σ →₀ ) :
            @[simp]
            theorem MvPolynomial.isEmptyAlgEquiv_apply (R : Type u) (σ : Type u_1) [CommSemiring R] [he : IsEmpty σ] (a : MvPolynomial σ R) :
            @[simp]
            theorem MvPolynomial.isEmptyAlgEquiv_symm_apply_support (R : Type u) (σ : Type u_1) [CommSemiring R] [he : IsEmpty σ] (a : R) :
            (↑(AlgEquiv.symm (MvPolynomial.isEmptyAlgEquiv R σ)) a).support = if a = 0 then else {0}
            def MvPolynomial.isEmptyAlgEquiv (R : Type u) (σ : Type u_1) [CommSemiring R] [he : IsEmpty σ] :

            The algebra isomorphism between multivariable polynomials in no variables and the ground ring.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem MvPolynomial.isEmptyRingEquiv_apply (R : Type u) (σ : Type u_1) [CommSemiring R] [IsEmpty σ] (a : MvPolynomial σ R) :
              ↑(MvPolynomial.isEmptyRingEquiv R σ) a = ↑(MvPolynomial.aeval fun a => IsEmpty.elim inst✝ a) a
              @[simp]
              theorem MvPolynomial.isEmptyRingEquiv_symm_apply_support (R : Type u) (σ : Type u_1) [CommSemiring R] [IsEmpty σ] (a : R) :
              (↑(RingEquiv.symm (MvPolynomial.isEmptyRingEquiv R σ)) a).support = if a = 0 then else {0}
              @[simp]
              theorem MvPolynomial.isEmptyRingEquiv_symm_apply_toFun (R : Type u) (σ : Type u_1) [CommSemiring R] [IsEmpty σ] (a : R) (j : σ →₀ ) :

              The ring isomorphism between multivariable polynomials in no variables and the ground ring.

              Equations
              Instances For
                @[simp]
                theorem MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [CommSemiring R] [CommSemiring S₃] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : RingHom.comp (RingHom.comp f g) MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g (MvPolynomial.X n)) = MvPolynomial.X n) (hgfC : RingHom.comp (RingHom.comp g f) MvPolynomial.C = MvPolynomial.C) (hgfX : ∀ (n : S₁), g (f (MvPolynomial.X n)) = MvPolynomial.X n) (a : MvPolynomial S₂ S₃) :
                ↑(RingEquiv.symm (MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX)) a = g a
                @[simp]
                theorem MvPolynomial.mvPolynomialEquivMvPolynomial_apply (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [CommSemiring R] [CommSemiring S₃] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : RingHom.comp (RingHom.comp f g) MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g (MvPolynomial.X n)) = MvPolynomial.X n) (hgfC : RingHom.comp (RingHom.comp g f) MvPolynomial.C = MvPolynomial.C) (hgfX : ∀ (n : S₁), g (f (MvPolynomial.X n)) = MvPolynomial.X n) (a : MvPolynomial S₁ R) :
                ↑(MvPolynomial.mvPolynomialEquivMvPolynomial R S₁ S₂ S₃ f g hfgC hfgX hgfC hgfX) a = f a
                def MvPolynomial.mvPolynomialEquivMvPolynomial (R : Type u) (S₁ : Type v) (S₂ : Type w) (S₃ : Type x) [CommSemiring R] [CommSemiring S₃] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : RingHom.comp (RingHom.comp f g) MvPolynomial.C = MvPolynomial.C) (hfgX : ∀ (n : S₂), f (g (MvPolynomial.X n)) = MvPolynomial.X n) (hgfC : RingHom.comp (RingHom.comp g f) MvPolynomial.C = MvPolynomial.C) (hgfX : ∀ (n : S₁), g (f (MvPolynomial.X n)) = MvPolynomial.X n) :

                A helper function for sumRingEquiv.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def MvPolynomial.sumRingEquiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
                  MvPolynomial (S₁ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)

                  The ring isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def MvPolynomial.sumAlgEquiv (R : Type u) (S₁ : Type v) (S₂ : Type w) [CommSemiring R] :
                    MvPolynomial (S₁ S₂) R ≃ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R)

                    The algebra isomorphism between multivariable polynomials in a sum of two types, and multivariable polynomials in one of the types, with coefficients in multivariable polynomials in the other type.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem MvPolynomial.optionEquivLeft_apply (R : Type u) (S₁ : Type v) [CommSemiring R] (a : MvPolynomial (Option S₁) R) :
                      ↑(MvPolynomial.optionEquivLeft R S₁) a = ↑(MvPolynomial.aeval fun o => match o, Polynomial.X, fun s => Polynomial.C (MvPolynomial.X s) with | some x, x_1, f => f x | none, y, x => y) a

                      The algebra isomorphism between multivariable polynomials in Option S₁ and polynomials with coefficients in MvPolynomial S₁ R.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The algebra isomorphism between multivariable polynomials in Option S₁ and multivariable polynomials with coefficients in polynomials.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The algebra isomorphism between multivariable polynomials in Fin (n + 1) and polynomials over multivariable polynomials in Fin n.

                          Equations
                          Instances For
                            theorem MvPolynomial.finSuccEquiv_eq (R : Type u) [CommSemiring R] (n : ) :
                            ↑(MvPolynomial.finSuccEquiv R n) = MvPolynomial.eval₂Hom (RingHom.comp Polynomial.C MvPolynomial.C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (MvPolynomial.X k)) i
                            @[simp]
                            theorem MvPolynomial.finSuccEquiv_apply (R : Type u) [CommSemiring R] (n : ) (p : MvPolynomial (Fin (n + 1)) R) :
                            ↑(MvPolynomial.finSuccEquiv R n) p = ↑(MvPolynomial.eval₂Hom (RingHom.comp Polynomial.C MvPolynomial.C) fun i => Fin.cases Polynomial.X (fun k => Polynomial.C (MvPolynomial.X k)) i) p
                            theorem MvPolynomial.finSuccEquiv_comp_C_eq_C {R : Type u} [CommSemiring R] (n : ) :
                            RingHom.comp (↑(AlgEquiv.symm (MvPolynomial.finSuccEquiv R n))) (RingHom.comp Polynomial.C MvPolynomial.C) = MvPolynomial.C

                            The coefficient of m in the i-th coefficient of finSuccEquiv R n f equals the coefficient of Finsupp.cons i m in f.