Mathlib.Algebra.MvPolynomial.Rename

MvPolynomial.rename definition

(f : σ → τ) : MvPolynomial σ R →ₐ[R] MvPolynomial τ R

Full source

/-- Rename all the variables in a multivariable polynomial. -/
def rename (f : σ → τ) : MvPolynomialMvPolynomial σ R →ₐ[R] MvPolynomial τ R :=
  aeval (XX ∘ f)

Variable renaming in multivariate polynomials

Informal description

Given a function $f : \sigma \to \tau$, the function $\text{rename}(f)$ is the $R$-algebra homomorphism from the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$ to $\text{MvPolynomial}(\tau, R)$ that renames the variables according to $f$. Specifically, it maps each variable $X_i$ in $\text{MvPolynomial}(\sigma, R)$ to $X_{f(i)}$ in $\text{MvPolynomial}(\tau, R)$ and preserves the coefficients and algebraic structure.

MvPolynomial.rename_C theorem

(f : σ → τ) (r : R) : rename f (C r) = C r

Full source

theorem rename_C (f : σ → τ) (r : R) : rename f (C r) = C r :=
  eval₂_C _ _ _

Renaming Preserves Constant Polynomials: $\text{rename}(f)(C(r)) = C(r)$

Informal description

For any function $f \colon \sigma \to \tau$ between index types and any coefficient $r \in R$, the renaming operation $\text{rename}(f)$ applied to the constant polynomial $C(r)$ yields $C(r)$ again. That is, renaming variables preserves constant polynomials: \[ \text{rename}(f)(C(r)) = C(r). \]

MvPolynomial.rename_X theorem

(f : σ → τ) (i : σ) : rename f (X i : MvPolynomial σ R) = X (f i)

Full source

@[simp]
theorem rename_X (f : σ → τ) (i : σ) : rename f (X i : MvPolynomial σ R) = X (f i) :=
  eval₂_X _ _ _

Renaming of Variables in Multivariate Polynomials: $\text{rename}(f)(X_i) = X_{f(i)}$

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types indexing variables, and $f : \sigma \to \tau$ be a function. For any variable $X_i$ in the multivariate polynomial ring $R[X_j : j \in \sigma]$, the renaming operation satisfies $\text{rename}(f)(X_i) = X_{f(i)}$ in $R[X_k : k \in \tau]$.

MvPolynomial.map_rename theorem

(f : R →+* S) (g : σ → τ) (p : MvPolynomial σ R) : map f (rename g p) = rename g (map f p)

Full source

theorem map_rename (f : R →+* S) (g : σ → τ) (p : MvPolynomial σ R) :
    map f (rename g p) = rename g (map f p) := by
  apply MvPolynomial.induction_on p
    (fun a => by simp only [map_C, rename_C])
    (fun p q hp hq => by simp only [hp, hq, map_add]) fun p n hp => by
    simp only [hp, rename_X, map_X, map_mul]

Commutativity of Coefficient Mapping and Variable Renaming: $\text{map}\, f \circ \text{rename}\, g = \text{rename}\, g \circ \text{map}\, f$

Informal description

Let $R$ and $S$ be commutative semirings, $\sigma$ and $\tau$ be types indexing variables, $f \colon R \to S$ be a semiring homomorphism, and $g \colon \sigma \to \tau$ be a function. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the following diagram commutes: \[ \text{map}\, f \circ \text{rename}\, g\, (p) = \text{rename}\, g \circ \text{map}\, f\, (p). \] In other words, applying coefficient mapping $f$ after renaming variables via $g$ yields the same result as renaming variables via $g$ after applying coefficient mapping $f$.

MvPolynomial.map_comp_rename theorem

(f : R →+* S) (g : σ → τ) : (map f).comp (rename g).toRingHom = (rename g).toRingHom.comp (map f)

Full source

lemma map_comp_rename (f : R →+* S) (g : σ → τ) :
    (map f).comp (rename g).toRingHom = (rename g).toRingHom.comp (map f) :=
  RingHom.ext fun p ↦ map_rename f g p

Commutativity of Coefficient Mapping and Variable Renaming for Ring Homomorphisms: $\text{map}\, f \circ \text{rename}\, g = \text{rename}\, g \circ \text{map}\, f$

Informal description

Let $R$ and $S$ be commutative semirings, $\sigma$ and $\tau$ be types, $f \colon R \to S$ be a semiring homomorphism, and $g \colon \sigma \to \tau$ be a function. Then the composition of the coefficient mapping $\text{map}\, f$ with the variable renaming homomorphism $\text{rename}\, g$ (as ring homomorphisms) is equal to the composition of $\text{rename}\, g$ with $\text{map}\, f$. That is, \[ \text{map}\, f \circ \text{rename}\, g = \text{rename}\, g \circ \text{map}\, f. \]

MvPolynomial.rename_rename theorem

(f : σ → τ) (g : τ → α) (p : MvPolynomial σ R) : rename g (rename f p) = rename (g ∘ f) p

Full source

@[simp]
theorem rename_rename (f : σ → τ) (g : τ → α) (p : MvPolynomial σ R) :
    rename g (rename f p) = rename (g ∘ f) p :=
  show rename g (eval₂ C (XX ∘ f) p) = _ by
    simp only [rename, aeval_eq_eval₂Hom]
    -- Porting note: the Lean 3 proof of this was very fragile and included a nonterminal `simp`.
    -- Hopefully this is less prone to breaking
    rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (XX ∘ g)) C (XX ∘ f) p]
    simp only [comp_def, eval₂Hom_X']
    refine eval₂Hom_congr ?_ rfl rfl
    ext1; simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]

Composition of Variable Renamings in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, $\sigma$, $\tau$, and $\alpha$ be types, and $f : \sigma \to \tau$ and $g : \tau \to \alpha$ be functions. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the composition of renaming $p$ first by $f$ and then by $g$ is equal to renaming $p$ by the composition $g \circ f$. That is, \[ \text{rename}(g) \circ \text{rename}(f)(p) = \text{rename}(g \circ f)(p). \]

