Mathlib.Algebra.MvPolynomial.Equiv

MvPolynomial.pUnitAlgEquiv definition

: MvPolynomial PUnit R ≃ₐ[R] R[X]

Full source

/-- The ring isomorphism between multivariable polynomials in a single variable and
polynomials over the ground ring.
-/
@[simps]
def pUnitAlgEquiv : MvPolynomialMvPolynomial PUnit R ≃ₐ[R] R[X] where
  toFun := eval₂ Polynomial.C fun _ => Polynomial.X
  invFun := Polynomial.eval₂ MvPolynomial.C (X PUnit.unit)
  left_inv := by
    let f : R[X]R[X] →+* MvPolynomial PUnit R := Polynomial.eval₂RingHom MvPolynomial.C (X PUnit.unit)
    let g : MvPolynomialMvPolynomial PUnit R →+* R[X] := eval₂Hom Polynomial.C fun _ => Polynomial.X
    show ∀ p, f.comp g p = p
    apply is_id
    · ext a
      dsimp [f, g]
      rw [eval₂_C, Polynomial.eval₂_C]
    · rintro ⟨⟩
      dsimp [f, g]
      rw [eval₂_X, Polynomial.eval₂_X]
  right_inv p :=
    Polynomial.induction_on p (fun a => by rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C])
    (fun p q hp hq => by rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]) fun p n _ => by
      rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,
        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]
  map_mul' _ _ := eval₂_mul _ _
  map_add' _ _ := eval₂_add _ _
  commutes' _ := eval₂_C _ _ _

Isomorphism between univariate and single-variable multivariate polynomial rings

Informal description

The ring isomorphism between the multivariate polynomial ring with variables indexed by the unit type $\text{PUnit}$ (i.e., polynomials in a single variable) and the univariate polynomial ring $R[X]$. More precisely, the isomorphism is given by: - The forward map evaluates a multivariate polynomial in $\text{MvPolynomial}(\text{PUnit}, R)$ by treating the single variable as $X$ and coefficients via the canonical embedding $\text{Polynomial.C}$. - The inverse map evaluates a univariate polynomial in $R[X]$ by treating $X$ as the single variable $\text{X PUnit.unit}$ in the multivariate polynomial ring and coefficients via the canonical embedding $\text{MvPolynomial.C}$. This isomorphism preserves the ring structure and is compatible with the $R$-algebra structure.

MvPolynomial.pUnitAlgEquiv_monomial theorem

 {d : PUnit →₀ ℕ} {r : R} : MvPolynomial.pUnitAlgEquiv R (MvPolynomial.monomial d r) = Polynomial.monomial (d ()) r

Full source

theorem pUnitAlgEquiv_monomial {d : PUnitPUnit →₀ ℕ} {r : R} :
    MvPolynomial.pUnitAlgEquiv R (MvPolynomial.monomial d r)
      = Polynomial.monomial (d ()) r := by
  simp [Polynomial.C_mul_X_pow_eq_monomial]

Monomial correspondence in the isomorphism between single-variable multivariate and univariate polynomial rings

Informal description

Let $R$ be a commutative semiring. For any finitely supported function $d : \text{PUnit} \to \mathbb{N}$ and any coefficient $r \in R$, the image of the monomial $r X^d$ under the algebra isomorphism $\text{MvPolynomial}(\text{PUnit}, R) \simeq R[X]$ is the univariate monomial $r X^{d()}$, where $d()$ denotes the value of $d$ at the unique element of $\text{PUnit}$.

MvPolynomial.pUnitAlgEquiv_symm_monomial theorem

 {d : PUnit →₀ ℕ} {r : R} :
  (MvPolynomial.pUnitAlgEquiv R).symm (Polynomial.monomial (d ()) r) = MvPolynomial.monomial d r

Full source

theorem pUnitAlgEquiv_symm_monomial {d : PUnitPUnit →₀ ℕ} {r : R} :
    (MvPolynomial.pUnitAlgEquiv R).symm (Polynomial.monomial (d ()) r)
      = MvPolynomial.monomial d r := by
  simp [MvPolynomial.monomial_eq]

Inverse of $\text{MvPolynomial}(\text{PUnit}, R) \simeq R[X]$ maps univariate monomial to multivariate monomial

Informal description

For any finitely supported function $d : \text{PUnit} \to \mathbb{N}$ and any coefficient $r \in R$, the inverse of the algebra isomorphism $\text{MvPolynomial}(\text{PUnit}, R) \simeq R[X]$ maps the univariate monomial $r X^{d()}$ to the multivariate monomial $r X^d$ in $\text{MvPolynomial}(\text{PUnit}, R)$, where $d()$ denotes the value of $d$ at the unique element of $\text{PUnit}$.

MvPolynomial.mapEquiv definition

[CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) : MvPolynomial σ S₁ ≃+* MvPolynomial σ S₂

Full source

/-- If `e : A ≃+* B` is an isomorphism of rings, then so is `map e`. -/
@[simps apply]
def mapEquiv [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) :
    MvPolynomialMvPolynomial σ S₁ ≃+* MvPolynomial σ S₂ :=
  { map (e : S₁ →+* S₂) with
    toFun := map (e : S₁ →+* S₂)
    invFun := map (e.symm : S₂ →+* S₁)
    left_inv := map_leftInverse e.left_inv
    right_inv := map_rightInverse e.right_inv }

Ring isomorphism of multivariate polynomial rings induced by a coefficient ring isomorphism

Informal description

Given a ring isomorphism $ e : S_1 \simeq+* S_2 $ between two commutative semirings $ S_1 $ and $ S_2 $, the function `mapEquiv e` is a ring isomorphism between the multivariate polynomial rings $ \text{MvPolynomial}(\sigma, S_1) $ and $ \text{MvPolynomial}(\sigma, S_2) $. This isomorphism is constructed by applying $ e $ to each coefficient of the polynomial while keeping the variables unchanged, and its inverse is given by applying the inverse isomorphism $ e^{-1} $.

MvPolynomial.mapEquiv_refl theorem

: mapEquiv σ (RingEquiv.refl R) = RingEquiv.refl _

Full source

@[simp]
theorem mapEquiv_refl : mapEquiv σ (RingEquiv.refl R) = RingEquiv.refl _ :=
  RingEquiv.ext map_id

Identity Ring Equivalence Preserved Under `mapEquiv`

Informal description

The ring isomorphism `mapEquiv` applied to the identity ring equivalence $\text{refl}_R$ on the coefficient ring $R$ yields the identity ring equivalence on the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$. That is, \[ \text{mapEquiv}_\sigma(\text{refl}_R) = \text{refl}_{\text{MvPolynomial}(\sigma, R)}. \]

MvPolynomial.mapEquiv_symm theorem

[CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) : (mapEquiv σ e).symm = mapEquiv σ e.symm

Full source

@[simp]
theorem mapEquiv_symm [CommSemiring S₁] [CommSemiring S₂] (e : S₁ ≃+* S₂) :
    (mapEquiv σ e).symm = mapEquiv σ e.symm :=
  rfl

Inverse of Induced Polynomial Ring Isomorphism Equals Isomorphism Induced by Inverse

Informal description

Let $S_1$ and $S_2$ be commutative semirings and let $e: S_1 \simeq+* S_2$ be a ring isomorphism. Then the inverse of the induced isomorphism $\text{mapEquiv}_\sigma e : \text{MvPolynomial}(\sigma, S_1) \simeq+* \text{MvPolynomial}(\sigma, S_2)$ is equal to the isomorphism induced by the inverse of $e$, i.e., $(\text{mapEquiv}_\sigma e)^{-1} = \text{mapEquiv}_\sigma e^{-1}$.

MvPolynomial.mapEquiv_trans theorem

 [CommSemiring S₁] [CommSemiring S₂] [CommSemiring S₃] (e : S₁ ≃+* S₂) (f : S₂ ≃+* S₃) :
  (mapEquiv σ e).trans (mapEquiv σ f) = mapEquiv σ (e.trans f)

Full source

@[simp]
theorem mapEquiv_trans [CommSemiring S₁] [CommSemiring S₂] [CommSemiring S₃] (e : S₁ ≃+* S₂)
    (f : S₂ ≃+* S₃) : (mapEquiv σ e).trans (mapEquiv σ f) = mapEquiv σ (e.trans f) :=
  RingEquiv.ext fun p => by
    simp only [RingEquiv.coe_trans, comp_apply, mapEquiv_apply, RingEquiv.coe_ringHom_trans,
      map_map]

Composition of Induced Polynomial Ring Isomorphisms Equals Isomorphism Induced by Composition

Informal description

Let $S_1$, $S_2$, and $S_3$ be commutative semirings, and let $e \colon S_1 \simeq+* S_2$ and $f \colon S_2 \simeq+* S_3$ be ring isomorphisms. Then the composition of the induced isomorphisms $\text{mapEquiv}_\sigma e \colon \text{MvPolynomial}(\sigma, S_1) \simeq+* \text{MvPolynomial}(\sigma, S_2)$ and $\text{mapEquiv}_\sigma f \colon \text{MvPolynomial}(\sigma, S_2) \simeq+* \text{MvPolynomial}(\sigma, S_3)$ is equal to the isomorphism induced by the composition $e \circ f \colon S_1 \simeq+* S_3$. That is, \[ (\text{mapEquiv}_\sigma e) \circ (\text{mapEquiv}_\sigma f) = \text{mapEquiv}_\sigma (e \circ f). \]

MvPolynomial.mapAlgEquiv definition

(e : A₁ ≃ₐ[R] A₂) : MvPolynomial σ A₁ ≃ₐ[R] MvPolynomial σ A₂

Full source

/-- If `e : A ≃ₐ[R] B` is an isomorphism of `R`-algebras, then so is `map e`. -/
@[simps apply]
def mapAlgEquiv (e : A₁ ≃ₐ[R] A₂) : MvPolynomialMvPolynomial σ A₁ ≃ₐ[R] MvPolynomial σ A₂ :=
  { mapAlgHom (e : A₁ →ₐ[R] A₂), mapEquiv σ (e : A₁ ≃+* A₂) with toFun := map (e : A₁ →+* A₂) }

$R$-algebra isomorphism of multivariate polynomial rings induced by a coefficient $R$-algebra isomorphism

Informal description

Given an $R$-algebra isomorphism $e : A_1 \simeq_{R} A_2$, the function `mapAlgEquiv σ e` is an $R$-algebra isomorphism between the multivariate polynomial rings $\text{MvPolynomial}(\sigma, A_1)$ and $\text{MvPolynomial}(\sigma, A_2)$. This isomorphism is constructed by applying $e$ to each coefficient of the polynomial while keeping the variables unchanged, and its inverse is given by applying the inverse isomorphism $e^{-1}$.

MvPolynomial.mapAlgEquiv_refl theorem

: mapAlgEquiv σ (AlgEquiv.refl : A₁ ≃ₐ[R] A₁) = AlgEquiv.refl

Full source

@[simp]
theorem mapAlgEquiv_refl : mapAlgEquiv σ (AlgEquiv.refl : A₁ ≃ₐ[R] A₁) = AlgEquiv.refl :=
  AlgEquiv.ext map_id

Reflexivity of Multivariate Polynomial Ring Isomorphism Induced by Reflexive Coefficient Isomorphism

Informal description

The $R$-algebra isomorphism `mapAlgEquiv σ` applied to the reflexive $R$-algebra isomorphism $\text{AlgEquiv.refl} \colon A_1 \simeq_{R} A_1$ yields the reflexive $R$-algebra isomorphism on the multivariate polynomial ring $\text{MvPolynomial}(\sigma, A_1)$. In other words, \[ \text{mapAlgEquiv}\, \sigma\, \text{AlgEquiv.refl} = \text{AlgEquiv.refl}. \]

MvPolynomial.mapAlgEquiv_symm theorem

(e : A₁ ≃ₐ[R] A₂) : (mapAlgEquiv σ e).symm = mapAlgEquiv σ e.symm

Full source

@[simp]
theorem mapAlgEquiv_symm (e : A₁ ≃ₐ[R] A₂) : (mapAlgEquiv σ e).symm = mapAlgEquiv σ e.symm :=
  rfl

Inverse of Induced Polynomial Ring Isomorphism Equals Isomorphism Induced by Inverse

Informal description

Given an $R$-algebra isomorphism $e : A_1 \simeq_{R} A_2$, the inverse of the induced $R$-algebra isomorphism $\text{MvPolynomial}(\sigma, A_1) \simeq_{R} \text{MvPolynomial}(\sigma, A_2)$ is equal to the $R$-algebra isomorphism induced by the inverse $e^{-1} : A_2 \simeq_{R} A_1$. In other words, $(\text{mapAlgEquiv}\ \sigma\ e)^{-1} = \text{mapAlgEquiv}\ \sigma\ e^{-1}$.

MvPolynomial.mapAlgEquiv_trans theorem

 (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃) : (mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f)

Full source

@[simp]
theorem mapAlgEquiv_trans (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃) :
    (mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f) := by
  ext
  simp only [AlgEquiv.trans_apply, mapAlgEquiv_apply, map_map]
  rfl

Composition of Induced Polynomial Ring Isomorphisms Equals Isomorphism Induced by Composition

Informal description

Let $R$ be a commutative semiring, and let $A_1$, $A_2$, $A_3$ be $R$-algebras. Given $R$-algebra isomorphisms $e \colon A_1 \simeq_{R} A_2$ and $f \colon A_2 \simeq_{R} A_3$, the composition of the induced isomorphisms $\text{mapAlgEquiv}\, \sigma\, e$ and $\text{mapAlgEquiv}\, \sigma\, f$ on the multivariate polynomial rings is equal to the isomorphism induced by the composition $e \circ f$. That is, \[ (\text{mapAlgEquiv}\, \sigma\, e) \circ (\text{mapAlgEquiv}\, \sigma\, f) = \text{mapAlgEquiv}\, \sigma\, (e \circ f). \]

MvPolynomial.eval₂_pUnitAlgEquiv_symm theorem

 {f : Polynomial R} {φ : R →+* S} {a : Unit → S} :
  ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ a = f.eval₂ φ (a ())

Full source

