Renaming variables of power series

This file establishes the rename operation on multivariate power series under a map with finite fibers, which modifies the set of variables.

Unlike polynomials, renaming variables in power series requires a finiteness condition on the map f : σ → τ between the index types. Specifically, we require that f has finite fibers, which is formalized as Filter.TendstoCofinite f. To see why this is necessary, consider a map from infinitely many variables to a single variable sending each X_i to X. The sum X_0 + X_1 + ⋯ is a valid power series in ℤ⟦X_0, X_1, ...⟧, but we cannot rename each X_i to X since its image X + X + ⋯ would have an infinite coefficient for X.

To avoid writing this assumption everywhere, we usually work with the typeclass assumption Filter.TendstoCofinite f. Note that this holds automatically if f is injective or if σ is finite.

This file is patterned after Mathlib/Algebra/MvPolynomial/Rename.lean.

Main declarations

• MvPowerSeries.rename
• MvPowerSeries.renameEquiv
• MvPowerSeries.killCompl

TODO

• Show that under appropriate substitution, MvPowerSeries.substAlgHom coincides with MvPowerSeries.rename in the CommRing case.

noncomputable def MvPowerSeries.renameFun {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [Semiring R] [Filter.TendstoCofinite f] : MvPowerSeries σ R → MvPowerSeries τ R

Implementation detail for rename. Use MvPowerSeries.rename instead.

noncomputable def MvPowerSeries.rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [CommSemiring R] [Filter.TendstoCofinite f] : MvPowerSeries σ R →ₐ[R] MvPowerSeries τ R

Rename all the variables in a multivariable power series by a map with finite fibers.

theorem MvPowerSeries.coeff_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [Filter.TendstoCofinite f] [CommSemiring R] (p : MvPowerSeries σ R) (x : τ →₀ ℕ) : (coeff x) ((rename f) p) = ∑ x ∈ ⋯.toFinset, (coeff x) p

theorem MvPowerSeries.rename_monomial {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [Filter.TendstoCofinite f] [CommSemiring R] (x : σ →₀ ℕ) (r : R) : (rename f) ((monomial x) r) = (monomial (Finsupp.mapDomain f x)) r

@[simp]

theorem MvPowerSeries.coeff_embDomain_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (e : σ ↪ τ) (p : MvPowerSeries σ R) (x : σ →₀ ℕ) : (coeff (Finsupp.embDomain e x)) ((rename ⇑e) p) = (coeff x) p

theorem MvPowerSeries.coeff_rename_eq_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [Filter.TendstoCofinite f] [CommSemiring R] (p : MvPowerSeries σ R) {x : τ →₀ ℕ} (h' : x ∉ Set.range (Finsupp.mapDomain f)) : (coeff x) ((rename f) p) = 0

@[simp]

theorem MvPowerSeries.rename_C {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [Filter.TendstoCofinite f] [CommSemiring R] (r : R) : (rename f) (C r) = C r

@[simp]

theorem MvPowerSeries.rename_X {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [Filter.TendstoCofinite f] [CommSemiring R] (i : σ) : (rename f) (X i) = X (f i)

@[simp]

theorem MvPowerSeries.rename_rename {σ : Type u_1} {τ : Type u_2} {γ : Type u_3} {R : Type u_4} (f : σ → τ) (g : τ → γ) [Filter.TendstoCofinite f] [CommSemiring R] [Filter.TendstoCofinite g] (p : MvPowerSeries σ R) : (rename g) ((rename f) p) = (rename (g ∘ f)) p

theorem MvPowerSeries.rename_comp_rename {σ : Type u_1} {τ : Type u_2} {γ : Type u_3} {R : Type u_4} (f : σ → τ) (g : τ → γ) [Filter.TendstoCofinite f] [CommSemiring R] [Filter.TendstoCofinite g] : (rename g).comp (rename f) = rename (g ∘ f)

@[simp]

theorem MvPowerSeries.rename_id {σ : Type u_1} {R : Type u_4} [CommSemiring R] : rename id = AlgHom.id R (MvPowerSeries σ R)

theorem MvPowerSeries.rename_id_apply {σ : Type u_1} {R : Type u_4} [CommSemiring R] (p : MvPowerSeries σ R) : (rename id) p = p

@[simp]

theorem MvPowerSeries.constantCoeff_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [Filter.TendstoCofinite f] [CommSemiring R] (p : MvPowerSeries σ R) : constantCoeff ((rename f) p) = constantCoeff p

theorem MvPowerSeries.rename_injective {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (e : σ ↪ τ) : Function.Injective ⇑(rename ⇑e)

theorem MvPowerSeries.rename_inj {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (e : σ ↪ τ) (p q : MvPowerSeries σ R) : (rename ⇑e) p = (rename ⇑e) q ↔ p = q

theorem MvPowerSeries.rename_map {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} (f : σ → τ) [Filter.TendstoCofinite f] [CommSemiring R] [CommSemiring S] (φ : R →+* S) (p : MvPowerSeries σ R) : (rename f) ((map φ) p) = (map φ) ((rename f) p)

theorem MvPowerSeries.rename_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_4} (f : σ → τ) [Filter.TendstoCofinite f] [CommSemiring R] (p : MvPolynomial σ R) : (rename f) ↑p = ↑((MvPolynomial.rename f) p)

noncomputable def MvPowerSeries.renameEquiv {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (e : σ ≃ τ) : MvPowerSeries σ R ≃ₐ[R] MvPowerSeries τ R

rename is an equivalence when the underlying map is an equivalence.

@[simp]

theorem MvPowerSeries.renameEquiv_apply {σ : Type u_1} {τ : Type u_2} (R : Type u_4) [CommSemiring R] (e : σ ≃ τ) (a✝ : MvPowerSeries σ R) : (renameEquiv R e) a✝ = (↑↑(rename ⇑e).toRingHom).toFun a✝

@[simp]

theorem MvPowerSeries.renameEquiv_refl {σ : Type u_1} {R : Type u_4} [CommSemiring R] : renameEquiv R (Equiv.refl σ) = AlgEquiv.refl

@[simp]

theorem MvPowerSeries.renameEquiv_symm {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : σ ≃ τ) : (renameEquiv R f).symm = renameEquiv R f.symm

@[simp]

theorem MvPowerSeries.renameEquiv_trans {σ : Type u_1} {τ : Type u_2} {γ : Type u_3} {R : Type u_4} [CommSemiring R] (e : σ ≃ τ) (f : τ ≃ γ) : (renameEquiv R e).trans (renameEquiv R f) = renameEquiv R (e.trans f)

noncomputable def MvPowerSeries.killComplFun {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (e : σ ↪ τ) (p : MvPowerSeries τ R) : MvPowerSeries σ R

Implementation detail for killCompl. Use MvPowerSeries.killCompl instead.

noncomputable def MvPowerSeries.killCompl {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (e : σ ↪ τ) : MvPowerSeries τ R →ₐ[R] MvPowerSeries σ R

Given an embedding e : σ ↪ τ, MvPowerSeries.killComplFun e is the function from R⟦τ⟧ to R⟦σ⟧ that is left inverse to rename e.injective.fiberFinite : R⟦σ⟧ → R⟦τ⟧ and sends the variables in the complement of the range of e to 0.

theorem MvPowerSeries.coeff_killCompl {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {e : σ ↪ τ} (p : MvPowerSeries τ R) (x : σ →₀ ℕ) : (coeff x) ((killCompl e) p) = (coeff (Finsupp.embDomain e x)) p

theorem MvPowerSeries.killCompl_monomial_embDomain {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {e : σ ↪ τ} (x : σ →₀ ℕ) (r : R) : (killCompl e) ((monomial (Finsupp.embDomain e x)) r) = (monomial x) r

theorem MvPowerSeries.killCompl_monomial_eq_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {e : σ ↪ τ} {x : τ →₀ ℕ} (r : R) (h : x ∉ Set.range (Finsupp.embDomain e)) : (killCompl e) ((monomial x) r) = 0

@[simp]

theorem MvPowerSeries.killCompl_C {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {e : σ ↪ τ} (r : R) : (killCompl e) (C r) = C r

@[simp]

theorem MvPowerSeries.killCompl_X {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {e : σ ↪ τ} (i : σ) : (killCompl e) (X (e i)) = X i

theorem MvPowerSeries.killCompl_X_eq_zero {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {e : σ ↪ τ} {t : τ} (h : t ∉ Set.range ⇑e) : (killCompl e) (X t) = 0

theorem MvPowerSeries.killCompl_comp_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {e : σ ↪ τ} : (killCompl e).comp (rename ⇑e) = AlgHom.id R (MvPowerSeries σ R)

@[simp]

theorem MvPowerSeries.killCompl_rename_app {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] {e : σ ↪ τ} (p : MvPowerSeries σ R) : (killCompl e) ((rename ⇑e) p) = p

theorem MvPowerSeries.killCompl_map {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] {e : σ ↪ τ} (φ : R →+* S) (p : MvPowerSeries τ R) : (killCompl e) ((map φ) p) = (map φ) ((killCompl e) p)