MvPolynomial.rename_comp_rename theorem

(f : σ → τ) (g : τ → α) : (rename (R := R) g).comp (rename f) = rename (g ∘ f)

Full source

lemma rename_comp_rename (f : σ → τ) (g : τ → α) :
    (rename (R := R) g).comp (rename f) = rename (g ∘ f) :=
  AlgHom.ext fun p ↦ rename_rename f g p

Composition of Renaming Homomorphisms Equals Renaming by Composition

Informal description

Let $R$ be a commutative semiring, and let $\sigma$, $\tau$, and $\alpha$ be types. For any functions $f : \sigma \to \tau$ and $g : \tau \to \alpha$, the composition of the renaming algebra homomorphisms $\text{rename}(g) \circ \text{rename}(f)$ is equal to the renaming homomorphism $\text{rename}(g \circ f)$. That is, \[ \text{rename}(g) \circ \text{rename}(f) = \text{rename}(g \circ f). \]

MvPolynomial.rename_id theorem

: rename id = AlgHom.id R (MvPolynomial σ R)

Full source

@[simp]
theorem rename_id : rename id = AlgHom.id R (MvPolynomial σ R) :=
  AlgHom.ext fun p ↦ eval₂_eta p

Identity Renaming is the Identity Homomorphism

Informal description

The renaming homomorphism corresponding to the identity function $\text{id} \colon \sigma \to \sigma$ is equal to the identity algebra homomorphism on the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$.

MvPolynomial.rename_id_apply theorem

(p : MvPolynomial σ R) : rename id p = p

Full source

lemma rename_id_apply (p : MvPolynomial σ R) : rename id p = p := by
  simp

Identity Renaming Preserves Polynomials

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, renaming the variables using the identity function leaves the polynomial unchanged, i.e., $\text{rename}(\text{id})(p) = p$.

MvPolynomial.rename_monomial theorem

(f : σ → τ) (d : σ →₀ ℕ) (r : R) : rename f (monomial d r) = monomial (d.mapDomain f) r

Full source

theorem rename_monomial (f : σ → τ) (d : σ →₀ ℕ) (r : R) :
    rename f (monomial d r) = monomial (d.mapDomain f) r := by
  rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d),
    Finsupp.prod_mapDomain_index]
  · rfl
  · exact fun n => pow_zero _
  · exact fun n i₁ i₂ => pow_add _ _ _

Renaming Monomials: $\text{rename}(f)(X^d \cdot r) = X^{d \circ f} \cdot r$

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types, and $f : \sigma \to \tau$ be a function. For any finitely supported function $d : \sigma \to \mathbb{N}$ and any coefficient $r \in R$, the renaming homomorphism applied to the monomial $X^d \cdot r$ yields the monomial $X^{d \circ f} \cdot r$ in the polynomial ring with variables indexed by $\tau$. In symbols: \[ \text{rename}(f)(X^d \cdot r) = X^{d \circ f} \cdot r \] where $d \circ f$ denotes the composition of $d$ with $f$, representing the exponents after renaming the variables.

MvPolynomial.rename_eq theorem

(f : σ → τ) (p : MvPolynomial σ R) : rename f p = Finsupp.mapDomain (Finsupp.mapDomain f) p

Full source

theorem rename_eq (f : σ → τ) (p : MvPolynomial σ R) :
    rename f p = Finsupp.mapDomain (Finsupp.mapDomain f) p := by
  simp only [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index]
  rfl

Variable Renaming as Double Domain Mapping in Multivariate Polynomials

Informal description

For any function $f : \sigma \to \tau$ and any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the polynomial obtained by renaming variables via $f$ is equal to applying the domain mapping operation twice to $p$ with respect to $f$. In symbols: $$\text{rename}(f)(p) = \text{mapDomain}(\text{mapDomain}(f))(p)$$ where $\text{mapDomain}(f)$ denotes the operation of mapping the domain of a finitely supported function via $f$.

MvPolynomial.rename_injective theorem

(f : σ → τ) (hf : Function.Injective f) : Function.Injective (rename f : MvPolynomial σ R → MvPolynomial τ R)

Full source

theorem rename_injective (f : σ → τ) (hf : Function.Injective f) :
    Function.Injective (rename f : MvPolynomial σ R → MvPolynomial τ R) := by
  have :
    (rename f : MvPolynomial σ R → MvPolynomial τ R) = Finsupp.mapDomain (Finsupp.mapDomain f) :=
    funext (rename_eq f)
  rw [this]
  exact Finsupp.mapDomain_injective (Finsupp.mapDomain_injective hf)

Injectivity of Variable Renaming in Multivariate Polynomials

Informal description

Let $f \colon \sigma \to \tau$ be an injective function between index types. Then the induced variable renaming map $\text{rename}(f) \colon R[X_i : i \in \sigma] \to R[X_j : j \in \tau]$ is also injective. Here, $R[X_i : i \in \sigma]$ denotes the multivariate polynomial ring over $R$ with variables indexed by $\sigma$.

MvPolynomial.rename_leftInverse theorem

 {f : σ → τ} {g : τ → σ} (hf : Function.LeftInverse f g) :
  Function.LeftInverse (rename f : MvPolynomial σ R → MvPolynomial τ R) (rename g)

Full source

theorem rename_leftInverse {f : σ → τ} {g : τ → σ} (hf : Function.LeftInverse f g) :
    Function.LeftInverse (rename f : MvPolynomial σ R → MvPolynomial τ R) (rename g) := by
  intro x
  simp [hf.comp_eq_id]