theorem eval₂_pUnitAlgEquiv_symm {f : Polynomial R} {φ : R →+* S} {a : Unit → S} :
    ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ a  =
      f.eval₂ φ (a ()) := by
  simp only [MvPolynomial.pUnitAlgEquiv_symm_apply]
  induction f using Polynomial.induction_on' with
  | add f g hf hg => simp [hf, hg]
  | monomial n r => simp

Evaluation Compatibility of Univariate-to-Multivariate Polynomial Isomorphism

Informal description

Let $R$ and $S$ be commutative semirings, and let $\varphi: R \to S$ be a semiring homomorphism. For any univariate polynomial $f \in R[X]$ and any evaluation function $a: \text{Unit} \to S$, the evaluation of the multivariate polynomial corresponding to $f$ under the inverse isomorphism $\text{pUnitAlgEquiv}^{-1}$ satisfies: \[ \text{eval}_2(\varphi, a, \text{pUnitAlgEquiv}^{-1}(f)) = \text{eval}_2(\varphi, a(\text{unit}), f) \] where $\text{unit}$ is the unique element of the unit type $\text{Unit}$.

MvPolynomial.eval₂_const_pUnitAlgEquiv_symm theorem

 {f : Polynomial R} {φ : R →+* S} {a : S} :
  ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ (fun _ ↦ a) = f.eval₂ φ a

Full source

theorem eval₂_const_pUnitAlgEquiv_symm {f : Polynomial R} {φ : R →+* S} {a : S} :
    ((MvPolynomial.pUnitAlgEquiv R).symm f : MvPolynomial Unit R).eval₂ φ (fun _ ↦ a)  =
      f.eval₂ φ a := by
  rw [eval₂_pUnitAlgEquiv_symm]

Evaluation Compatibility of Constant Function with Univariate-to-Multivariate Polynomial Isomorphism

Informal description

Let $R$ and $S$ be commutative semirings, and let $\varphi: R \to S$ be a semiring homomorphism. For any univariate polynomial $f \in R[X]$ and any element $a \in S$, the evaluation of the multivariate polynomial corresponding to $f$ under the inverse isomorphism $\text{pUnitAlgEquiv}^{-1}$ satisfies: \[ \text{eval}_2(\varphi, \lambda \_. a, \text{pUnitAlgEquiv}^{-1}(f)) = \text{eval}_2(\varphi, a, f) \] where $\lambda \_. a$ denotes the constant function from $\text{Unit}$ to $S$ that always returns $a$.

MvPolynomial.eval₂_pUnitAlgEquiv theorem

 {f : MvPolynomial PUnit R} {φ : R →+* S} {a : PUnit → S} :
  ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ (a default) = f.eval₂ φ a

Full source

theorem eval₂_pUnitAlgEquiv {f : MvPolynomial PUnit R} {φ : R →+* S} {a : PUnit → S} :
    ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ (a default) = f.eval₂ φ a := by
  simp only [MvPolynomial.pUnitAlgEquiv_apply]
  induction f using MvPolynomial.induction_on' with
  | monomial d r => simp
  | add f g hf hg => simp [hf, hg]

Compatibility of Evaluation with Univariate-Multivariate Polynomial Isomorphism

Informal description

Let $R$ and $S$ be commutative semirings, and let $\phi: R \to S$ be a semiring homomorphism. For any multivariate polynomial $f \in R[X_{\text{unit}}]$ (where $\text{unit}$ is the unique element of $\text{PUnit}$) and any evaluation map $a: \text{PUnit} \to S$, the evaluation of the univariate polynomial corresponding to $f$ under the isomorphism $\text{MvPolynomial}(\text{PUnit}, R) \cong R[X]$ satisfies: \[ \text{eval}_2(\phi, a(\text{default}), \text{pUnitAlgEquiv}(f)) = \text{eval}_2(\phi, a, f) \] where $\text{default}$ is the unique element of $\text{PUnit}$.

MvPolynomial.eval₂_const_pUnitAlgEquiv theorem

 {f : MvPolynomial PUnit R} {φ : R →+* S} {a : S} :
  ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ a = f.eval₂ φ (fun _ ↦ a)

Full source

theorem eval₂_const_pUnitAlgEquiv {f : MvPolynomial PUnit R} {φ : R →+* S} {a : S} :
    ((MvPolynomial.pUnitAlgEquiv R) f : Polynomial R).eval₂ φ a = f.eval₂ φ (fun _ ↦ a) := by
  rw [← eval₂_pUnitAlgEquiv]

Evaluation Compatibility for Constant Functions under Univariate-Multivariate Polynomial Isomorphism

Informal description

Let $R$ and $S$ be commutative semirings, $\phi: R \to S$ a semiring homomorphism, and $a \in S$. For any multivariate polynomial $f \in R[X_{\text{unit}}]$ (where $\text{unit}$ is the unique element of $\text{PUnit}$), the evaluation of its corresponding univariate polynomial under the isomorphism $\text{MvPolynomial}(\text{PUnit}, R) \cong R[X]$ satisfies: \[ \text{eval}_2(\phi, a, \text{pUnitAlgEquiv}(f)) = \text{eval}_2(\phi, (x \mapsto a), f) \] where the right side evaluates $f$ using the constant function $x \mapsto a$ for all variables.

MvPolynomial.sumToIter definition

: MvPolynomial (S₁ ⊕ S₂) R →+* MvPolynomial S₁ (MvPolynomial S₂ R)

Full source

/-- 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.
-/
def sumToIter : MvPolynomialMvPolynomial (S₁ ⊕ S₂) R →+* MvPolynomial S₁ (MvPolynomial S₂ R) :=
  eval₂Hom (C.comp C) fun bc => Sum.recOn bc X (CC ∘ X)

Decomposition of multivariate polynomials over a sum type

Informal description

The ring homomorphism from the multivariate polynomial ring over the sum type $S_1 \oplus S_2$ with coefficients in $R$ to the multivariate polynomial ring over $S_1$ with coefficients in the multivariate polynomial ring over $S_2$ with coefficients in $R$. More precisely, it maps: - A constant polynomial $a \in R$ to the constant polynomial $C(a)$ in $R[X_{S_1}, X_{S_2}]$, viewed as $R[X_{S_1}][X_{S_2}]$. - A variable $X_{\text{inl}(b)}$ (where $b \in S_1$) to the variable $X_b$ in $R[X_{S_1}][X_{S_2}]$. - A variable $X_{\text{inr}(c)}$ (where $c \in S_2$) to the constant polynomial $X_c$ in $R[X_{S_2}]$, viewed as an element of $R[X_{S_1}][X_{S_2}]$ via the embedding $C \circ X$.

MvPolynomial.sumToIter_C theorem

(a : R) : sumToIter R S₁ S₂ (C a) = C (C a)

Full source

@[simp]
theorem sumToIter_C (a : R) : sumToIter R S₁ S₂ (C a) = C (C a) :=
  eval₂_C _ _ a

Preservation of Constants under Sum-to-Iterated Polynomial Ring Homomorphism

Informal description

For any coefficient $a \in R$ in a commutative semiring $R$, the ring homomorphism `sumToIter` maps the constant polynomial $C(a)$ in the multivariate polynomial ring over $S_1 \oplus S_2$ to the constant polynomial $C(C(a))$ in the multivariate polynomial ring over $S_1$ with coefficients in the multivariate polynomial ring over $S_2$. In other words, the following diagram commutes for constants: \[ \text{sumToIter}(C(a)) = C(C(a)) \]

MvPolynomial.sumToIter_Xl theorem

(b : S₁) : sumToIter R S₁ S₂ (X (Sum.inl b)) = X b

Full source

@[simp]
theorem sumToIter_Xl (b : S₁) : sumToIter R S₁ S₂ (X (Sum.inl b)) = X b :=
  eval₂_X _ _ (Sum.inl b)

Mapping of left sum variables under polynomial ring equivalence

Informal description

For any element $b \in S_1$, the ring homomorphism `sumToIter` maps the monomial $X_{\text{inl}(b)}$ in the multivariate polynomial ring over $S_1 \oplus S_2$ to the monomial $X_b$ in the multivariate polynomial ring over $S_1$ with coefficients in $R[X_{S_2}]$.

MvPolynomial.sumToIter_Xr theorem

(c : S₂) : sumToIter R S₁ S₂ (X (Sum.inr c)) = C (X c)

Full source

@[simp]
theorem sumToIter_Xr (c : S₂) : sumToIter R S₁ S₂ (X (Sum.inr c)) = C (X c) :=
  eval₂_X _ _ (Sum.inr c)

Image of right injection monomial under sum-to-iterated polynomial ring homomorphism

Informal description

For any element $c \in S_2$, the ring homomorphism `sumToIter` maps the monomial $X_{\text{inr}(c)}$ in the multivariate polynomial ring over $S_1 \oplus S_2$ to the constant polynomial $C(X_c)$ in the multivariate polynomial ring over $S_1$ with coefficients in the multivariate polynomial ring over $S_2$.

MvPolynomial.iterToSum definition

: MvPolynomial S₁ (MvPolynomial S₂ R) →+* MvPolynomial (S₁ ⊕ S₂) R

Full source

/-- 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.
-/
def iterToSum : MvPolynomialMvPolynomial S₁ (MvPolynomial S₂ R) →+* MvPolynomial (S₁ ⊕ S₂) R :=
  eval₂Hom (eval₂Hom C (XX ∘ Sum.inr)) (XX ∘ Sum.inl)

Ring homomorphism from iterated to summed multivariate polynomial rings

Informal description

The ring homomorphism from the multivariate polynomial ring over $S_1$ with coefficients in the multivariate polynomial ring over $S_2$ with coefficients in $R$, to the multivariate polynomial ring over the sum type $S_1 \oplus S_2$ with coefficients in $R$. This homomorphism is constructed by evaluating the coefficients (which are themselves polynomials) using the embedding of $S_2$ variables into the sum type, and then evaluating the resulting polynomial using the embedding of $S_1$ variables into the sum type.

MvPolynomial.iterToSum_C_C theorem

(a : R) : iterToSum R S₁ S₂ (C (C a)) = C a

Full source

@[simp]
theorem iterToSum_C_C (a : R) : iterToSum R S₁ S₂ (C (C a)) = C a :=
  Eq.trans (eval₂_C _ _ (C a)) (eval₂_C _ _ _)

Double Constant Polynomial Maps to Single Constant under iterToSum

Informal description

For any coefficient $a \in R$, the ring homomorphism $\text{iterToSum}$ from the iterated multivariate polynomial ring $\text{MvPolynomial}(S_1, \text{MvPolynomial}(S_2, R))$ to the summed multivariate polynomial ring $\text{MvPolynomial}(S_1 \oplus S_2, R)$ maps the constant polynomial $C(C(a))$ to the constant polynomial $C(a)$. In other words, the double constant polynomial $C(C(a))$ in the iterated ring is mapped to the single constant polynomial $C(a)$ in the summed ring.

MvPolynomial.iterToSum_X theorem

(b : S₁) : iterToSum R S₁ S₂ (X b) = X (Sum.inl b)

Full source

@[simp]
theorem iterToSum_X (b : S₁) : iterToSum R S₁ S₂ (X b) = X (Sum.inl b) :=
  eval₂_X _ _ _

$\text{iterToSum}$ maps $X_b$ to $X_{\text{inl}(b)}$

Informal description

For any variable index $b \in S_1$, the ring homomorphism $\text{iterToSum}$ maps the monomial $X_b$ in the iterated polynomial ring $\text{MvPolynomial}(S_1, \text{MvPolynomial}(S_2, R))$ to the monomial $X_{\text{Sum.inl}(b)}$ in the summed polynomial ring $\text{MvPolynomial}(S_1 \oplus S_2, R)$.

MvPolynomial.iterToSum_C_X theorem

(c : S₂) : iterToSum R S₁ S₂ (C (X c)) = X (Sum.inr c)

Full source

@[simp]
theorem iterToSum_C_X (c : S₂) : iterToSum R S₁ S₂ (C (X c)) = X (Sum.inr c) :=
  Eq.trans (eval₂_C _ _ (X c)) (eval₂_X _ _ _)

Image of Constant Variable Polynomial under Iterated-to-Sum Homomorphism: $\text{iterToSum}(C(X_c)) = X_{\text{inr}(c)}$

Informal description

For any commutative semiring $R$ and types $S_1$ and $S_2$, the ring homomorphism $\text{iterToSum}$ from the iterated multivariate polynomial ring $\text{MvPolynomial}(S_1, \text{MvPolynomial}(S_2, R))$ to the summed multivariate polynomial ring $\text{MvPolynomial}(S_1 \oplus S_2, R)$ satisfies the following property: for any variable $c \in S_2$, the image of the constant polynomial $C(X_c)$ (where $X_c$ is the degree one monomial in $\text{MvPolynomial}(S_2, R)$) under $\text{iterToSum}$ is equal to the degree one monomial $X_{\text{Sum.inr}(c)}$ in $\text{MvPolynomial}(S_1 \oplus S_2, R)$.

MvPolynomial.isEmptyAlgEquiv definition

: MvPolynomial σ R ≃ₐ[R] R

Full source

/-- The algebra isomorphism between multivariable polynomials in no variables
and the ground ring. -/
@[simps! apply]
def isEmptyAlgEquiv : MvPolynomialMvPolynomial σ R ≃ₐ[R] R :=
  .ofAlgHom (aeval isEmptyElim) (Algebra.ofId _ _) (by ext) (by ext i m; exact isEmptyElim i)

Algebra isomorphism between multivariate polynomials in no variables and the base ring

Informal description

The algebra isomorphism between the multivariate polynomial ring with variables indexed by an empty type $\sigma$ and the ground commutative semiring $R$. Specifically, it maps any polynomial in $\text{MvPolynomial}(\sigma, R)$ to its constant term in $R$, and conversely, embeds any element of $R$ as a constant polynomial. This isomorphism is constructed as an algebra homomorphism in both directions, with the composition in each direction being the identity. The forward direction is given by evaluating the polynomial (which has no variables to substitute), and the backward direction is the canonical embedding of $R$ into the polynomial ring.

