Renaming variables, and discarding the ones outside the range

Renaming the variables of a multivariable polynomial along an equivalence e : σ ≃ τ is a ring equivalence. Mathlib's RingHomInvPair.of_ringEquiv and RingHomInvPair.of_ringEquiv_symm are deliberately not instances, so this file registers them for MvPolynomial.renameEquiv. This lets semilinear equivalences over variable renaming be used and inverted without requiring downstream local instances.

Along an injective renaming f : σ → τ, Mathlib's MvPolynomial.killCompl sets the variables outside the range of f to zero. When exactly one variable X a is discarded, the polynomials it kills are exactly the multiples of X a.

Main definitions

• TauCeti.renameRingHomInvPair: variable renaming and its inverse form a RingHomInvPair.
• TauCeti.renameRingHomInvPairSymm: the same inverse pair in the reverse direction.

Main results

• MvPolynomial.killCompl_X_of_notMem_range: a variable outside the range of an injective renaming is killed by killCompl.
• MvPolynomial.killCompl_eq_zero_iff_X_dvd: when the range of the renaming is the complement of a single variable X a, discarding that variable kills exactly the multiples of X a.
• Polynomial.map_eval_map_rename: for a polynomial family with coefficients in MvPolynomial, specializing after renaming the parameters along f is specializing at the composite point.

@[simp]

theorem MvPolynomial.killCompl_X_of_notMem_range {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) {a : τ} (ha : a ∉ Set.range f) : (killCompl hf) (X a) = 0

A variable outside the range of an injective renaming is killed by killCompl.

theorem MvPolynomial.killCompl_eq_zero_iff_X_dvd {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) {a : τ} (ha : Set.range f = {a}ᶜ) (p : MvPolynomial τ R) : (killCompl hf) p = 0 ↔ X a ∣ p

When the range of an injective renaming is the complement of a single variable X a, discarding the variables outside the range kills exactly the multiples of X a.

theorem Polynomial.map_eval_map_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] (f : σ → τ) (P : Polynomial (MvPolynomial σ R)) (y : τ → R) : map (MvPolynomial.eval y) (map (MvPolynomial.rename f).toRingHom P) = map (MvPolynomial.eval (y ∘ f)) P

Renaming the parameters of a polynomial family P : (MvPolynomial σ R)[X] along f and then specializing them at y is specializing P at y ∘ f.

instance TauCeti.renameRingHomInvPair {σ : Type u_1} {τ : Type u_2} (R : Type u_3) [CommSemiring R] (e : σ ≃ τ) : RingHomInvPair ↑(MvPolynomial.renameEquiv R e).toRingEquiv ↑(MvPolynomial.renameEquiv R e).toRingEquiv.symm

A polynomial variable-renaming ring equivalence and its inverse form a RingHomInvPair.

instance TauCeti.renameRingHomInvPairSymm {σ : Type u_1} {τ : Type u_2} (R : Type u_3) [CommSemiring R] (e : σ ≃ τ) : RingHomInvPair ↑(MvPolynomial.renameEquiv R e).toRingEquiv.symm ↑(MvPolynomial.renameEquiv R e).toRingEquiv

The inverse polynomial variable-renaming ring equivalence and the forward equivalence form a RingHomInvPair.