Left Inverse Property of Variable Renaming in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, and let $\sigma$ and $\tau$ be types. Given functions $f \colon \sigma \to \tau$ and $g \colon \tau \to \sigma$ such that $g$ is a left inverse of $f$ (i.e., $g(f(x)) = x$ for all $x \in \sigma$), then the renaming homomorphism $\text{rename}(g)$ is a left inverse of $\text{rename}(f)$. That is, for any multivariate polynomial $p \in R[X_i : i \in \sigma]$, we have \[ \text{rename}(g)(\text{rename}(f)(p)) = p. \]

MvPolynomial.rename_rightInverse theorem

 {f : σ → τ} {g : τ → σ} (hf : Function.RightInverse f g) :
  Function.RightInverse (rename f : MvPolynomial σ R → MvPolynomial τ R) (rename g)

Full source

theorem rename_rightInverse {f : σ → τ} {g : τ → σ} (hf : Function.RightInverse f g) :
    Function.RightInverse (rename f : MvPolynomial σ R → MvPolynomial τ R) (rename g) :=
 rename_leftInverse hf

Right Inverse Property of Variable Renaming in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, and let $\sigma$ and $\tau$ be types. Given functions $f \colon \sigma \to \tau$ and $g \colon \tau \to \sigma$ such that $f$ is a right inverse of $g$ (i.e., $f(g(y)) = y$ for all $y \in \tau$), then the renaming homomorphism $\text{rename}(f)$ is a right inverse of $\text{rename}(g)$. That is, for any multivariate polynomial $q \in R[X_j : j \in \tau]$, we have \[ \text{rename}(f)(\text{rename}(g)(q)) = q. \]

MvPolynomial.rename_surjective theorem

(f : σ → τ) (hf : Function.Surjective f) : Function.Surjective (rename f : MvPolynomial σ R → MvPolynomial τ R)

Full source

theorem rename_surjective (f : σ → τ) (hf : Function.Surjective f) :
    Function.Surjective (rename f : MvPolynomial σ R → MvPolynomial τ R) :=
  let ⟨_, hf⟩ := hf.hasRightInverse; rename_rightInverse hf |>.surjective

Surjectivity of Variable Renaming in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, and let $\sigma$ and $\tau$ be types. Given a surjective function $f \colon \sigma \to \tau$, the induced algebra homomorphism $\text{rename}(f) \colon R[X_i : i \in \sigma] \to R[X_j : j \in \tau]$ is also surjective. That is, for every polynomial $q \in R[X_j : j \in \tau]$, there exists a polynomial $p \in R[X_i : i \in \sigma]$ such that $\text{rename}(f)(p) = q$.

MvPolynomial.killCompl definition

: MvPolynomial τ R →ₐ[R] MvPolynomial σ R

Full source

/-- Given a function between sets of variables `f : σ → τ` that is injective with proof `hf`,
  `MvPolynomial.killCompl hf` is the `AlgHom` from `R[τ]` to `R[σ]` that is left inverse to
  `rename f : R[σ] → R[τ]` and sends the variables in the complement of the range of `f` to `0`. -/
def killCompl : MvPolynomialMvPolynomial τ R →ₐ[R] MvPolynomial σ R :=
  aeval fun i => if h : i ∈ Set.range f then X <| (Equiv.ofInjective f hf).symm ⟨i, h⟩ else 0

Algebra homomorphism killing variables outside the range of an injective map

Informal description

Given an injective function $ f : \sigma \to \tau $ with proof $ hf $ of injectivity, the algebra homomorphism $ \text{killCompl}\, hf : R[\tau] \to R[\sigma] $ is defined as follows: for each variable $ i \in \tau $, if $ i $ is in the range of $ f $, it maps $ X_i $ to $ X_{f^{-1}(i)} $, otherwise it maps $ X_i $ to $ 0 $. This homomorphism is left inverse to the renaming homomorphism $ \text{rename}\, f : R[\sigma] \to R[\tau] $.

MvPolynomial.killCompl_C theorem

(r : R) : killCompl hf (C r) = C r

Full source

theorem killCompl_C (r : R) : killCompl hf (C r) = C r := algHom_C _ _

Constant Polynomial Preservation under Variable Killing Homomorphism

Informal description

For any coefficient $r \in R$ in the commutative semiring $R$, the algebra homomorphism $\text{killCompl}\, hf$ maps the constant polynomial $C(r)$ in $R[\tau]$ to the constant polynomial $C(r)$ in $R[\sigma]$. That is, $\text{killCompl}\, hf(C(r)) = C(r)$.

MvPolynomial.killCompl_comp_rename theorem

: (killCompl hf).comp (rename f) = AlgHom.id R _

Full source

theorem killCompl_comp_rename : (killCompl hf).comp (rename f) = AlgHom.id R _ :=
  algHom_ext fun i => by
    dsimp
    rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos, Equiv.ofInjective_symm_apply]

Composition of killCompl and rename yields identity: $(\text{killCompl}\, hf) \circ (\text{rename}\, f) = \text{id}$

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types, and $f : \sigma \to \tau$ be an injective function. The composition of the algebra homomorphism $\text{killCompl}\, hf : R[\tau] \to R[\sigma]$ (which kills variables outside the range of $f$) with the renaming homomorphism $\text{rename}\, f : R[\sigma] \to R[\tau]$ is equal to the identity algebra homomorphism on $R[\sigma]$.

MvPolynomial.killCompl_rename_app theorem

(p : MvPolynomial σ R) : killCompl hf (rename f p) = p

Full source

@[simp]
theorem killCompl_rename_app (p : MvPolynomial σ R) : killCompl hf (rename f p) = p :=
  AlgHom.congr_fun (killCompl_comp_rename hf) p