MvPolynomial.aeval_injective_iff_of_isEmpty theorem

 [CommSemiring S₁] [Algebra R S₁] {f : σ → S₁} :
  Function.Injective (aeval f : MvPolynomial σ R →ₐ[R] S₁) ↔ Function.Injective (algebraMap R S₁)

Full source

@[simp]
lemma aeval_injective_iff_of_isEmpty [CommSemiring S₁] [Algebra R S₁] {f : σ → S₁} :
    Function.InjectiveFunction.Injective (aeval f : MvPolynomial σ R →ₐ[R] S₁) ↔
      Function.Injective (algebraMap R S₁) := by
  have : aeval f = (Algebra.ofId R S₁).comp (@isEmptyAlgEquiv R σ _ _).toAlgHom := by
    ext i
    exact IsEmpty.elim' ‹IsEmpty σ› i
  rw [this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R σ _ _).bijective]
  rfl

Injectivity of Evaluation Homomorphism for Empty Variable Set in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, $S₁$ a commutative semiring with an $R$-algebra structure, and $\sigma$ an empty type. For any function $f \colon \sigma \to S₁$, the evaluation homomorphism $\text{aeval}(f) \colon R[X_i : i \in \sigma] \to S₁$ is injective if and only if the canonical algebra map $R \to S₁$ is injective.

MvPolynomial.isEmptyRingEquiv definition

: MvPolynomial σ R ≃+* R

Full source

/-- The ring isomorphism between multivariable polynomials in no variables
and the ground ring. -/
@[simps! apply]
def isEmptyRingEquiv : MvPolynomialMvPolynomial σ R ≃+* R := (isEmptyAlgEquiv R σ).toRingEquiv

Ring isomorphism between zero-variable polynomials and the base ring

Informal description

The ring isomorphism between the multivariate polynomial ring with variables indexed by an empty type $\sigma$ and the ground commutative semiring $R$. Specifically, it maps any polynomial in $\text{MvPolynomial}(\sigma, R)$ to its constant term in $R$, and conversely, embeds any element of $R$ as a constant polynomial. This isomorphism is constructed as a ring homomorphism in both directions, with the composition in each direction being the identity. The forward direction is given by evaluating the polynomial (which has no variables to substitute), and the backward direction is the canonical embedding of $R$ into the polynomial ring.

MvPolynomial.isEmptyRingEquiv_symm_toRingHom theorem

: (isEmptyRingEquiv R σ).symm.toRingHom = C

Full source

lemma isEmptyRingEquiv_symm_toRingHom : (isEmptyRingEquiv R σ).symm.toRingHom = C := rfl

Inverse of Zero-Variable Polynomial Isomorphism is Constant Embedding

Informal description

The ring homomorphism obtained as the inverse of the isomorphism $\text{MvPolynomial}(\sigma, R) \simeq R$ (when $\sigma$ is empty) is equal to the constant polynomial embedding $C \colon R \to \text{MvPolynomial}(\sigma, R)$.

MvPolynomial.isEmptyRingEquiv_symm_apply theorem

(r : R) : (isEmptyRingEquiv R σ).symm r = C r

Full source

@[simp] lemma isEmptyRingEquiv_symm_apply (r : R) : (isEmptyRingEquiv R σ).symm r = C r := rfl

Inverse of Zero-Variable Polynomial Isomorphism Maps to Constant Polynomial

Informal description

For any element $r$ in a commutative semiring $R$ and an empty type $\sigma$, the inverse of the ring isomorphism $\text{MvPolynomial}(\sigma, R) \simeq R$ maps $r$ to the constant polynomial $C(r)$.

MvPolynomial.isEmptyRingEquiv_eq_coeff_zero theorem

{σ R : Type*} [CommSemiring R] [IsEmpty σ] {x} : isEmptyRingEquiv R σ x = x.coeff 0

Full source

lemma isEmptyRingEquiv_eq_coeff_zero {σ R : Type*} [CommSemiring R] [IsEmpty σ] {x} :
    isEmptyRingEquiv R σ x = x.coeff 0 := by
  obtain ⟨x, rfl⟩ := (isEmptyRingEquiv R σ).symm.surjective x; simp

Isomorphism between zero-variable polynomials and base ring evaluates to constant term

Informal description

For any commutative semiring $R$ and any empty type $\sigma$, the ring isomorphism $\text{MvPolynomial}(\sigma, R) \simeq R$ maps a polynomial $x$ to its constant term (the coefficient of the zero monomial). That is, $\text{isEmptyRingEquiv}_{R,\sigma}(x) = \text{coeff}_0(x)$.

MvPolynomial.mvPolynomialEquivMvPolynomial definition

 [CommSemiring S₃] (f : MvPolynomial S₁ R →+* MvPolynomial S₂ S₃) (g : MvPolynomial S₂ S₃ →+* MvPolynomial S₁ R)
  (hfgC : (f.comp g).comp C = C) (hfgX : ∀ n, f (g (X n)) = X n) (hgfC : (g.comp f).comp C = C)
  (hgfX : ∀ n, g (f (X n)) = X n) : MvPolynomial S₁ R ≃+* MvPolynomial S₂ S₃

Full source

/-- A helper function for `sumRingEquiv`. -/
@[simps]
def mvPolynomialEquivMvPolynomial [CommSemiring S₃] (f : MvPolynomialMvPolynomial S₁ R →+* MvPolynomial S₂ S₃)
    (g : MvPolynomialMvPolynomial S₂ S₃ →+* MvPolynomial S₁ R) (hfgC : (f.comp g).comp C = C)
    (hfgX : ∀ n, f (g (X n)) = X n) (hgfC : (g.comp f).comp C = C) (hgfX : ∀ n, g (f (X n)) = X n) :
    MvPolynomialMvPolynomial S₁ R ≃+* MvPolynomial S₂ S₃ where
  toFun := f
  invFun := g
  left_inv := is_id (RingHom.comp _ _) hgfC hgfX
  right_inv := is_id (RingHom.comp _ _) hfgC hfgX
  map_mul' := f.map_mul
  map_add' := f.map_add

Ring equivalence between multivariate polynomial rings

Informal description

Given commutative semirings $R$, $S_1$, $S_2$, and $S_3$, and ring homomorphisms $f: R[S_1] \to S_3[S_2]$ and $g: S_3[S_2] \to R[S_1]$ satisfying: 1. $f \circ g$ acts as identity on constant polynomials via $C$, 2. $f(g(X_n)) = X_n$ for all $n \in S_2$, 3. $g \circ f$ acts as identity on constant polynomials via $C$, 4. $g(f(X_n)) = X_n$ for all $n \in S_1$, then $f$ and $g$ form a ring equivalence between the multivariate polynomial rings $R[S_1]$ and $S_3[S_2]$.

MvPolynomial.sumRingEquiv definition

: MvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R)

Full source

/-- 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.
-/
def sumRingEquiv : MvPolynomialMvPolynomial (S₁ ⊕ S₂) R ≃+* MvPolynomial S₁ (MvPolynomial S₂ R) := by
  apply mvPolynomialEquivMvPolynomial R (S₁ ⊕ S₂) _ _ (sumToIter R S₁ S₂) (iterToSum R S₁ S₂)
  · refine RingHom.ext (hom_eq_hom _ _ ?hC ?hX)
    case hC => ext1; simp only [RingHom.comp_apply, iterToSum_C_C, sumToIter_C]
    case hX => intro; simp only [RingHom.comp_apply, iterToSum_C_X, sumToIter_Xr]
  · simp [iterToSum_X, sumToIter_Xl]
  · ext1; simp only [RingHom.comp_apply, sumToIter_C, iterToSum_C_C]
  · rintro ⟨⟩ <;> simp only [sumToIter_Xl, iterToSum_X, sumToIter_Xr, iterToSum_C_X]

Ring isomorphism between multivariate polynomial rings over a sum type and iterated polynomial rings

Informal description

The ring isomorphism between the multivariate polynomial ring over the sum type $S_1 \oplus S_2$ with coefficients in $R$, and the multivariate polynomial ring over $S_1$ with coefficients in the multivariate polynomial ring over $S_2$ with coefficients in $R$. More precisely, this isomorphism maps: - A constant polynomial $a \in R$ to the constant polynomial $C(a)$ in $R[X_{S_1}][X_{S_2}]$. - A variable $X_{\text{inl}(b)}$ (where $b \in S_1$) to the variable $X_b$ in $R[X_{S_1}][X_{S_2}]$. - A variable $X_{\text{inr}(c)}$ (where $c \in S_2$) to the constant polynomial $X_c$ in $R[X_{S_2}]$, viewed as an element of $R[X_{S_1}][X_{S_2}]$ via the embedding $C \circ X$.

MvPolynomial.sumAlgEquiv definition

: MvPolynomial (S₁ ⊕ S₂) R ≃ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R)

Full source

/-- 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.
-/
@[simps!]
def sumAlgEquiv : MvPolynomialMvPolynomial (S₁ ⊕ S₂) R ≃ₐ[R] MvPolynomial S₁ (MvPolynomial S₂ R) :=
  { sumRingEquiv R S₁ S₂ with
    commutes' := by
      intro r
      have A : algebraMap R (MvPolynomial S₁ (MvPolynomial S₂ R)) r = (C (C r) :) := rfl
      have B : algebraMap R (MvPolynomial (S₁ ⊕ S₂) R) r = C r := rfl
      simp only [sumRingEquiv, mvPolynomialEquivMvPolynomial, Equiv.toFun_as_coe,
        Equiv.coe_fn_mk, B, sumToIter_C, A] }

Algebra isomorphism between multivariate polynomial rings over a sum type and iterated polynomial rings

Informal description

The algebra isomorphism between the multivariate polynomial ring over the sum type $S_1 \oplus S_2$ with coefficients in a commutative semiring $R$, and the multivariate polynomial ring over $S_1$ with coefficients in the multivariate polynomial ring over $S_2$ with coefficients in $R$. This isomorphism preserves the $R$-algebra structure and maps: - A constant polynomial $a \in R$ to the constant polynomial $C(C(a))$ in $R[X_{S_1}][X_{S_2}]$. - A variable $X_{\text{inl}(b)}$ (where $b \in S_1$) to the variable $X_b$ in $R[X_{S_1}][X_{S_2}]$. - A variable $X_{\text{inr}(c)}$ (where $c \in S_2$) to the constant polynomial $X_c$ in $R[X_{S_2}]$, viewed as an element of $R[X_{S_1}][X_{S_2}]$ via the embedding $C \circ X$.

MvPolynomial.sumAlgEquiv_comp_rename_inr theorem

 :
  (sumAlgEquiv R S₁ S₂).toAlgHom.comp (rename Sum.inr) =
    IsScalarTower.toAlgHom R (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R))

Full source

lemma sumAlgEquiv_comp_rename_inr :
    (sumAlgEquiv R S₁ S₂).toAlgHom.comp (rename Sum.inr) = IsScalarTower.toAlgHom R
        (MvPolynomial S₂ R) (MvPolynomial S₁ (MvPolynomial S₂ R)) := by
  ext i
  simp

Composition of sum algebra isomorphism with right renaming equals scalar tower homomorphism

Informal description

The composition of the algebra homomorphism induced by the algebra isomorphism `sumAlgEquiv` between multivariate polynomial rings over a sum type and iterated polynomial rings, with the renaming homomorphism `rename Sum.inr`, is equal to the algebra homomorphism `IsScalarTower.toAlgHom` from the multivariate polynomial ring over $S_2$ with coefficients in $R$ to the multivariate polynomial ring over $S_1$ with coefficients in the multivariate polynomial ring over $S_2$ with coefficients in $R$.

MvPolynomial.sumAlgEquiv_comp_rename_inl theorem

: (sumAlgEquiv R S₁ S₂).toAlgHom.comp (rename Sum.inl) = MvPolynomial.mapAlgHom (Algebra.ofId _ _)

Full source

lemma sumAlgEquiv_comp_rename_inl :
    (sumAlgEquiv R S₁ S₂).toAlgHom.comp (rename Sum.inl) =
      MvPolynomial.mapAlgHom (Algebra.ofId _ _) := by
  ext i
  simp

Composition of sum algebra equivalence with left renaming equals coefficient mapping via canonical algebra homomorphism

Informal description

Let $R$ be a commutative semiring, and let $S_1$ and $S_2$ be types. The composition of the algebra homomorphism induced by the sum algebra equivalence $\text{sumAlgEquiv}\, R\, S_1\, S_2$ with the renaming homomorphism $\text{rename}\, \text{Sum.inl}$ is equal to the algebra homomorphism $\text{mapAlgHom}$ applied to the canonical algebra homomorphism $\text{Algebra.ofId}\, S_1\, (\text{MvPolynomial}\, S_1\, R)$.

MvPolynomial.commAlgEquiv definition

: MvPolynomial S₁ (MvPolynomial S₂ R) ≃ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R)

Full source

/-- The algebra isomorphism between multivariable polynomials in variables `S₁` of multivariable
polynomials in variables `S₂` and multivariable polynomials in variables `S₂` of multivariable
polynomials in variables `S₁`. -/
noncomputable
def commAlgEquiv : MvPolynomialMvPolynomial S₁ (MvPolynomial S₂ R) ≃ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R) :=
  (sumAlgEquiv R S₁ S₂).symm.trans <| (renameEquiv _ (.sumComm S₁ S₂)).trans (sumAlgEquiv R S₂ S₁)

Commutativity isomorphism of iterated multivariate polynomial rings

Informal description

The algebra isomorphism between the multivariate polynomial ring over $S_1$ with coefficients in the multivariate polynomial ring over $S_2$ with coefficients in $R$, and the multivariate polynomial ring over $S_2$ with coefficients in the multivariate polynomial ring over $S_1$ with coefficients in $R$. This isomorphism preserves the $R$-algebra structure and is constructed by: 1. Taking the inverse of the sum algebra isomorphism between $MvPolynomial (S_1 \oplus S_2) R$ and $MvPolynomial S_1 (MvPolynomial S_2 R)$, 2. Composing with the renaming equivalence induced by the sum commutativity isomorphism $S_1 \oplus S_2 \simeq S_2 \oplus S_1$, 3. Finally composing with the sum algebra isomorphism between $MvPolynomial (S_2 \oplus S_1) R$ and $MvPolynomial S_2 (MvPolynomial S_1 R)$.

MvPolynomial.commAlgEquiv_C theorem

(p) : commAlgEquiv R S₁ S₂ (.C p) = .map C p

Full source

@[simp] lemma commAlgEquiv_C (p) : commAlgEquiv R S₁ S₂ (.C p) = .map C p := by
  suffices (commAlgEquiv R S₁ S₂).toAlgHom.comp
      (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) _) = mapAlgHom (Algebra.ofId _ _) by
    exact DFunLike.congr_fun this p
  ext x : 1
  simp [commAlgEquiv]

Image of Constant Polynomial under Commutativity Isomorphism: $\text{commAlgEquiv}(C(p)) = \text{map}\, C\, p$

Informal description

For any commutative semiring $R$ and types $S_1$ and $S_2$, the algebra isomorphism $\text{commAlgEquiv}$ between iterated multivariate polynomial rings satisfies the following property: for any polynomial $p \in \text{MvPolynomial}(S_2, R)$, the image of the constant polynomial $C(p)$ under $\text{commAlgEquiv}$ is equal to the polynomial obtained by applying the coefficient mapping homomorphism $\text{map}\, C$ to $p$.

MvPolynomial.commAlgEquiv_C_X theorem

(i) : commAlgEquiv R S₁ S₂ (.C (.X i)) = .X i

Full source

lemma commAlgEquiv_C_X (i) : commAlgEquiv R S₁ S₂ (.C (.X i)) = .X i := by simp

Image of Constant Monomial under Commutativity Isomorphism: $\text{commAlgEquiv}(C(X_i)) = X_i$

Informal description

For any commutative semiring $R$ and types $S_1$ and $S_2$, the algebra isomorphism $\text{commAlgEquiv}$ between iterated multivariate polynomial rings satisfies the following property: for any variable index $i \in S_2$, the image of the constant polynomial $C(X_i)$ under $\text{commAlgEquiv}$ is equal to the monomial $X_i$ in $\text{MvPolynomial}(S_2, \text{MvPolynomial}(S_1, R))$.

MvPolynomial.commAlgEquiv_X theorem

(i) : commAlgEquiv R S₁ S₂ (.X i) = .C (.X i)

Full source

@[simp] lemma commAlgEquiv_X (i) : commAlgEquiv R S₁ S₂ (.X i) = .C (.X i) := by simp [commAlgEquiv]

Image of monomial $X_i$ under commutativity isomorphism of iterated polynomial rings

Informal description

For any variable index $i \in S_1$, the algebra isomorphism $\text{commAlgEquiv}$ between iterated multivariate polynomial rings maps the monomial $X_i$ in $\text{MvPolynomial}(S_1, \text{MvPolynomial}(S_2, R))$ to the constant polynomial $C(X_i)$ in $\text{MvPolynomial}(S_2, \text{MvPolynomial}(S_1, R))$.

MvPolynomial.optionEquivLeft definition

: MvPolynomial (Option S₁) R ≃ₐ[R] Polynomial (MvPolynomial S₁ R)

Full source

/-- The algebra isomorphism between multivariable polynomials in `Option S₁` and
polynomials with coefficients in `MvPolynomial S₁ R`.
-/
@[simps! -isSimp]
def optionEquivLeft : MvPolynomialMvPolynomial (Option S₁) R ≃ₐ[R] Polynomial (MvPolynomial S₁ R) :=
  AlgEquiv.ofAlgHom (MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (X s))
    (Polynomial.aevalTower (MvPolynomial.rename some) (X none))
    (by ext : 2 <;> simp) (by ext i : 2; cases i <;> simp)

Isomorphism between multivariate polynomials in $\text{Option}\, S₁$ and univariate polynomials over $R[X_i : i \in S₁]$

Informal description

The algebra isomorphism between the multivariate polynomial ring $R[X_i : i \in \text{Option}\, S₁]$ and the univariate polynomial ring over the multivariate polynomial ring $R[X_i : i \in S₁]$. Specifically, it maps: - The variable $\text{none}$ to the polynomial variable $X$ in the univariate polynomial ring. - The variable $\text{some}\, x$ (for $x \in S₁$) to the constant polynomial $\text{C}(X_x)$, where $X_x$ is the monomial corresponding to $x$ in $R[X_i : i \in S₁]$.

MvPolynomial.optionEquivLeft_X_some theorem

(x : S₁) : optionEquivLeft R S₁ (X (some x)) = Polynomial.C (X x)

Full source

lemma optionEquivLeft_X_some (x : S₁) : optionEquivLeft R S₁ (X (some x)) = Polynomial.C (X x) := by
  simp [optionEquivLeft_apply, aeval_X]

Image of Some Variable under Option Equivalence: $\text{optionEquivLeft}(X_{\text{some}\,x}) = \text{C}(X_x)$

Informal description

For any variable $x \in S₁$, the algebra isomorphism $\text{optionEquivLeft}$ maps the monomial $X_{\text{some}\,x}$ in the multivariate polynomial ring $R[X_i : i \in \text{Option}\, S₁]$ to the constant polynomial $\text{C}(X_x)$ in the univariate polynomial ring over $R[X_i : i \in S₁]$. That is, \[ \text{optionEquivLeft}(X_{\text{some}\,x}) = \text{C}(X_x). \]

MvPolynomial.optionEquivLeft_X_none theorem

: optionEquivLeft R S₁ (X none) = Polynomial.X

Full source

lemma optionEquivLeft_X_none : optionEquivLeft R S₁ (X none) = Polynomial.X := by
  simp [optionEquivLeft_apply, aeval_X]

Image of None Variable under Option Equivalence: $\text{optionEquivLeft}(X_{\text{none}}) = X$

Informal description

Under the algebra isomorphism `optionEquivLeft` between the multivariate polynomial ring $R[X_i : i \in \text{Option}\, S₁]$ and the univariate polynomial ring over $R[X_i : i \in S₁]$, the variable $X_{\text{none}}$ is mapped to the polynomial variable $X$ in the univariate polynomial ring. That is, $\text{optionEquivLeft}(X_{\text{none}}) = X$.

MvPolynomial.optionEquivLeft_C theorem

(r : R) : optionEquivLeft R S₁ (C r) = Polynomial.C (C r)

Full source

lemma optionEquivLeft_C (r : R) : optionEquivLeft R S₁ (C r) = Polynomial.C (C r) := by
  simp only [optionEquivLeft_apply, aeval_C, Polynomial.algebraMap_apply, algebraMap_eq]

Isomorphism preserves constant polynomials: $\text{optionEquivLeft}(C(r)) = \text{Polynomial.C}(C(r))$

Informal description

For any commutative semiring $R$ and any type $S₁$, the algebra isomorphism $\text{optionEquivLeft}_{R,S₁}$ maps the constant polynomial $C(r) \in R[X_i : i \in \text{Option}\, S₁]$ to the constant polynomial $\text{Polynomial.C}(C(r))$ in the univariate polynomial ring over $R[X_i : i \in S₁]$. In other words, the following diagram commutes: \[ \text{optionEquivLeft}_{R,S₁}(C(r)) = \text{Polynomial.C}(C(r)) \]

MvPolynomial.optionEquivLeft_monomial theorem

(m : Option S₁ →₀ ℕ) (r : R) : optionEquivLeft R S₁ (monomial m r) = .monomial (m none) (monomial m.some r)

Full source

theorem optionEquivLeft_monomial (m : OptionOption S₁ →₀ ℕ) (r : R) :
    optionEquivLeft R S₁ (monomial m r) = .monomial (m none) (monomial m.some r) := by
  rw [optionEquivLeft_apply, aeval_monomial, prod_option_index]
  · rw [MvPolynomial.monomial_eq, ← Polynomial.C_mul_X_pow_eq_monomial]
    simp only [Polynomial.algebraMap_apply, algebraMap_eq, Option.elim_none, Option.elim_some,
      map_mul, mul_assoc]
    apply congr_arg₂ _ rfl
    simp only [mul_comm, map_finsuppProd, map_pow]
  · intros; simp
  · intros; rw [pow_add]

Monomial Image under Option Equivalence: $\text{optionEquivLeft}(r X^m) = X^{m(\text{none})} \cdot (r X^{m|_{\text{some}}})$

Informal description

Let $R$ be a commutative semiring and $S₁$ a type. For any finitely supported function $m \colon \text{Option}\, S₁ \to \mathbb{N}$ and any coefficient $r \in R$, the algebra isomorphism $\text{optionEquivLeft}_{R,S₁}$ maps the monomial $r X^m$ in $R[X_i : i \in \text{Option}\, S₁]$ to the monomial $X^{m(\text{none})} \cdot (r X^{m|_{\text{some}}})$ in $R[X_i : i \in S₁][X]$, where $m|_{\text{some}}$ is the restriction of $m$ to $S₁$. In symbols: \[ \text{optionEquivLeft}_{R,S₁}(r X^m) = X^{m(\text{none})} \cdot (r X^{m|_{\text{some}}}) \]

MvPolynomial.optionEquivLeft_coeff_coeff theorem

 (n : Option S₁ →₀ ℕ) (f : MvPolynomial (Option S₁) R) :
  coeff n.some (Polynomial.coeff (optionEquivLeft R S₁ f) (n none)) = coeff n f

Full source

/-- The coefficient of `n.some` in the `n none`-th coefficient of `optionEquivLeft R S₁ f`
equals the coefficient of `n` in `f` -/
theorem optionEquivLeft_coeff_coeff (n : OptionOption S₁ →₀ ℕ) (f : MvPolynomial (Option S₁) R) :
    coeff n.some (Polynomial.coeff (optionEquivLeft R S₁ f) (n none)) =
      coeff n f := by
  induction' f using MvPolynomial.induction_on' with j r p q hp hq generalizing n
  swap
  · simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
  · rw [optionEquivLeft_monomial]
    classical
    simp only [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial, apply_ite]
    simp only [coeff_zero]
    by_cases hj : j = n
    · simp [hj]
    · rw [if_neg hj]
      simp only [ite_eq_right_iff]
      intro hj_none hj_some
      apply False.elim (hj _)
      simp only [Finsupp.ext_iff, Option.forall, hj_none, true_and]
      simpa only [Finsupp.ext_iff] using hj_some

Coefficient Correspondence under Option Equivalence: $\text{coeff } n|_{\text{some}} (X^{n(\text{none})} \text{ coeff}) = \text{coeff } n$

Informal description

For any finitely supported function $n \colon \text{Option}\, S₁ \to \mathbb{N}$ and any multivariate polynomial $f \in R[X_i : i \in \text{Option}\, S₁]$, the coefficient of the monomial $n|_{\text{some}}$ in the coefficient of $X^{n(\text{none})}$ in the polynomial $\text{optionEquivLeft}_{R,S₁}(f)$ equals the coefficient of the monomial $n$ in $f$. In symbols: \[ \text{coeff } n|_{\text{some}} \left( \text{Polynomial.coeff } (\text{optionEquivLeft}_{R,S₁} f) (n(\text{none})) \right) = \text{coeff } n f \]

MvPolynomial.optionEquivLeft_elim_eval theorem

 (s : S₁ → R) (y : R) (f : MvPolynomial (Option S₁) R) :
  eval (fun x ↦ Option.elim x y s) f = Polynomial.eval y (Polynomial.map (eval s) (optionEquivLeft R S₁ f))

Full source

theorem optionEquivLeft_elim_eval (s : S₁ → R) (y : R) (f : MvPolynomial (Option S₁) R) :
    eval (fun x ↦ Option.elim x y s) f =
      Polynomial.eval y (Polynomial.map (eval s) (optionEquivLeft R S₁ f)) := by
  -- turn this into a def `Polynomial.mapAlgHom`
  let φ : (MvPolynomial S₁ R)[X](MvPolynomial S₁ R)[X] →ₐ[R] R[X] :=
    { Polynomial.mapRingHom (eval s) with
      commutes' := fun r => by
        convert Polynomial.map_C (eval s)
        exact (eval_C _).symm }
  show
    aeval (fun x ↦ Option.elim x y s) f =
      (Polynomial.aeval y).comp (φ.comp (optionEquivLeft _ _).toAlgHom) f
  congr 2
  apply MvPolynomial.algHom_ext
  rw [Option.forall]
  simp only [aeval_X, Option.elim_none, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp,
    Polynomial.coe_aeval_eq_eval, AlgHom.coe_mk, coe_mapRingHom, AlgHom.coe_coe, comp_apply,
    optionEquivLeft_apply, Polynomial.map_X, Polynomial.eval_X, Option.elim_some, Polynomial.map_C,
    eval_X, Polynomial.eval_C, implies_true, and_self, φ]

Evaluation of Multivariate Polynomials via Option Equivalence and Univariate Evaluation

Informal description

Let $R$ be a commutative semiring, $S₁$ a type, and $s : S₁ \to R$ a valuation of variables. For any $y \in R$ and any multivariate polynomial $f \in R[X_i : i \in \text{Option}\, S₁]$, the evaluation of $f$ at the extended valuation $\text{Option.elim}\, x\, y\, s$ (which maps $\text{none}$ to $y$ and $\text{some}\, x$ to $s(x)$) is equal to evaluating the univariate polynomial $\text{Polynomial.map}\, (\text{eval}\, s)\, (\text{optionEquivLeft}\, R\, S₁\, f)$ at $y$. In other words: \[ \text{eval}\, (\lambda x.\, \text{Option.elim}\, x\, y\, s)\, f = \text{Polynomial.eval}\, y\, (\text{Polynomial.map}\, (\text{eval}\, s)\, (\text{optionEquivLeft}\, R\, S₁\, f)) \]

MvPolynomial.natDegree_optionEquivLeft theorem

(p : MvPolynomial (Option S₁) R) : (optionEquivLeft R S₁ p).natDegree = p.degreeOf .none

Full source