Identity property of variable renaming and killing: $\text{killCompl}\, hf \circ \text{rename}\, f = \text{id}$ on $R[\sigma]$

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types, and $f : \sigma \to \tau$ be an injective function. For any multivariate polynomial $p \in R[\sigma]$, the composition of the renaming homomorphism $\text{rename}\, f$ with the variable-killing homomorphism $\text{killCompl}\, hf$ yields the original polynomial, i.e., $\text{killCompl}\, hf (\text{rename}\, f (p)) = p$.

MvPolynomial.renameEquiv definition

(f : σ ≃ τ) : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R

Full source

/-- `MvPolynomial.rename e` is an equivalence when `e` is. -/
@[simps apply]
def renameEquiv (f : σ ≃ τ) : MvPolynomialMvPolynomial σ R ≃ₐ[R] MvPolynomial τ R :=
  { rename f with
    toFun := rename f
    invFun := rename f.symm
    left_inv := fun p => by rw [rename_rename, f.symm_comp_self, rename_id_apply]
    right_inv := fun p => by rw [rename_rename, f.self_comp_symm, rename_id_apply] }

Variable renaming equivalence for multivariate polynomials

Informal description

Given a bijection $f : \sigma \simeq \tau$ between index types $\sigma$ and $\tau$, the function $\text{renameEquiv}(f)$ is an $R$-algebra equivalence between the multivariate polynomial rings $\text{MvPolynomial}(\sigma, R)$ and $\text{MvPolynomial}(\tau, R)$. It renames variables according to $f$ and its inverse renames variables according to $f^{-1}$, preserving the algebraic structure.

MvPolynomial.renameEquiv_refl theorem

: renameEquiv R (Equiv.refl σ) = AlgEquiv.refl

Full source

@[simp]
theorem renameEquiv_refl : renameEquiv R (Equiv.refl σ) = AlgEquiv.refl :=
  AlgEquiv.ext (by simp)

Identity Renaming Equivalence is the Identity Algebra Equivalence

Informal description

The variable renaming equivalence for multivariate polynomials, when applied to the identity equivalence $\text{id} \colon \sigma \to \sigma$, is equal to the identity algebra equivalence on the multivariate polynomial ring $\text{MvPolynomial}(\sigma, R)$.

MvPolynomial.renameEquiv_symm theorem

(f : σ ≃ τ) : (renameEquiv R f).symm = renameEquiv R f.symm

Full source

@[simp]
theorem renameEquiv_symm (f : σ ≃ τ) : (renameEquiv R f).symm = renameEquiv R f.symm :=
  rfl

Inverse of Variable Renaming Equivalence for Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, and let $\sigma$ and $\tau$ be types indexing the variables of multivariate polynomials. For any bijection $f : \sigma \simeq \tau$, the inverse of the variable renaming equivalence $\text{renameEquiv}(f) : \text{MvPolynomial}(\sigma, R) \simeq \text{MvPolynomial}(\tau, R)$ is equal to the variable renaming equivalence $\text{renameEquiv}(f^{-1}) : \text{MvPolynomial}(\tau, R) \simeq \text{MvPolynomial}(\sigma, R)$.

MvPolynomial.renameEquiv_trans theorem

(e : σ ≃ τ) (f : τ ≃ α) : (renameEquiv R e).trans (renameEquiv R f) = renameEquiv R (e.trans f)

Full source

@[simp]
theorem renameEquiv_trans (e : σ ≃ τ) (f : τ ≃ α) :
    (renameEquiv R e).trans (renameEquiv R f) = renameEquiv R (e.trans f) :=
  AlgEquiv.ext (rename_rename e f)

Composition of Renaming Equivalences for Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, and let $\sigma \simeq \tau$ and $\tau \simeq \alpha$ be type equivalences. The composition of the renaming equivalences $\text{renameEquiv}(e) : \text{MvPolynomial}(\sigma, R) \simeq \text{MvPolynomial}(\tau, R)$ and $\text{renameEquiv}(f) : \text{MvPolynomial}(\tau, R) \simeq \text{MvPolynomial}(\alpha, R)$ is equal to the renaming equivalence $\text{renameEquiv}(e \circ f) : \text{MvPolynomial}(\sigma, R) \simeq \text{MvPolynomial}(\alpha, R)$. In other words, the following diagram commutes: \[ \text{MvPolynomial}(\sigma, R) \xrightarrow{\text{renameEquiv}(e)} \text{MvPolynomial}(\tau, R) \xrightarrow{\text{renameEquiv}(f)} \text{MvPolynomial}(\alpha, R) \] is equal to: \[ \text{MvPolynomial}(\sigma, R) \xrightarrow{\text{renameEquiv}(e \circ f)} \text{MvPolynomial}(\alpha, R) \]

MvPolynomial.eval₂_rename theorem

: (rename k p).eval₂ f g = p.eval₂ f (g ∘ k)

Full source

theorem eval₂_rename : (rename k p).eval₂ f g = p.eval₂ f (g ∘ k) := by
  apply MvPolynomial.induction_on p <;>
    · intros
      simp [*]

Evaluation of Renamed Multivariate Polynomial: $\text{eval}_2(f, g, \text{rename}(k)(p)) = \text{eval}_2(f, g \circ k, p)$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ and $\tau$ be types indexing variables, $f : R \to S_1$ be a semiring homomorphism, $g : \tau \to S_1$ be a valuation, and $k : \sigma \to \tau$ be a function. For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the evaluation of the renamed polynomial $\text{rename}(k)(p)$ satisfies: \[ \text{eval}_2(f, g, \text{rename}(k)(p)) = \text{eval}_2(f, g \circ k, p) \]

MvPolynomial.eval_rename theorem

(g : τ → R) (p : MvPolynomial σ R) : eval g (rename k p) = eval (g ∘ k) p

Full source

theorem eval_rename (g : τ → R) (p : MvPolynomial σ R) : eval g (rename k p) = eval (g ∘ k) p :=
  eval₂_rename _ _ _ _