@[simp]
lemma natDegree_optionEquivLeft (p : MvPolynomial (Option S₁) R) :
    (optionEquivLeft R S₁ p).natDegree = p.degreeOf .none := by
  apply le_antisymm
  · rw [Polynomial.natDegree_le_iff_coeff_eq_zero]
    intro N hN
    ext σ
    trans p.coeff (σ.embDomain .some + .single .none N)
    · simpa using optionEquivLeft_coeff_coeff R S₁ (σ.embDomain .some + .single .none N) p
    simp only [coeff_zero, ← not_mem_support_iff]
    intro H
    simpa using (degreeOf_lt_iff ((zero_le _).trans_lt hN)).mp hN _ H
  · rw [degreeOf_le_iff]
    intro σ hσ
    refine Polynomial.le_natDegree_of_ne_zero fun H ↦ ?_
    have := optionEquivLeft_coeff_coeff R S₁ σ p
    rw [H, coeff_zero, eq_comm, ← not_mem_support_iff] at this
    exact this hσ

Natural Degree Correspondence: $\text{natDegree}(\text{optionEquivLeft}(p)) = \text{degreeOf}(\text{none}, p)$

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \text{Option}\, S₁]$, the natural degree of the univariate polynomial $\text{optionEquivLeft}_{R,S₁}(p)$ is equal to the degree of $p$ with respect to the variable $\text{none}$. That is, \[ \text{natDegree}(\text{optionEquivLeft}_{R,S₁}(p)) = \text{degreeOf}(\text{none}, p). \]

MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le theorem

 (p : MvPolynomial (Option S₁) R) (i : ℕ) (hi : i ≤ p.totalDegree) :
  ((optionEquivLeft R S₁ p).coeff i).totalDegree + i ≤ p.totalDegree

Full source

lemma totalDegree_coeff_optionEquivLeft_add_le
    (p : MvPolynomial (Option S₁) R) (i : ℕ) (hi : i ≤ p.totalDegree) :
    ((optionEquivLeft R S₁ p).coeff i).totalDegree + i ≤ p.totalDegree := by
  classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simpa
  rw [totalDegree, add_comm, Finset.add_sup (by simpa only [support_nonempty]), Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_coeff R S₁] using hσ

Sum of Coefficient Degree and Index Bounded by Total Degree under Option Equivalence

Informal description

Let $R$ be a commutative semiring and $S₁$ a type. For any multivariate polynomial $p \in R[X_i : i \in \text{Option}\, S₁]$ and any natural number $i$ such that $i \leq \text{totalDegree}(p)$, the sum of the total degree of the $i$-th coefficient of $\text{optionEquivLeft}_{R,S₁}(p)$ and $i$ is less than or equal to the total degree of $p$. In symbols: \[ \text{totalDegree}(\text{coeff}_i(\text{optionEquivLeft}_{R,S₁}(p))) + i \leq \text{totalDegree}(p) \]

MvPolynomial.totalDegree_coeff_optionEquivLeft_le theorem

(p : MvPolynomial (Option S₁) R) (i : ℕ) : ((optionEquivLeft R S₁ p).coeff i).totalDegree ≤ p.totalDegree

Full source

lemma totalDegree_coeff_optionEquivLeft_le
    (p : MvPolynomial (Option S₁) R) (i : ℕ) :
    ((optionEquivLeft R S₁ p).coeff i).totalDegree ≤ p.totalDegree := by
  classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simp
  rw [totalDegree, Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain, add_comm i]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_coeff R S₁] using hσ

Total Degree Bound for Coefficients under Option Equivalence: $\text{totalDegree}(\text{coeff}_i(\text{optionEquivLeft}(p))) \leq \text{totalDegree}(p)$

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \text{Option}\, S₁]$ and any natural number $i$, the total degree of the $i$-th coefficient of the univariate polynomial $\text{optionEquivLeft}_{R,S₁}(p)$ is less than or equal to the total degree of $p$. In symbols: \[ \text{totalDegree}(\text{coeff}_i(\text{optionEquivLeft}_{R,S₁}(p))) \leq \text{totalDegree}(p) \]

MvPolynomial.optionEquivRight definition

: MvPolynomial (Option S₁) R ≃ₐ[R] MvPolynomial S₁ R[X]

Full source

/-- The algebra isomorphism between multivariable polynomials in `Option S₁` and
multivariable polynomials with coefficients in polynomials.
-/
@[simps!]
def optionEquivRight : MvPolynomialMvPolynomial (Option S₁) R ≃ₐ[R] MvPolynomial S₁ R[X] :=
  AlgEquiv.ofAlgHom (MvPolynomial.aeval fun o => o.elim (C Polynomial.X) X)
    (MvPolynomial.aevalTower (Polynomial.aeval (X none)) fun i => X (Option.some i))
    (by
      ext : 2 <;>
        simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp,
          IsScalarTower.coe_toAlgHom', comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X,
          Option.elim', aevalTower_X, AlgHom.coe_id, id, eq_self_iff_true, imp_true_iff])
    (by
      ext ⟨i⟩ : 2 <;>
        simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C,
          Polynomial.aeval_X, AlgHom.coe_id, id, aevalTower_X])

Isomorphism between multivariate polynomials in Option variables and polynomials in polynomial coefficients

Informal description

The algebra isomorphism between the multivariate polynomial ring $R[X_i : i \in \text{Option } S₁]$ and the multivariate polynomial ring $(R[X])[Y_j : j \in S₁]$, where $R[X]$ is the univariate polynomial ring over $R$. This isomorphism is defined by: - Mapping the variable $X_{\text{none}}$ to the polynomial variable $X$ in $R[X]$ - Mapping each variable $X_{\text{some } j}$ (for $j \in S₁$) to the corresponding variable $Y_j$ in $(R[X])[Y_j : j \in S₁]$

MvPolynomial.optionEquivRight_X_some theorem

(x : S₁) : optionEquivRight R S₁ (X (some x)) = X x

Full source

lemma optionEquivRight_X_some (x : S₁) : optionEquivRight R S₁ (X (some x)) = X x := by
  simp [optionEquivRight_apply, aeval_X]

Isomorphism Action on Some Variables: $\text{optionEquivRight}_{R,S₁}(X_{\text{some } x}) = X_x$

Informal description

For any variable $x \in S₁$, the algebra isomorphism $\text{optionEquivRight}_{R,S₁}$ maps the monomial $X_{\text{some } x}$ in the multivariate polynomial ring $R[X_i : i \in \text{Option } S₁]$ to the monomial $X_x$ in the multivariate polynomial ring $(R[X])[Y_j : j \in S₁]$.

MvPolynomial.optionEquivRight_X_none theorem

: optionEquivRight R S₁ (X none) = C Polynomial.X

Full source

lemma optionEquivRight_X_none : optionEquivRight R S₁ (X none) = C Polynomial.X := by
  simp [optionEquivRight_apply, aeval_X]

Isomorphism maps $X_{\text{none}}$ to $X$ in polynomial ring

Informal description

Under the algebra isomorphism $\text{optionEquivRight}_{R,S₁}$ between multivariate polynomial rings, the variable $X_{\text{none}}$ in $R[X_i : i \in \text{Option } S₁]$ is mapped to the polynomial variable $X$ in the univariate polynomial ring $R[X]$, i.e., \[ \text{optionEquivRight}_{R,S₁}(X_{\text{none}}) = C(X) \] where $C$ is the constant embedding from $R[X]$ to the multivariate polynomial ring $(R[X])[Y_j : j \in S₁]$.

MvPolynomial.optionEquivRight_C theorem

(r : R) : optionEquivRight R S₁ (C r) = C (Polynomial.C r)

Full source

lemma optionEquivRight_C (r : R) : optionEquivRight R S₁ (C r) = C (Polynomial.C r) := by
  simp only [optionEquivRight_apply, aeval_C, algebraMap_apply, Polynomial.algebraMap_eq]

Constant Polynomial Preservation under $\text{optionEquivRight}_{R,S₁}$: $\text{optionEquivRight}_{R,S₁}(C(r)) = C(\text{Polynomial.C}(r))$

Informal description

For any commutative semiring $R$ and any type $S₁$, the algebra isomorphism $\text{optionEquivRight}_{R,S₁}$ maps the constant polynomial $C(r) \in R[X_i : i \in \text{Option } S₁]$ to the constant polynomial $C(\text{Polynomial.C}(r)) \in (R[X])[Y_j : j \in S₁]$, where $\text{Polynomial.C}(r)$ is the constant polynomial in the univariate polynomial ring $R[X]$.

MvPolynomial.finSuccEquiv definition

: MvPolynomial (Fin (n + 1)) R ≃ₐ[R] Polynomial (MvPolynomial (Fin n) R)

Full source

/-- The algebra isomorphism between multivariable polynomials in `Fin (n + 1)` and
polynomials over multivariable polynomials in `Fin n`.
-/
def finSuccEquiv : MvPolynomialMvPolynomial (Fin (n + 1)) R ≃ₐ[R] Polynomial (MvPolynomial (Fin n) R) :=
  (renameEquiv R (_root_.finSuccEquiv n)).trans (optionEquivLeft R (Fin n))

Isomorphism between multivariate polynomials in $n+1$ variables and univariate polynomials over $n$-variable polynomials

Informal description

The algebra isomorphism between the multivariate polynomial ring $R[X_0, \ldots, X_n]$ in $n+1$ variables and the univariate polynomial ring over the multivariate polynomial ring $R[X_0, \ldots, X_{n-1}]$ in $n$ variables. This isomorphism maps: - The variable $X_0$ to the polynomial variable $X$ in the univariate polynomial ring. - The variable $X_{k+1}$ (for $k \in \text{Fin}\,n$) to the constant polynomial $\text{C}(X_k)$, where $X_k$ is the monomial corresponding to $k$ in $R[X_0, \ldots, X_{n-1}]$.

MvPolynomial.finSuccEquiv_eq theorem

 :
  (finSuccEquiv R n : MvPolynomial (Fin (n + 1)) R →+* Polynomial (MvPolynomial (Fin n) R)) =
    eval₂Hom (Polynomial.C.comp (C : R →+* MvPolynomial (Fin n) R)) fun i : Fin (n + 1) =>
      Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i

Full source

theorem finSuccEquiv_eq :
    (finSuccEquiv R n : MvPolynomialMvPolynomial (Fin (n + 1)) R →+* Polynomial (MvPolynomial (Fin n) R)) =
      eval₂Hom (Polynomial.C.comp (C : R →+* MvPolynomial (Fin n) R)) fun i : Fin (n + 1) =>
        Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i := by
  ext i : 2
  · simp only [finSuccEquiv, optionEquivLeft_apply, aeval_C, AlgEquiv.coe_trans, RingHom.coe_coe,
      coe_eval₂Hom, comp_apply, renameEquiv_apply, eval₂_C, RingHom.coe_comp, rename_C]
    rfl
  · refine Fin.cases ?_ ?_ i <;> simp [optionEquivLeft_apply, finSuccEquiv]

Equality of $\text{finSuccEquiv}_{R,n}$ with Evaluation Homomorphism for Multivariate Polynomials

Informal description

The algebra isomorphism $\text{finSuccEquiv}_{R,n}$ from the multivariate polynomial ring $R[X_0, \ldots, X_n]$ to the univariate polynomial ring over $R[X_0, \ldots, X_{n-1}]$ is equal to the evaluation homomorphism $\text{eval₂Hom}$ defined by: - Composing the constant embedding $\text{C} \colon R \to R[X_0, \ldots, X_{n-1}]$ with the univariate polynomial constant embedding $\text{Polynomial.C}$. - Mapping the variable $X_0$ to the polynomial variable $X$ and each variable $X_{k+1}$ (for $k \in \text{Fin}\,n$) to the constant polynomial $\text{Polynomial.C}(X_k)$, where $X_k$ is the monomial corresponding to $k$ in $R[X_0, \ldots, X_{n-1}]$.

MvPolynomial.finSuccEquiv_apply theorem

 (p : MvPolynomial (Fin (n + 1)) R) :
  finSuccEquiv R n p =
    eval₂Hom (Polynomial.C.comp (C : R →+* MvPolynomial (Fin n) R))
      (fun i : Fin (n + 1) => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i) p

Full source

theorem finSuccEquiv_apply (p : MvPolynomial (Fin (n + 1)) R) :
    finSuccEquiv R n p =
      eval₂Hom (Polynomial.C.comp (C : R →+* MvPolynomial (Fin n) R))
        (fun i : Fin (n + 1) => Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i) p := by
  rw [← finSuccEquiv_eq, RingHom.coe_coe]

Evaluation Formula for Multivariate-to-Univariate Polynomial Isomorphism

Informal description

For any commutative semiring $R$ and natural number $n$, the algebra isomorphism $\text{finSuccEquiv}_{R,n}$ from the multivariate polynomial ring $R[X_0, \ldots, X_n]$ to the univariate polynomial ring over $R[X_0, \ldots, X_{n-1}]$ satisfies the following property for any polynomial $p \in R[X_0, \ldots, X_n]$: \[ \text{finSuccEquiv}_{R,n}(p) = \text{eval₂Hom}(\text{Polynomial.C} \circ \text{C}, \varphi)(p) \] where: - $\text{C} \colon R \to R[X_0, \ldots, X_{n-1}]$ is the constant embedding - $\text{Polynomial.C}$ is the constant embedding for univariate polynomials - $\varphi \colon \text{Fin}(n+1) \to \text{Polynomial}(R[X_0, \ldots, X_{n-1}])$ maps: - $0$ to the polynomial variable $X$ - $k+1$ (for $k \in \text{Fin}\,n$) to the constant polynomial $\text{Polynomial.C}(X_k)$

MvPolynomial.finSuccEquiv_comp_C_eq_C theorem

 {R : Type u} [CommSemiring R] (n : ℕ) :
  (↑(MvPolynomial.finSuccEquiv R n).symm : Polynomial (MvPolynomial (Fin n) R) →+* _).comp
      (Polynomial.C.comp MvPolynomial.C) =
    (MvPolynomial.C : R →+* MvPolynomial (Fin n.succ) R)

Full source

theorem finSuccEquiv_comp_C_eq_C {R : Type u} [CommSemiring R] (n : ℕ) :
    (↑(MvPolynomial.finSuccEquiv R n).symm : PolynomialPolynomial (MvPolynomial (Fin n) R) →+* _).comp
        (Polynomial.C.comp MvPolynomial.C) =
      (MvPolynomial.C : R →+* MvPolynomial (Fin n.succ) R) := by
  refine RingHom.ext fun x => ?_
  rw [RingHom.comp_apply]
  refine
    (MvPolynomial.finSuccEquiv R n).injective
      (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) ?_)
  simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]