Evaluation of Renamed Multivariate Polynomial: $\text{eval}(g, \text{rename}(k)(p)) = \text{eval}(g \circ k, p)$

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types indexing variables, $g : \tau \to R$ be a valuation, and $k : \sigma \to \tau$ be a function. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the evaluation of the renamed polynomial $\text{rename}(k)(p)$ satisfies: \[ \text{eval}(g, \text{rename}(k)(p)) = \text{eval}(g \circ k, p) \]

MvPolynomial.eval₂Hom_rename theorem

: eval₂Hom f g (rename k p) = eval₂Hom f (g ∘ k) p

Full source

theorem eval₂Hom_rename : eval₂Hom f g (rename k p) = eval₂Hom f (g ∘ k) p :=
  eval₂_rename _ _ _ _

Evaluation Homomorphism of Renamed Multivariate Polynomial: $\text{eval₂Hom}(f, g) \circ \text{rename}(k) = \text{eval₂Hom}(f, g \circ k)$

Informal description

Let $R$ and $S_1$ be commutative semirings, $\sigma$ and $\tau$ be types indexing variables, $f : R \to S_1$ be a semiring homomorphism, $g : \tau \to S_1$ be a valuation, and $k : \sigma \to \tau$ be a function. For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the evaluation homomorphism of the renamed polynomial satisfies: \[ \text{eval₂Hom}(f, g)(\text{rename}(k)(p)) = \text{eval₂Hom}(f, g \circ k)(p) \]

MvPolynomial.aeval_rename theorem

[Algebra R S] : aeval g (rename k p) = aeval (g ∘ k) p

Full source

theorem aeval_rename [Algebra R S] : aeval g (rename k p) = aeval (g ∘ k) p :=
  eval₂Hom_rename _ _ _ _

Algebra Evaluation of Renamed Multivariate Polynomial: $\text{aeval}(g) \circ \text{rename}(k) = \text{aeval}(g \circ k)$

Informal description

Let $R$ be a commutative semiring, $S$ an $R$-algebra, $\sigma$ and $\tau$ types indexing variables, $g : \tau \to S$ a valuation, and $k : \sigma \to \tau$ a function. For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the algebra evaluation of the renamed polynomial satisfies: \[ \text{aeval}(g)(\text{rename}(k)(p)) = \text{aeval}(g \circ k)(p) \]

MvPolynomial.aeval_comp_rename theorem

[Algebra R S] : (aeval (R := R) g).comp (rename k) = MvPolynomial.aeval (g ∘ k)

Full source

lemma aeval_comp_rename [Algebra R S] :
    (aeval (R := R) g).comp (rename k) = MvPolynomial.aeval (g ∘ k) :=
  AlgHom.ext fun p ↦ aeval_rename k g p

Composition of Algebra Evaluation and Renaming: $\text{aeval}(g) \circ \text{rename}(k) = \text{aeval}(g \circ k)$

Informal description

Let $R$ be a commutative semiring, $S$ an $R$-algebra, $\sigma$ and $\tau$ types indexing variables, $g : \tau \to S$ a valuation, and $k : \sigma \to \tau$ a function. For any multivariate polynomial $p \in \text{MvPolynomial}(\sigma, R)$, the composition of the algebra evaluation homomorphism $\text{aeval}(g)$ with the renaming homomorphism $\text{rename}(k)$ is equal to the algebra evaluation homomorphism induced by the composition $g \circ k$: \[ \text{aeval}(g) \circ \text{rename}(k) = \text{aeval}(g \circ k). \]

MvPolynomial.rename_eval₂ theorem

(g : τ → MvPolynomial σ R) : rename k (p.eval₂ C (g ∘ k)) = (rename k p).eval₂ C (rename k ∘ g)

Full source

theorem rename_eval₂ (g : τ → MvPolynomial σ R) :
    rename k (p.eval₂ C (g ∘ k)) = (rename k p).eval₂ C (renamerename k ∘ g) := by
  apply MvPolynomial.induction_on p <;>
    · intros
      simp [*]

Commutativity of Renaming and Evaluation: $\text{rename}(k) \circ \text{eval}_2(C, g \circ k) = \text{eval}_2(C, \text{rename}(k) \circ g) \circ \text{rename}(k)$

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types indexing variables, $k : \sigma \to \tau$ be a function, and $p \in \text{MvPolynomial}(\sigma, R)$ be a multivariate polynomial. For any function $g : \tau \to \text{MvPolynomial}(\sigma, R)$, the following equality holds: \[ \text{rename}(k)\big(\text{eval}_2(C, g \circ k, p)\big) = \text{eval}_2\big(C, \text{rename}(k) \circ g, \text{rename}(k)(p)\big) \] where $C : R \to \text{MvPolynomial}(\sigma, R)$ is the constant polynomial embedding, and $\text{eval}_2$ is the evaluation of multivariate polynomials via a semiring homomorphism and valuation.

MvPolynomial.rename_prod_mk_eval₂ theorem

 (j : τ) (g : σ → MvPolynomial σ R) : rename (Prod.mk j) (p.eval₂ C g) = p.eval₂ C fun x => rename (Prod.mk j) (g x)

Full source

theorem rename_prod_mk_eval₂ (j : τ) (g : σ → MvPolynomial σ R) :
    rename (Prod.mk j) (p.eval₂ C g) = p.eval₂ C fun x => rename (Prod.mk j) (g x) := by
  apply MvPolynomial.induction_on p <;>
    · intros
      simp [*]

Compatibility of Renaming and Evaluation for Multivariate Polynomials: $\text{rename}(\text{Prod.mk}(j), \text{eval}_2(C, g, p)) = \text{eval}_2(C, \lambda x \mapsto \text{rename}(\text{Prod.mk}(j), g(x)), p)$

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types, and $p$ be a multivariate polynomial in $\text{MvPolynomial}(\sigma, R)$. For any $j \in \tau$ and any function $g \colon \sigma \to \text{MvPolynomial}(\sigma, R)$, the following equality holds: \[ \text{rename}(\text{Prod.mk}(j), \text{eval}_2(C, g, p)) = \text{eval}_2(C, \lambda x \mapsto \text{rename}(\text{Prod.mk}(j), g(x)), p) \] where $\text{Prod.mk}(j) \colon \sigma \to \sigma \times \tau$ is the function mapping each $x \in \sigma$ to $(x, j)$, $C \colon R \to \text{MvPolynomial}(\sigma, R)$ is the constant polynomial embedding, and $\text{eval}_2$ is the evaluation of multivariate polynomials via a semiring homomorphism and a valuation.

MvPolynomial.eval₂_rename_prod_mk theorem

 (g : σ × τ → S) (i : σ) (p : MvPolynomial τ R) : (rename (Prod.mk i) p).eval₂ f g = eval₂ f (fun j => g (i, j)) p

Full source

theorem eval₂_rename_prod_mk (g : σ × τ → S) (i : σ) (p : MvPolynomial τ R) :
    (rename (Prod.mk i) p).eval₂ f g = eval₂ f (fun j => g (i, j)) p := by
  apply MvPolynomial.induction_on p <;>
    · intros
      simp [*]

Evaluation of Renamed Multivariate Polynomial via Product Projection: $\text{eval}_2(f, g, \text{rename}(\text{Prod.mk } i)(p)) = \text{eval}_2(f, \lambda j. g(i,j), p)$

Informal description

Let $R$ and $S$ be commutative semirings, $\sigma$ and $\tau$ be types indexing variables, $f \colon R \to S$ be a semiring homomorphism, and $g \colon \sigma \times \tau \to S$ be a valuation. For any $i \in \sigma$ and any multivariate polynomial $p \in R[X_j : j \in \tau]$, the evaluation of the renamed polynomial $\text{rename}(\text{Prod.mk } i)(p)$ satisfies: \[ \text{eval}_2(f, g, \text{rename}(\text{Prod.mk } i)(p)) = \text{eval}_2(f, \lambda j. g(i,j), p) \] where $\text{Prod.mk } i \colon \tau \to \sigma \times \tau$ is the function $j \mapsto (i,j)$.

MvPolynomial.eval_rename_prod_mk theorem

(g : σ × τ → R) (i : σ) (p : MvPolynomial τ R) : eval g (rename (Prod.mk i) p) = eval (fun j => g (i, j)) p

Full source

theorem eval_rename_prod_mk (g : σ × τ → R) (i : σ) (p : MvPolynomial τ R) :
    eval g (rename (Prod.mk i) p) = eval (fun j => g (i, j)) p :=
  eval₂_rename_prod_mk (RingHom.id _) _ _ _

Evaluation of Renamed Polynomial via Product Projection: $\text{eval}(g, \text{rename}((i, \cdot))(p)) = \text{eval}(g(i, \cdot), p)$

Informal description

Let $R$ be a commutative semiring, $\sigma$ and $\tau$ be types indexing variables, and $g : \sigma \times \tau \to R$ be a valuation. For any $i \in \sigma$ and any multivariate polynomial $p \in R[X_j : j \in \tau]$, the evaluation of the renamed polynomial $\text{rename}(\text{Prod.mk } i)(p)$ at $g$ equals the evaluation of $p$ at the valuation $\lambda j. g(i,j)$. In other words: \[ \text{eval}(g, \text{rename}(\text{Prod.mk } i)(p)) = \text{eval}(\lambda j. g(i,j), p) \] where $\text{Prod.mk } i : \tau \to \sigma \times \tau$ is the function $j \mapsto (i,j)$.

MvPolynomial.exists_finset_rename theorem