Commutativity of Constant Embedding with Multivariate-Univariate Polynomial Isomorphism

Informal description

For any commutative semiring $R$ and natural number $n$, the composition of the inverse of the algebra isomorphism $\text{finSuccEquiv}_{R,n}$ with the constant embedding $\text{Polynomial.C} \circ \text{C}$ equals the constant embedding $\text{C}$ into the multivariate polynomial ring $R[X_0, \ldots, X_n]$. In other words, the following diagram commutes: \[ \begin{tikzcd} R \arrow[r, "\text{C}"] \arrow[dr, "\text{C}"'] & \text{Polynomial}(R[X_0, \ldots, X_{n-1}]) \arrow[d, "\text{finSuccEquiv}_{R,n}^{-1}"] \\ & R[X_0, \ldots, X_n] \end{tikzcd} \] where: - $\text{C}$ denotes the constant embedding into the appropriate polynomial ring - $\text{Polynomial.C}$ is the constant embedding for univariate polynomials - $\text{finSuccEquiv}_{R,n}$ is the isomorphism between $R[X_0, \ldots, X_n]$ and $\text{Polynomial}(R[X_0, \ldots, X_{n-1}])$

MvPolynomial.finSuccEquiv_X_zero theorem

: finSuccEquiv R n (X 0) = Polynomial.X

Full source

theorem finSuccEquiv_X_zero : finSuccEquiv R n (X 0) = Polynomial.X := by simp [finSuccEquiv_apply]

Isomorphism maps $X_0$ to $X$ in multivariate-to-univariate polynomial equivalence

Informal description

For any commutative semiring $R$ and natural number $n$, the algebra isomorphism $\text{finSuccEquiv}_{R,n}$ maps the variable $X_0$ in the multivariate polynomial ring $R[X_0, \ldots, X_n]$ to the polynomial variable $X$ in the univariate polynomial ring over $R[X_0, \ldots, X_{n-1}]$. That is, \[ \text{finSuccEquiv}_{R,n}(X_0) = X. \]

MvPolynomial.finSuccEquiv_X_succ theorem

{j : Fin n} : finSuccEquiv R n (X j.succ) = Polynomial.C (X j)

Full source

theorem finSuccEquiv_X_succ {j : Fin n} : finSuccEquiv R n (X j.succ) = Polynomial.C (X j) := by
  simp [finSuccEquiv_apply]

Isomorphism Maps Successor Variable to Constant Polynomial: $\text{finSuccEquiv}_{R,n}(X_{j+1}) = \text{C}(X_j)$

Informal description

For any commutative semiring $R$ and natural number $n$, the algebra isomorphism $\text{finSuccEquiv}_{R,n}$ maps the monomial $X_{j+1}$ in the multivariate polynomial ring $R[X_0, \ldots, X_n]$ to the constant polynomial $\text{Polynomial.C}(X_j)$ in the univariate polynomial ring over $R[X_0, \ldots, X_{n-1}]$, for any $j \in \text{Fin}\,n$.

MvPolynomial.finSuccEquiv_coeff_coeff theorem

 (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) :
  coeff m (Polynomial.coeff (finSuccEquiv R n f) i) = coeff (m.cons i) f

Full source

/-- The coefficient of `m` in the `i`-th coefficient of `finSuccEquiv R n f` equals the
    coefficient of `Finsupp.cons i m` in `f`. -/
theorem finSuccEquiv_coeff_coeff (m : FinFin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) :
    coeff m (Polynomial.coeff (finSuccEquiv R n f) i) = coeff (m.cons i) f := by
  induction f using MvPolynomial.induction_on' generalizing i m with
  | add p q hp hq => simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
  | monomial j r =>
    simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
      Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
      Fin.cases_succ, ← map_prod, ← RingHom.map_pow, Function.comp_apply]
    rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]; congr 1
    obtain rfl | hjmi := eq_or_ne j (m.cons i)
    · simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul,
        Finsupp.prod_pow] using coeff_monomial m m (1 : R)
    · simp only [hjmi, if_false]
      obtain hij | rfl := ne_or_eq i (j 0)
      · simp only [hij, if_false, coeff_zero]
      simp only [eq_self_iff_true, if_true]
      have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction
      simpa only [monomial_eq, C_1, one_mul, Finsupp.prod_pow, tail_apply, if_neg hmj.symm] using
        coeff_monomial m j.tail (1 : R)

Coefficient Correspondence in Multivariate-to-Univariate Polynomial Isomorphism: $\text{coeff}_m(\text{coeff}_i(\varphi(f))) = \text{coeff}_{\mathrm{cons}(i, m)}(f)$

Informal description

For any finitely supported function $m \colon \mathrm{Fin}\,n \to \mathbb{N}$, any multivariate polynomial $f \in R[X_0, \ldots, X_n]$, and any natural number $i$, the coefficient of the monomial $m$ in the $i$-th coefficient of $\mathrm{finSuccEquiv}_{R,n}(f)$ (viewed as a univariate polynomial over $R[X_0, \ldots, X_{n-1}]$) is equal to the coefficient of the monomial $\mathrm{cons}(i, m)$ in $f$. In symbols: \[ \text{coeff}_m \big(\text{coeff}_i (\mathrm{finSuccEquiv}_{R,n}(f))\big) = \text{coeff}_{\mathrm{cons}(i, m)}(f). \]

MvPolynomial.eval_eq_eval_mv_eval' theorem

 (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (n + 1)) R) :
  eval (Fin.cons y s : Fin (n + 1) → R) f = Polynomial.eval y (Polynomial.map (eval s) (finSuccEquiv R n f))

Full source