(p : MvPolynomial σ R) : ∃ (s : Finset σ) (q : MvPolynomial { x // x ∈ s } R), p = rename (↑) q

Full source

/-- Every polynomial is a polynomial in finitely many variables. -/
theorem exists_finset_rename (p : MvPolynomial σ R) :
    ∃ (s : Finset σ) (q : MvPolynomial { x // x ∈ s } R), p = rename (↑) q := by
  classical
  apply induction_on p
  · intro r
    exact ⟨∅, C r, by rw [rename_C]⟩
  · rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
    refine ⟨s ∪ t, ⟨?_, ?_⟩⟩
    · refine rename (Subtype.map id ?_) p + rename (Subtype.map id ?_) q <;>
        simp +contextual only [id, true_or, or_true,
          Finset.mem_union, forall_true_iff]
    · simp only [rename_rename, map_add]
      rfl
  · rintro p n ⟨s, p, rfl⟩
    refine ⟨insert n s, ⟨?_, ?_⟩⟩
    · refine rename (Subtype.map id ?_) p * X ⟨n, s.mem_insert_self n⟩
      simp +contextual only [id, or_true, Finset.mem_insert, forall_true_iff]
    · simp only [rename_rename, rename_X, Subtype.coe_mk, map_mul]
      rfl

Finite Variable Representation of Multivariate Polynomials

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, there exists a finite subset $s \subseteq \sigma$ and a polynomial $q \in R[X_j : j \in s]$ such that $p$ can be obtained by renaming the variables of $q$ via the inclusion map $s \hookrightarrow \sigma$. In other words, $p$ is a polynomial in finitely many variables from $\sigma$.

MvPolynomial.exists_finset_rename₂ theorem

 (p₁ p₂ : MvPolynomial σ R) : ∃ (s : Finset σ) (q₁ q₂ : MvPolynomial s R), p₁ = rename (↑) q₁ ∧ p₂ = rename (↑) q₂

Full source

/-- `exists_finset_rename` for two polynomials at once: for any two polynomials `p₁`, `p₂` in a
  polynomial semiring `R[σ]` of possibly infinitely many variables, `exists_finset_rename₂` yields
  a finite subset `s` of `σ` such that both `p₁` and `p₂` are contained in the polynomial semiring
  `R[s]` of finitely many variables. -/
theorem exists_finset_rename₂ (p₁ p₂ : MvPolynomial σ R) :
    ∃ (s : Finset σ) (q₁ q₂ : MvPolynomial s R), p₁ = rename (↑) q₁ ∧ p₂ = rename (↑) q₂ := by
  obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁
  obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂
  classical
    use s₁ ∪ s₂
    use rename (Set.inclusion s₁.subset_union_left) q₁
    use rename (Set.inclusion s₁.subset_union_right) q₂
    constructor <;> simp [Function.comp_def]

Finite Variable Representation for Pairs of Multivariate Polynomials

Informal description

For any two multivariate polynomials $p₁$ and $p₂$ in $R[X_i : i \in \sigma]$, there exists a finite subset $s \subseteq \sigma$ and polynomials $q₁, q₂ \in R[X_j : j \in s]$ such that $p₁$ and $p₂$ can be obtained by renaming the variables of $q₁$ and $q₂$ via the inclusion map $s \hookrightarrow \sigma$. That is, $p₁ = \text{rename}(\iota)(q₁)$ and $p₂ = \text{rename}(\iota)(q₂)$, where $\iota$ is the inclusion of $s$ into $\sigma$.

MvPolynomial.exists_fin_rename theorem

 (p : MvPolynomial σ R) : ∃ (n : ℕ) (f : Fin n → σ) (_hf : Injective f) (q : MvPolynomial (Fin n) R), p = rename f q

Full source

/-- Every polynomial is a polynomial in finitely many variables. -/
theorem exists_fin_rename (p : MvPolynomial σ R) :
    ∃ (n : ℕ) (f : Fin n → σ) (_hf : Injective f) (q : MvPolynomial (Fin n) R), p = rename f q := by
  obtain ⟨s, q, rfl⟩ := exists_finset_rename p
  let n := Fintype.card { x // x ∈ s }
  let e := Fintype.equivFin { x // x ∈ s }
  refine ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, ?_⟩
  rw [← rename_rename, rename_rename e]
  simp only [Function.comp_def, Equiv.symm_apply_apply, rename_rename]

Finite Variable Representation of Multivariate Polynomials via Injection

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, there exists a natural number $n$, an injective function $f \colon \{1,\dots,n\} \to \sigma$, and a polynomial $q \in R[X_1,\dots,X_n]$ such that $p$ can be obtained by renaming the variables of $q$ via $f$, i.e., $p = \text{rename}(f)(q)$.

MvPolynomial.eval₂_cast_comp theorem

 (f : σ → τ) (c : ℤ →+* R) (g : τ → R) (p : MvPolynomial σ ℤ) : eval₂ c (g ∘ f) p = eval₂ c g (rename f p)

Full source

theorem eval₂_cast_comp (f : σ → τ) (c : ℤℤ →+* R) (g : τ → R) (p : MvPolynomial σ ℤ) :
    eval₂ c (g ∘ f) p = eval₂ c g (rename f p) := by
  apply MvPolynomial.induction_on p (fun n => by simp only [eval₂_C, rename_C])
    (fun p q hp hq => by simp only [hp, hq, rename, eval₂_add, map_add])
    fun p n hp => by simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]

Evaluation of Renamed Integer Polynomials: $\text{eval}_2(c, g \circ f, p) = \text{eval}_2(c, g, \text{rename}(f)(p))$

Informal description

Let $f \colon \sigma \to \tau$ be a function between index types, $c \colon \mathbb{Z} \to R$ a ring homomorphism, and $g \colon \tau \to R$ a valuation function. For any multivariate polynomial $p$ with integer coefficients in variables indexed by $\sigma$, the evaluation of $p$ under the composition $g \circ f$ and homomorphism $c$ equals the evaluation of the renamed polynomial $\text{rename}(f)(p)$ under $g$ and $c$. That is: \[ \text{eval}_2(c, g \circ f, p) = \text{eval}_2(c, g, \text{rename}(f)(p)). \]

MvPolynomial.coeff_rename_mapDomain theorem

 (f : σ → τ) (hf : Injective f) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) : (rename f φ).coeff (d.mapDomain f) = φ.coeff d

Full source

@[simp]
theorem coeff_rename_mapDomain (f : σ → τ) (hf : Injective f) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) :
    (rename f φ).coeff (d.mapDomain f) = φ.coeff d := by
  classical
  apply φ.induction_on' (P := fun ψ => coeff (Finsupp.mapDomain f d) ((rename f) ψ) = coeff d ψ)
  -- Lean could no longer infer the motive
  · intro u r
    rw [rename_monomial, coeff_monomial, coeff_monomial]
    simp only [(Finsupp.mapDomain_injective hf).eq_iff]
  · intros
    simp only [*, map_add, coeff_add]

Preservation of Coefficients under Injective Variable Renaming in Multivariate Polynomials

Informal description

Let $f \colon \sigma \to \tau$ be an injective function, $\varphi$ a multivariate polynomial in variables $\sigma$ with coefficients in a commutative semiring $R$, and $d \colon \sigma \to \mathbb{N}$ a finitely supported function representing a monomial. Then the coefficient of the monomial $d \circ f$ in the renamed polynomial $\text{rename}(f)(\varphi)$ is equal to the coefficient of the monomial $d$ in $\varphi$. In symbols: \[ \text{coeff}_{d \circ f}(\text{rename}(f)(\varphi)) = \text{coeff}_d(\varphi) \]

MvPolynomial.coeff_rename_embDomain theorem

(f : σ ↪ τ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) : (rename f φ).coeff (d.embDomain f) = φ.coeff d

Full source

@[simp]
theorem coeff_rename_embDomain (f : σ ↪ τ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) :
    (rename f φ).coeff (d.embDomain f) = φ.coeff d := by
  rw [Finsupp.embDomain_eq_mapDomain f, coeff_rename_mapDomain f f.injective]

Coefficient Preservation under Injective Variable Renaming via Embedding

Informal description

Let $f \colon \sigma \hookrightarrow \tau$ be an injective function embedding, $\varphi$ a multivariate polynomial in variables $\sigma$ with coefficients in a commutative semiring $R$, and $d \colon \sigma \to_{\text{f}} \mathbb{N}$ a finitely supported function representing a monomial. Then the coefficient of the embedded monomial $\text{embDomain}\,f\,d$ in the renamed polynomial $\text{rename}\,f\,\varphi$ is equal to the coefficient of $d$ in $\varphi$. In symbols: \[ \text{coeff}_{\text{embDomain}\,f\,d}(\text{rename}\,f\,\varphi) = \text{coeff}_d(\varphi) \]

MvPolynomial.coeff_rename_eq_zero theorem

 (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ) (h : ∀ u : σ →₀ ℕ, u.mapDomain f = d → φ.coeff u = 0) :
  (rename f φ).coeff d = 0

Full source

theorem coeff_rename_eq_zero (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ)
    (h : ∀ u : σ →₀ ℕ, u.mapDomain f = d → φ.coeff u = 0) : (rename f φ).coeff d = 0 := by
  classical
  rw [rename_eq, ← not_mem_support_iff]
  intro H
  replace H := mapDomain_support H
  rw [Finset.mem_image] at H
  obtain ⟨u, hu, rfl⟩ := H
  specialize h u rfl
  simp? at h hu says simp only [Finsupp.mem_support_iff, ne_eq] at h hu
  contradiction

Vanishing Coefficients under Variable Renaming in Multivariate Polynomials

Informal description

Let $f : \sigma \to \tau$ be a function, $\varphi$ a multivariate polynomial in variables $\sigma$ with coefficients in a commutative semiring $R$, and $d : \tau \to_{\text{f}} \mathbb{N}$ a monomial in variables $\tau$. If for every monomial $u : \sigma \to_{\text{f}} \mathbb{N}$ such that $\text{mapDomain}\, f\, u = d$, the coefficient of $u$ in $\varphi$ is zero, then the coefficient of $d$ in the renamed polynomial $\text{rename}\, f\, \varphi$ is also zero.

MvPolynomial.coeff_rename_ne_zero theorem

 (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ) (h : (rename f φ).coeff d ≠ 0) :
  ∃ u : σ →₀ ℕ, u.mapDomain f = d ∧ φ.coeff u ≠ 0

Full source

theorem coeff_rename_ne_zero (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ)
    (h : (rename f φ).coeff d ≠ 0) : ∃ u : σ →₀ ℕ, u.mapDomain f = d ∧ φ.coeff u ≠ 0 := by
  contrapose! h
  apply coeff_rename_eq_zero _ _ _ h

Existence of Nonzero Preimage Coefficient under Variable Renaming in Multivariate Polynomials

Informal description

Let $f \colon \sigma \to \tau$ be a function, $\varphi$ a multivariate polynomial in variables $\sigma$ with coefficients in a commutative semiring $R$, and $d \colon \tau \to_{\text{f}} \mathbb{N}$ a monomial in variables $\tau$. If the coefficient of $d$ in the renamed polynomial $\operatorname{rename}(f)(\varphi)$ is nonzero, then there exists a monomial $u \colon \sigma \to_{\text{f}} \mathbb{N}$ such that $\operatorname{mapDomain}(f)(u) = d$ and the coefficient of $u$ in $\varphi$ is nonzero.

MvPolynomial.constantCoeff_rename theorem

{τ : Type*} (f : σ → τ) (φ : MvPolynomial σ R) : constantCoeff (rename f φ) = constantCoeff φ

Full source

@[simp]
theorem constantCoeff_rename {τ : Type*} (f : σ → τ) (φ : MvPolynomial σ R) :
    constantCoeff (rename f φ) = constantCoeff φ := by
  apply φ.induction_on
  · intro a
    simp only [constantCoeff_C, rename_C]
  · intro p q hp hq
    simp only [hp, hq, map_add]
  · intro p n hp
    simp only [hp, rename_X, constantCoeff_X, map_mul]

Preservation of Constant Term under Variable Renaming in Multivariate Polynomials

Informal description

For any function $f \colon \sigma \to \tau$ and any multivariate polynomial $\varphi \in R[X_i : i \in \sigma]$, the constant term of the polynomial obtained by renaming variables via $f$ is equal to the constant term of $\varphi$. That is, \[ \text{constantCoeff}(\text{rename}(f)(\varphi)) = \text{constantCoeff}(\varphi). \]

MvPolynomial.support_rename_of_injective theorem

 {p : MvPolynomial σ R} {f : σ → τ} [DecidableEq τ] (h : Function.Injective f) :
  (rename f p).support = Finset.image (Finsupp.mapDomain f) p.support

Full source

theorem support_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} [DecidableEq τ]
    (h : Function.Injective f) :
    (rename f p).support = Finset.image (Finsupp.mapDomain f) p.support := by
  rw [rename_eq]
  exact Finsupp.mapDomain_support_of_injective (Finsupp.mapDomain_injective h) _

Support of Renamed Polynomial under Injective Variable Mapping

Informal description

Let $p \in R[X_i : i \in \sigma]$ be a multivariate polynomial and $f \colon \sigma \to \tau$ an injective function. Then the support of the polynomial obtained by renaming variables via $f$ is equal to the image of the support of $p$ under the mapping of finitely supported functions induced by $f$. That is, \[ \operatorname{support}(\operatorname{rename}(f)(p)) = \{\operatorname{mapDomain}(f)(m) \mid m \in \operatorname{support}(p)\}. \]

Mathlib.Algebra.MvPolynomial.Rename

Main declarations

Notation