theorem eval_eq_eval_mv_eval' (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (n + 1)) R) :
    eval (Fin.cons y s : Fin (n + 1) → R) f =
      Polynomial.eval y (Polynomial.map (eval s) (finSuccEquiv R n f)) := by
  -- turn this into a def `Polynomial.mapAlgHom`
  let φ : (MvPolynomial (Fin n) R)[X](MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
    { Polynomial.mapRingHom (eval s) with
      commutes' := fun r => by
        convert Polynomial.map_C (eval s)
        exact (eval_C _).symm }
  show
    aeval (Fin.cons y s : Fin (n + 1) → R) f =
      (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f
  congr 2
  apply MvPolynomial.algHom_ext
  rw [Fin.forall_iff_succ]
  simp only [φ, aeval_X, Fin.cons_zero, AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp,
    Polynomial.coe_aeval_eq_eval, Polynomial.map_C, AlgHom.coe_mk, RingHom.toFun_eq_coe,
    Polynomial.coe_mapRingHom, comp_apply, finSuccEquiv_apply, eval₂Hom_X',
    Fin.cases_zero, Polynomial.map_X, Polynomial.eval_X, Fin.cons_succ,
    Fin.cases_succ, eval_X, Polynomial.eval_C,
    RingHom.coe_mk, MonoidHom.coe_coe, AlgHom.coe_coe, implies_true, and_self,
    RingHom.toMonoidHom_eq_coe]

Evaluation of Multivariate Polynomial via Univariate Reduction

Informal description

For any valuation $s \colon \text{Fin}\,n \to R$ of the first $n$ variables, any element $y \in R$, and any multivariate polynomial $f \in R[X_0, \ldots, X_n]$, the evaluation of $f$ at the extended valuation $\text{Fin.cons}(y, s) \colon \text{Fin}(n+1) \to R$ is equal to the evaluation at $y$ of the univariate polynomial obtained by first applying the isomorphism $\text{finSuccEquiv}_{R,n}$ to $f$ and then mapping the coefficients via $\text{eval}(s)$. In symbols: \[ \text{eval}(\text{Fin.cons}(y, s), f) = \text{Polynomial.eval}\big(y, \text{Polynomial.map}(\text{eval}(s), \text{finSuccEquiv}_{R,n}(f))\big). \]

MvPolynomial.coeff_eval_eq_eval_coeff theorem

 (s' : S₁ → R) (f : Polynomial (MvPolynomial S₁ R)) (i : ℕ) :
  Polynomial.coeff (Polynomial.map (eval s') f) i = eval s' (Polynomial.coeff f i)

Full source

theorem coeff_eval_eq_eval_coeff (s' : S₁ → R) (f : Polynomial (MvPolynomial S₁ R))
    (i : ℕ) : Polynomial.coeff (Polynomial.map (eval s') f) i = eval s' (Polynomial.coeff f i) := by
  simp only [Polynomial.coeff_map]

Coefficient Evaluation Commutes with Polynomial Evaluation

Informal description

For any valuation $s' \colon S_1 \to R$ of the variables, any polynomial $f$ with coefficients in the multivariate polynomial ring $\text{MvPolynomial}(S_1, R)$, and any natural number $i$, the $i$-th coefficient of the polynomial obtained by evaluating $f$ at $s'$ is equal to the evaluation at $s'$ of the $i$-th coefficient of $f$. In symbols: \[ \text{coeff}_i \big(\text{map}(\text{eval}(s'), f)\big) = \text{eval}(s') (\text{coeff}_i f). \]

MvPolynomial.support_coeff_finSuccEquiv theorem

 {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : Fin n →₀ ℕ} :
  m ∈ ((finSuccEquiv R n f).coeff i).support ↔ m.cons i ∈ f.support

Full source

theorem support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : FinFin n →₀ ℕ} :
    m ∈ ((finSuccEquiv R n f).coeff i).supportm ∈ ((finSuccEquiv R n f).coeff i).support ↔ m.cons i ∈ f.support := by
  apply Iff.intro
  · intro h
    simpa [← finSuccEquiv_coeff_coeff] using h
  · intro h
    simpa [mem_support_iff, ← finSuccEquiv_coeff_coeff m f i] using h

Support Correspondence in Multivariate-to-Univariate Polynomial Isomorphism: $m \in \mathrm{support}(\mathrm{coeff}_i(\varphi(f))) \leftrightarrow \mathrm{cons}(i, m) \in \mathrm{support}(f)$

Informal description

For a multivariate polynomial $f \in R[X_0, \ldots, X_n]$, a natural number $i$, and a monomial $m \in R[X_1, \ldots, X_n]$, the monomial $m$ appears in the support of the $i$-th coefficient of $\mathrm{finSuccEquiv}_{R,n}(f)$ (viewed as a univariate polynomial over $R[X_1, \ldots, X_n]$) if and only if the monomial $\mathrm{cons}(i, m)$ appears in the support of $f$. In symbols: \[ m \in \mathrm{support}(\mathrm{coeff}_i(\mathrm{finSuccEquiv}_{R,n}(f))) \leftrightarrow \mathrm{cons}(i, m) \in \mathrm{support}(f). \]

MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le theorem

 (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) (hi : (finSuccEquiv R n f).coeff i ≠ 0) :
  totalDegree ((finSuccEquiv R n f).coeff i) + i ≤ totalDegree f

Full source

/--
The `totalDegree` of a multivariable polynomial `p` is at least `i` more than the `totalDegree` of
the `i`th coefficient of `finSuccEquiv` applied to `p`, if this is nonzero.
-/
lemma totalDegree_coeff_finSuccEquiv_add_le (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ)
    (hi : (finSuccEquiv R n f).coeff i ≠ 0) :
    totalDegree ((finSuccEquiv R n f).coeff i) + i ≤ totalDegree f := by
  have hf'_sup : ((finSuccEquiv R n f).coeff i).support.Nonempty := by
    rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
    exact hi
  -- Let σ be a monomial index of ((finSuccEquiv R n p).coeff i) of maximal total degree
  have ⟨σ, hσ1, hσ2⟩ := Finset.exists_mem_eq_sup (support _) hf'_sup
                          (fun s => Finsupp.sum s fun _ e => e)
  -- Then cons i σ is a monomial index of p with total degree equal to the desired bound
  let σ' : FinFin (n+1) →₀ ℕ := cons i σ
  convert le_totalDegree (s := σ') _
  · rw [totalDegree, hσ2, sum_cons, add_comm]
  · rw [← support_coeff_finSuccEquiv]
    exact hσ1

Total Degree Bound for Coefficients in Multivariate-to-Univariate Polynomial Isomorphism

Informal description

Let $f$ be a multivariate polynomial in $n+1$ variables over a commutative semiring $R$, and let $\varphi(f)$ be its image under the isomorphism $\mathrm{finSuccEquiv}_{R,n}$ to a univariate polynomial over $R[X_1, \ldots, X_n]$. For any $i \in \mathbb{N}$ such that the $i$-th coefficient of $\varphi(f)$ is nonzero, the sum of the total degree of this coefficient and $i$ is less than or equal to the total degree of $f$. In symbols: \[ \mathrm{totalDegree}(\mathrm{coeff}_i(\varphi(f))) + i \leq \mathrm{totalDegree}(f). \]

MvPolynomial.support_finSuccEquiv theorem

 (f : MvPolynomial (Fin (n + 1)) R) :
  (finSuccEquiv R n f).support = Finset.image (fun m : Fin (n + 1) →₀ ℕ => m 0) f.support

Full source

theorem support_finSuccEquiv (f : MvPolynomial (Fin (n + 1)) R) :
    (finSuccEquiv R n f).support = Finset.image (fun m : FinFin (n + 1) →₀ ℕ => m 0) f.support := by
  ext i
  rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff]
  constructor
  · rintro ⟨m, hm⟩
    refine ⟨cons i m, ?_, cons_zero _ _⟩
    rw [← support_coeff_finSuccEquiv]
    simpa using hm
  · rintro ⟨m, h, rfl⟩
    refine ⟨tail m, ?_⟩
    rwa [← coeff, zero_apply, ← mem_support_iff, support_coeff_finSuccEquiv, cons_tail]

Support Projection in Multivariate-to-Univariate Polynomial Isomorphism: $\mathrm{supp}(\varphi(f)) = \{m(0) \mid m \in \mathrm{supp}(f)\}$

Informal description

For any multivariate polynomial $f \in R[X_0, \ldots, X_n]$, the support of the univariate polynomial $\mathrm{finSuccEquiv}_{R,n}(f)$ (viewed as a polynomial over $R[X_1, \ldots, X_n]$) is equal to the image under the projection $m \mapsto m(0)$ of the support of $f$. In symbols: \[ \mathrm{supp}(\mathrm{finSuccEquiv}_{R,n}(f)) = \{m(0) \mid m \in \mathrm{supp}(f)\}. \]

MvPolynomial.mem_support_finSuccEquiv theorem

 {f : MvPolynomial (Fin (n + 1)) R} {x} :
  x ∈ (finSuccEquiv R n f).support ↔ x ∈ (fun m : Fin (n + 1) →₀ _ ↦ m 0) '' f.support

Full source

theorem mem_support_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {x} :
    x ∈ (finSuccEquiv R n f).supportx ∈ (finSuccEquiv R n f).support ↔ x ∈ (fun m : Fin (n + 1) →₀ _ ↦ m 0) '' f.support := by
  simpa using congr(x ∈ $(support_finSuccEquiv f))

Support Membership Characterization in Multivariate-to-Univariate Polynomial Isomorphism: $x \in \mathrm{supp}(\varphi(f)) \leftrightarrow \exists m \in \mathrm{supp}(f),\, x = m(0)$

Informal description

For a multivariate polynomial $f \in R[X_0, \ldots, X_n]$ and a natural number $x$, the following are equivalent: 1. $x$ belongs to the support of the univariate polynomial $\mathrm{finSuccEquiv}_{R,n}(f)$ (viewed as a polynomial over $R[X_1, \ldots, X_n]$). 2. There exists a monomial $m$ in the support of $f$ such that $x = m(0)$. In symbols: \[ x \in \mathrm{supp}(\mathrm{finSuccEquiv}_{R,n}(f)) \leftrightarrow \exists m \in \mathrm{supp}(f),\, x = m(0). \]

MvPolynomial.image_support_finSuccEquiv theorem

 {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} :
  ((finSuccEquiv R n f).coeff i).support.image (Finsupp.cons i) = {m ∈ f.support | m 0 = i}

Full source

theorem image_support_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} :
    ((finSuccEquiv R n f).coeff i).support.image (Finsupp.cons i) = {m ∈ f.support | m 0 = i} := by
  ext m
  rw [Finset.mem_filter, Finset.mem_image, mem_support_iff]
  conv_lhs =>
    congr
    ext
    rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]
  constructor
  · rintro ⟨m', ⟨h, hm'⟩⟩
    simp only [← hm']
    exact ⟨h, by rw [cons_zero]⟩
  · intro h
    use tail m
    rw [← h.2, cons_tail]
    simp [h.1]

Support Correspondence in Multivariate-to-Univariate Polynomial Isomorphism: $\mathrm{cons}(i, \mathrm{supp}(c_i)) = \{m \in \mathrm{supp}(f) \mid m(0) = i\}$

Informal description

For any multivariate polynomial $f \in R[X_0, \ldots, X_n]$ and any natural number $i$, the image of the support of the $i$-th coefficient of $\mathrm{finSuccEquiv}_{R,n}(f)$ (viewed as a univariate polynomial over $R[X_0, \ldots, X_{n-1}]$) under the map $\mathrm{cons}(i, \cdot)$ is equal to the subset of monomials in the support of $f$ whose exponent at $X_0$ is $i$. In symbols: \[ \{\mathrm{cons}(i, m) \mid m \in \mathrm{supp}(\mathrm{coeff}_i(\mathrm{finSuccEquiv}_{R,n}(f)))\} = \{m \in \mathrm{supp}(f) \mid m(0) = i\}. \]

MvPolynomial.mem_image_support_coeff_finSuccEquiv theorem

 {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
  x ∈ Finsupp.cons i '' ((finSuccEquiv R n f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i

Full source

lemma mem_image_support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
    x ∈ Finsupp.cons i '' ((finSuccEquiv R n f).coeff i).supportx ∈ Finsupp.cons i '' ((finSuccEquiv R n f).coeff i).support ↔
      x ∈ f.support ∧ x 0 = i := by
  simpa using congr(x ∈ $image_support_finSuccEquiv)

Characterization of Monomials in Support via FinSuccEquiv: $x \in \mathrm{cons}(i, \mathrm{supp}(c_i)) \leftrightarrow x \in \mathrm{supp}(f) \land x(0) = i$

Informal description

For any multivariate polynomial $f \in R[X_0, \ldots, X_n]$, any natural number $i$, and any monomial $x$, the following are equivalent: 1. $x$ is in the image of the support of the $i$-th coefficient of $\mathrm{finSuccEquiv}_{R,n}(f)$ under the map $\mathrm{cons}(i, \cdot)$. 2. $x$ is in the support of $f$ and the exponent of $X_0$ in $x$ is $i$. In symbols: \[ x \in \{\mathrm{cons}(i, m) \mid m \in \mathrm{supp}(\mathrm{coeff}_i(\mathrm{finSuccEquiv}_{R,n}(f)))\} \leftrightarrow x \in \mathrm{supp}(f) \land x(0) = i. \]

MvPolynomial.mem_support_coeff_finSuccEquiv theorem

 {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} : x ∈ ((finSuccEquiv R n f).coeff i).support ↔ x.cons i ∈ f.support

Full source

lemma mem_support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
    x ∈ ((finSuccEquiv R n f).coeff i).supportx ∈ ((finSuccEquiv R n f).coeff i).support ↔ x.cons i ∈ f.support := by
  rw [← (Finsupp.cons_right_injective i).mem_finset_image (a := x),
    image_support_finSuccEquiv]
  simp only [Finset.mem_filter, mem_support_iff, ne_eq, cons_zero, and_true]

Support Membership Correspondence in Multivariate-to-Univariate Polynomial Isomorphism

Informal description

For any multivariate polynomial $f \in R[X_0, \ldots, X_n]$ and any natural number $i$, a monomial $x$ belongs to the support of the $i$-th coefficient of $\mathrm{finSuccEquiv}_{R,n}(f)$ (viewed as a univariate polynomial over $R[X_0, \ldots, X_{n-1}]$) if and only if the monomial obtained by prepending $i$ to $x$ (i.e., $\mathrm{cons}(i, x)$) belongs to the support of $f$. In symbols: \[ x \in \mathrm{supp}(\mathrm{coeff}_i(\mathrm{finSuccEquiv}_{R,n}(f))) \leftrightarrow \mathrm{cons}(i, x) \in \mathrm{supp}(f). \]

MvPolynomial.support_finSuccEquiv_nonempty theorem

{f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) : (finSuccEquiv R n f).support.Nonempty

Full source

theorem support_finSuccEquiv_nonempty {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
    (finSuccEquiv R n f).support.Nonempty := by
  rwa [Polynomial.support_nonempty, EmbeddingLike.map_ne_zero_iff]

Nonempty Support of Polynomial under FinSuccEquiv for Nonzero Polynomials

Informal description

For any nonzero multivariate polynomial $f \in R[X_0, \ldots, X_n]$, the support of its image under the isomorphism `finSuccEquiv R n` (which maps $f$ to a univariate polynomial over $R[X_0, \ldots, X_{n-1}]$) is nonempty. In other words, if $f \neq 0$, then there exists at least one monomial in the univariate polynomial representation of $f$ with a nonzero coefficient.

MvPolynomial.degree_finSuccEquiv theorem

{f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) : (finSuccEquiv R n f).degree = degreeOf 0 f

Full source

theorem degree_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
    (finSuccEquiv R n f).degree = degreeOf 0 f := by
  -- TODO: these should be lemmas
  have h₀ : ∀ {α β : Type _} (f : α → β), (fun x => x) ∘ f = f := fun f => rfl
  have h₁ : ∀ {α β : Type _} (f : α → β), f ∘ (fun x => x) = f := fun f => rfl

  have h' : ((finSuccEquiv R n f).support.sup fun x => x) = degreeOf 0 f := by
    rw [degreeOf_eq_sup, support_finSuccEquiv, Finset.sup_image, h₀]
  rw [Polynomial.degree, ← h', Nat.cast_withBot,
    Finset.coe_sup_of_nonempty (support_finSuccEquiv_nonempty h), Finset.max_eq_sup_coe, h₁]

Degree Preservation in Multivariate-to-Univariate Polynomial Isomorphism: $\deg(\varphi(f)) = \deg_{X_0}(f)$

Informal description

For any nonzero multivariate polynomial $f \in R[X_0, \ldots, X_n]$, the degree of its image under the isomorphism $\mathrm{finSuccEquiv}_{R,n}$ (which maps $f$ to a univariate polynomial over $R[X_1, \ldots, X_n]$) is equal to the degree of the variable $X_0$ in $f$. That is, \[ \deg(\mathrm{finSuccEquiv}_{R,n}(f)) = \deg_{X_0}(f). \]

MvPolynomial.natDegree_finSuccEquiv theorem

(f : MvPolynomial (Fin (n + 1)) R) : (finSuccEquiv R n f).natDegree = degreeOf 0 f

Full source

theorem natDegree_finSuccEquiv (f : MvPolynomial (Fin (n + 1)) R) :
    (finSuccEquiv R n f).natDegree = degreeOf 0 f := by
  by_cases c : f = 0
  · rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
  · rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]

Natural Degree Preservation in Multivariate-to-Univariate Polynomial Isomorphism: $\mathrm{natDegree}(\varphi(f)) = \deg_{X_0}(f)$

Informal description

For any multivariate polynomial $f \in R[X_0, \ldots, X_n]$, the natural degree of its image under the isomorphism $\mathrm{finSuccEquiv}_{R,n}$ (which maps $f$ to a univariate polynomial over $R[X_1, \ldots, X_n]$) is equal to the degree of the variable $X_0$ in $f$. That is, \[ \mathrm{natDegree}(\mathrm{finSuccEquiv}_{R,n}(f)) = \deg_{X_0}(f). \]

MvPolynomial.degreeOf_coeff_finSuccEquiv theorem

 (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ℕ) :
  degreeOf j (Polynomial.coeff (finSuccEquiv R n p) i) ≤ degreeOf j.succ p

Full source

theorem degreeOf_coeff_finSuccEquiv (p : MvPolynomial (Fin (n + 1)) R) (j : Fin n) (i : ℕ) :
    degreeOf j (Polynomial.coeff (finSuccEquiv R n p) i) ≤ degreeOf j.succ p := by
  rw [degreeOf_eq_sup, degreeOf_eq_sup, Finset.sup_le_iff]
  intro m hm
  rw [← Finsupp.cons_succ j i m]
  exact Finset.le_sup
    (f := fun (g : FinFin (Nat.succ n) →₀ ℕ) => g (Fin.succ j))
    (support_coeff_finSuccEquiv.1 hm)

Degree Bound in Multivariate-to-Univariate Polynomial Isomorphism: $\deg_{X_j}(\text{coeff}_i(\varphi(p))) \leq \deg_{X_{j+1}}(p)$

Informal description

For any multivariate polynomial $p \in R[X_0, \ldots, X_n]$, any index $j \in \text{Fin}\,n$, and any natural number $i$, the degree of the variable $X_j$ in the $i$-th coefficient of the univariate polynomial $\text{finSuccEquiv}_{R,n}(p)$ is less than or equal to the degree of the variable $X_{j+1}$ in $p$. In symbols: \[ \deg_{X_j}(\text{coeff}_i(\text{finSuccEquiv}_{R,n}(p))) \leq \deg_{X_{j+1}}(p). \]

MvPolynomial.finSuccEquiv_rename_finSuccEquiv theorem

 (e : σ ≃ Fin n) (φ : MvPolynomial (Option σ) R) :
  ((finSuccEquiv R n) ((rename ((Equiv.optionCongr e).trans (_root_.finSuccEquiv n).symm)) φ)) =
    Polynomial.map (rename e).toRingHom (optionEquivLeft R σ φ)

Full source

/-- Consider a multivariate polynomial `φ` whose variables are indexed by `Option σ`,
and suppose that `σ ≃ Fin n`.
Then one may view `φ` as a polynomial over `MvPolynomial (Fin n) R`, by

1. renaming the variables via `Option σ ≃ Fin (n+1)`, and then singling out the `0`-th variable
    via `MvPolynomial.finSuccEquiv`;
2. first viewing it as polynomial over `MvPolynomial σ R` via `MvPolynomial.optionEquivLeft`,
    and then renaming the variables.

This lemma shows that both constructions are the same. -/
lemma finSuccEquiv_rename_finSuccEquiv (e : σ ≃ Fin n) (φ : MvPolynomial (Option σ) R) :
    ((finSuccEquiv R n) ((rename ((Equiv.optionCongr e).trans (_root_.finSuccEquiv n).symm)) φ)) =
      Polynomial.map (rename e).toRingHom (optionEquivLeft R σ φ) := by
  suffices (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ((Equiv.optionCongr e).trans
        (_root_.finSuccEquiv n).symm)).toRingHom =
      (Polynomial.mapRingHom (rename e).toRingHom).comp (optionEquivLeft R σ) by
    exact DFunLike.congr_fun this φ
  apply ringHom_ext
  · simp [Polynomial.algebraMap_apply, algebraMap_eq, finSuccEquiv_apply, optionEquivLeft_apply]
  · rintro (i|i) <;> simp [finSuccEquiv_apply, optionEquivLeft_apply]

Commutative Diagram for Multivariate Polynomial Isomorphisms via Fin Equivalence

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type, and $n$ a natural number. Given an equivalence $e : \sigma \simeq \text{Fin}\,n$ and a multivariate polynomial $\varphi \in R[X_i : i \in \text{Option}\,\sigma]$, the following diagram commutes: 1. First apply the equivalence $\text{Option}\,\sigma \simeq \text{Fin}(n+1)$ obtained by composing $\text{Equiv.optionCongr}\,e$ with $\text{finSuccEquiv}\,n^{-1}$, then apply the isomorphism $\text{finSuccEquiv}\,R\,n$ to get a univariate polynomial over $R[X_i : i \in \text{Fin}\,n]$. 2. Alternatively, first apply the isomorphism $\text{optionEquivLeft}\,R\,\sigma$ to get a univariate polynomial over $R[X_i : i \in \sigma]$, then apply the ring homomorphism induced by renaming variables via $e$. The equality states that both paths yield the same result: \[ \text{finSuccEquiv}_{R,n} \circ \text{rename}\,(\text{optionCongr}\,e \circ \text{finSuccEquiv}\,n^{-1}) (\varphi) = \text{Polynomial.map}\,(\text{rename}\,e) \circ \text{optionEquivLeft}_{R,\sigma} (\varphi) \]

MvPolynomial.rename_polynomial_aeval_X theorem

 {σ τ : Type*} (f : σ → τ) (i : σ) (p : R[X]) :
  rename f (Polynomial.aeval (X i) p) = Polynomial.aeval (X (f i) : MvPolynomial τ R) p

Full source

@[simp]
theorem rename_polynomial_aeval_X {σ τ : Type*} (f : σ → τ) (i : σ) (p : R[X]) :
    rename f (Polynomial.aeval (X i) p) = Polynomial.aeval (X (f i) : MvPolynomial τ R) p := by
  rw [← aeval_algHom_apply, rename_X]

Compatibility of Renaming with Polynomial Evaluation in Multivariate Polynomial Rings

Informal description

Let $\sigma$ and $\tau$ be types, $R$ be a commutative semiring, $f : \sigma \to \tau$ be a function, $i \in \sigma$, and $p \in R[X]$. Then the renaming of the polynomial evaluation of $p$ at $X_i$ under $f$ is equal to the polynomial evaluation of $p$ at $X_{f(i)}$ in the multivariate polynomial ring $MvPolynomial\,\tau\,R$. In symbols: $$\text{rename}\,f\,(\text{Polynomial.aeval}\,(X_i)\,p) = \text{Polynomial.aeval}\,(X_{f(i)} : MvPolynomial\,\tau\,R)\,p$$

Polynomial.toMvPolynomial definition

(i : σ) : R[X] →ₐ[R] MvPolynomial σ R

Full source

/-- The embedding of `R[X]` into `R[Xᵢ]` as an `R`-algebra homomorphism. -/
noncomputable def Polynomial.toMvPolynomial (i : σ) : R[X]R[X] →ₐ[R] MvPolynomial σ R :=
  aeval (MvPolynomial.X i)

Embedding of univariate polynomials into multivariate polynomials via variable $X_i$

Informal description

For a given variable index $i \in \sigma$, the function maps a univariate polynomial $p \in R[X]$ to its image in the multivariate polynomial ring $R[X_j : j \in \sigma]$ by treating $X$ in $R[X]$ as the variable $X_i$ in $R[X_j : j \in \sigma]$. This is an $R$-algebra homomorphism.

Polynomial.toMvPolynomial_C theorem

(i : σ) (r : R) : (C r).toMvPolynomial i = MvPolynomial.C r

Full source

@[simp]
lemma Polynomial.toMvPolynomial_C (i : σ) (r : R) : (C r).toMvPolynomial i = MvPolynomial.C r := by
  simp [toMvPolynomial]

Constant Polynomial Embedding Preserves Constants in Multivariate Polynomial Ring

Informal description

For any commutative semiring $R$, any type $\sigma$, any variable index $i \in \sigma$, and any coefficient $r \in R$, the embedding of the constant polynomial $C(r)$ into the multivariate polynomial ring $R[X_j : j \in \sigma]$ via the variable $X_i$ equals the constant polynomial $C(r)$ in the multivariate polynomial ring. In symbols: $$(C(r)).\text{toMvPolynomial}\,i = C(r)$$

Polynomial.toMvPolynomial_X theorem

(i : σ) : X.toMvPolynomial i = MvPolynomial.X (R := R) i

Full source

@[simp]
lemma Polynomial.toMvPolynomial_X (i : σ) : X.toMvPolynomial i = MvPolynomial.X (R := R) i := by
  simp [toMvPolynomial]

Image of $X$ under univariate-to-multivariate embedding is $X_i$

Informal description

For any commutative semiring $R$ and any index $i \in \sigma$, the image of the polynomial variable $X$ under the embedding from univariate polynomials $R[X]$ to multivariate polynomials $R[X_j : j \in \sigma]$ is equal to the monomial $X_i$ in the multivariate polynomial ring. That is, \[ X.\text{toMvPolynomial}(i) = X_i. \]

Polynomial.toMvPolynomial_eq_rename_comp theorem

 (i : σ) : toMvPolynomial (R := R) i = (MvPolynomial.rename (fun _ : Unit ↦ i)).comp (MvPolynomial.pUnitAlgEquiv R).symm

Full source

lemma Polynomial.toMvPolynomial_eq_rename_comp (i : σ) :
    toMvPolynomial (R := R) i =
      (MvPolynomial.rename (fun _ : Unit ↦ i)).comp (MvPolynomial.pUnitAlgEquiv R).symm := by
  ext
  simp

Decomposition of univariate-to-multivariate embedding via renaming and unit isomorphism

Informal description

For any commutative semiring $R$ and any variable index $i \in \sigma$, the embedding $\text{toMvPolynomial}(i) \colon R[X] \to R[X_j : j \in \sigma]$ is equal to the composition of the isomorphism $(MvPolynomial.pUnitAlgEquiv R).symm \colon R[X] \to MvPolynomial(\text{PUnit}, R)$ with the renaming map $MvPolynomial.rename (fun \_ \mapsto i) \colon MvPolynomial(\text{PUnit}, R) \to R[X_j : j \in \sigma]$. In symbols: \[ \text{toMvPolynomial}(i) = \text{rename}(\lambda \_. i) \circ (\text{pUnitAlgEquiv } R)^{-1} \]

Polynomial.toMvPolynomial_injective theorem

(i : σ) : Function.Injective (toMvPolynomial (R := R) i)

Full source

lemma Polynomial.toMvPolynomial_injective (i : σ) :
    Function.Injective (toMvPolynomial (R := R) i) := by
  simp only [toMvPolynomial_eq_rename_comp, AlgHom.coe_comp, AlgHom.coe_coe,
    EquivLike.injective_comp]
  exact MvPolynomial.rename_injective (fun x ↦ i) fun _ _ _ ↦ rfl

Injectivity of the Univariate-to-Multivariate Polynomial Embedding via Variable $X_i$

Informal description

For any commutative semiring $R$ and any variable index $i \in \sigma$, the embedding $\text{toMvPolynomial}(i) \colon R[X] \to R[X_j : j \in \sigma]$ is injective. That is, if two univariate polynomials $p, q \in R[X]$ satisfy $p.\text{toMvPolynomial}(i) = q.\text{toMvPolynomial}(i)$, then $p = q$.

MvPolynomial.eval_comp_toMvPolynomial theorem

(f : σ → R) (i : σ) : (eval f).comp (toMvPolynomial (R := R) i) = Polynomial.evalRingHom (f i)

Full source

@[simp]
lemma MvPolynomial.eval_comp_toMvPolynomial (f : σ → R) (i : σ) :
    (eval f).comp (toMvPolynomial (R := R) i) = Polynomial.evalRingHom (f i) := by
  ext <;> simp

Compatibility of Evaluation with Univariate-to-Multivariate Embedding: $\text{eval}(f) \circ \text{toMvPolynomial}(i) = \text{evalRingHom}(f(i))$

Informal description

For any commutative semiring $R$, any valuation $f \colon \sigma \to R$, and any variable index $i \in \sigma$, the composition of the evaluation homomorphism $\text{eval}(f) \colon R[X_j : j \in \sigma] \to R$ with the embedding $\text{toMvPolynomial}(i) \colon R[X] \to R[X_j : j \in \sigma]$ equals the univariate polynomial evaluation homomorphism $\text{Polynomial.evalRingHom}(f(i)) \colon R[X] \to R$. In symbols: \[ \text{eval}(f) \circ \text{toMvPolynomial}(i) = \text{evalRingHom}(f(i)) \]

MvPolynomial.eval_toMvPolynomial theorem

(f : σ → R) (i : σ) (p : R[X]) : eval f (p.toMvPolynomial i) = Polynomial.eval (f i) p

Full source

@[simp]
lemma MvPolynomial.eval_toMvPolynomial (f : σ → R) (i : σ) (p : R[X]) :
    eval f (p.toMvPolynomial i) = Polynomial.eval (f i) p :=
  DFunLike.congr_fun (eval_comp_toMvPolynomial ..) p

Evaluation of Univariate Polynomials Embedded in Multivariate Polynomials

Informal description

For any commutative semiring $R$, any valuation $f \colon \sigma \to R$, any variable index $i \in \sigma$, and any univariate polynomial $p \in R[X]$, the evaluation of the multivariate polynomial $p.\text{toMvPolynomial}(i)$ at $f$ equals the evaluation of $p$ at $f(i)$. That is, \[ \text{eval}(f)(p.\text{toMvPolynomial}(i)) = \text{Polynomial.eval}(f(i))(p). \]

MvPolynomial.aeval_comp_toMvPolynomial theorem

(f : σ → S) (i : σ) : (aeval (R := R) f).comp (toMvPolynomial i) = Polynomial.aeval (f i)

Full source

@[simp]
lemma MvPolynomial.aeval_comp_toMvPolynomial (f : σ → S) (i : σ) :
    (aeval (R := R) f).comp (toMvPolynomial i) = Polynomial.aeval (f i) := by
  ext
  simp

Composition of Multivariate and Univariate Evaluation Homomorphisms via Variable Embedding

Informal description

Let $R$ be a commutative semiring, $S$ an $R$-algebra, and $\sigma$ a type. For any function $f : \sigma \to S$ and any index $i \in \sigma$, the composition of the algebra evaluation homomorphism $\text{aeval}(f) : \text{MvPolynomial}(\sigma, R) \to S$ with the embedding $\text{toMvPolynomial}(i) : R[X] \to \text{MvPolynomial}(\sigma, R)$ is equal to the univariate polynomial evaluation homomorphism $\text{aeval}(f(i)) : R[X] \to S$. That is, \[ \text{aeval}(f) \circ \text{toMvPolynomial}(i) = \text{aeval}(f(i)). \]

MvPolynomial.aeval_toMvPolynomial theorem

(f : σ → S) (i : σ) (p : R[X]) : aeval f (p.toMvPolynomial i) = Polynomial.aeval (f i) p

Full source

@[simp]
lemma MvPolynomial.aeval_toMvPolynomial (f : σ → S) (i : σ) (p : R[X]) :
    aeval f (p.toMvPolynomial i) = Polynomial.aeval (f i) p :=
  DFunLike.congr_fun (aeval_comp_toMvPolynomial ..) p

Evaluation of Univariate Polynomials Embedded in Multivariate Polynomials via $\text{aeval}$

Informal description

Let $R$ be a commutative semiring, $S$ an $R$-algebra, and $\sigma$ a type. For any function $f : \sigma \to S$, any index $i \in \sigma$, and any univariate polynomial $p \in R[X]$, the evaluation of the multivariate polynomial $\text{toMvPolynomial}_i(p)$ under the algebra homomorphism $\text{aeval}(f)$ is equal to the evaluation of $p$ at $f(i)$. That is, \[ \text{aeval}(f)(\text{toMvPolynomial}_i(p)) = \text{aeval}(f(i))(p). \]

MvPolynomial.rename_comp_toMvPolynomial theorem

(f : σ → τ) (a : σ) : (rename (R := R) f).comp (Polynomial.toMvPolynomial a) = Polynomial.toMvPolynomial (f a)

Full source

@[simp]
lemma MvPolynomial.rename_comp_toMvPolynomial (f : σ → τ) (a : σ) :
    (rename (R := R) f).comp (Polynomial.toMvPolynomial a) = Polynomial.toMvPolynomial (f a) := by
  ext
  simp

Compatibility of Renaming and Univariate-to-Multivariate Embedding

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types, and $f : \sigma \to \tau$ be a function. For any $a \in \sigma$, the composition of the renaming map $\text{rename}_f : R[X_i : i \in \sigma] \to R[X_j : j \in \tau]$ (induced by $f$) with the embedding $\text{toMvPolynomial}_a : R[X] \to R[X_i : i \in \sigma]$ (which maps $X$ to $X_a$) is equal to the embedding $\text{toMvPolynomial}_{f(a)} : R[X] \to R[X_j : j \in \tau]$ (which maps $X$ to $X_{f(a)}$). In other words, the following diagram commutes: \[ \begin{CD} R[X] @>{\text{toMvPolynomial}_a}>> R[X_i : i \in \sigma] \\ @. @VV{\text{rename}_f}V \\ R[X] @>{\text{toMvPolynomial}_{f(a)}}>> R[X_j : j \in \tau] \end{CD} \]

MvPolynomial.rename_toMvPolynomial theorem

(f : σ → τ) (a : σ) (p : R[X]) : (rename (R := R) f) (p.toMvPolynomial a) = p.toMvPolynomial (f a)

Full source

@[simp]
lemma MvPolynomial.rename_toMvPolynomial (f : σ → τ) (a : σ) (p : R[X]) :
    (rename (R := R) f) (p.toMvPolynomial a) = p.toMvPolynomial (f a) :=
  DFunLike.congr_fun (rename_comp_toMvPolynomial ..) p

Commutativity of Renaming and Univariate-to-Multivariate Embedding

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types, and $f : \sigma \to \tau$ be a function. For any $a \in \sigma$ and any univariate polynomial $p \in R[X]$, the renaming map $\text{rename}_f : R[X_i : i \in \sigma] \to R[X_j : j \in \tau]$ applied to the image of $p$ under the embedding $\text{toMvPolynomial}_a : R[X] \to R[X_i : i \in \sigma]$ is equal to the image of $p$ under the embedding $\text{toMvPolynomial}_{f(a)} : R[X] \to R[X_j : j \in \tau]$. In other words, the following diagram commutes: \[ \begin{CD} R[X] @>{\text{toMvPolynomial}_a}>> R[X_i : i \in \sigma] \\ @. @VV{\text{rename}_f}V \\ R[X] @>{\text{toMvPolynomial}_{f(a)}}>> R[X_j : j \in \tau] \end{CD} \]

Mathlib.Algebra.MvPolynomial.Equiv

Notation

Tags