feat(PowerSeries): rename a power series as multivariate power series

Mathlib/RingTheory/MvPowerSeries/Basic.lean

@@ -918,6 +918,11 @@ theorem _root_.MvPowerSeries.monomial_smul_eq (e : σ →₀ ℕ) (p : ℕ) (r :
     (by simp), Finsupp.prod]
   simp [pow_mul]
 
+theorem _root_.MvPowerSeries.monomial_mapDomain_eq_prod {τ : Type*} (d : σ →₀ ℕ) (f : σ → τ) :
+    MvPowerSeries.monomial (mapDomain f d) (1 : R)
+      = d.prod fun s e ↦ MvPowerSeries.X (f s) ^ e := by
+  simp [pow_add, prod_sum_index, MvPowerSeries.monomial_one_eq, mapDomain]
+
 section Algebra
 
 variable (A : Type*) [CommSemiring A] [Algebra R A]

Mathlib/RingTheory/MvPowerSeries/Equiv.lean

@@ -1,14 +1,16 @@
 /-
 Copyright (c) 2026 Bingyu Xia. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Bingyu Xia
+Authors: Bingyu Xia, Wenrong Zou
 -/
 module
 
 public import Mathlib.Algebra.Lie.OfAssociative
 public import Mathlib.RingTheory.AdicCompletion.Algebra
 public import Mathlib.RingTheory.MvPolynomial.Ideal
 public import Mathlib.RingTheory.MvPowerSeries.Trunc
+public import Mathlib.RingTheory.MvPowerSeries.Rename
+public import Mathlib.RingTheory.PowerSeries.Substitution
 
 /-!
 # Equivalences related to power series rings
@@ -23,6 +25,8 @@ This file establishes a number of equivalences related to power series rings.
 
 @[expose] public section
 
+universe u v w
+
 noncomputable section
 
 namespace MvPowerSeries
@@ -157,3 +161,79 @@ lemma toAdicCompletionAlgEquiv_symm_apply
 end toAdicCompletion
 
 end MvPowerSeries
+
+section toMvPowerSeries
+
+variable {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S]
+variable {σ τ : Type*} {f : PowerSeries R} (i : σ) (r : R)
+
+open Function PowerSeries Filter Finsupp
+namespace PowerSeries
+
+/-- Given a power series p(X) ∈ R⟦X⟧ and an index i, we may view it as a
+multivariate power series p(X_i) ∈ R⟦X_1, ..., X_n⟧.
+-/
+noncomputable
+def toMvPowerSeries : PowerSeries R →ₐ[R] MvPowerSeries σ R :=
+  MvPowerSeries.rename (fun _ => i)
+
+theorem toMvPowerSeries_apply : f.toMvPowerSeries i = f.rename (fun _ => i) := rfl
+
+theorem toMvPowerSeries_C : (C r).toMvPowerSeries i = MvPowerSeries.C r := by
+  have : C r = MvPowerSeries.C r := rfl
+  rw [toMvPowerSeries_apply, this, MvPowerSeries.rename_C]
+
+theorem toMvPowerSeries_X : X.toMvPowerSeries i = MvPowerSeries.X i (R := R) := by
+  rw [toMvPowerSeries_apply, X, MvPowerSeries.rename_X]
+
+theorem toMvPowerSeries_injective (i : σ) : Function.Injective (toMvPowerSeries (R := R) i) :=
+  MvPowerSeries.rename_injective (Embedding.punit i)
+
+section CommRing
+
+variable {R : Type*} [CommRing R] {f : PowerSeries R} (i : σ) (r : R) (p : R⟦X⟧)
+
+theorem toMvPowerSeries_eq_subst : f.toMvPowerSeries i = f.subst (MvPowerSeries.X i) := by
+  rw [toMvPowerSeries_apply, MvPowerSeries.rename_eq_subst, comp_def, subst]
+
+theorem HasSubst.toMvPowerSeries (hf : f.constantCoeff = 0) :
+    MvPowerSeries.HasSubst (f.toMvPowerSeries · (σ := σ)) (S := R) where
+  const_coeff := by simp_all [constantCoeff, toMvPowerSeries_apply]
+  coeff_zero d := Set.Finite.subset (Finite.of_fintype ↥d.support) fun s => by classical
+    contrapose
+    simp only [SetLike.mem_coe, mem_support_iff, Decidable.not_not, Set.mem_setOf_eq]
+    have : (MvPowerSeries.subst (MvPowerSeries.X (R := R) ∘ fun x ↦ s) f)
+      = f.subst (MvPowerSeries.X s) := rfl
+    intro hd
+    rw [toMvPowerSeries_apply, MvPowerSeries.rename_eq_subst, this, coeff_subst (HasSubst.X _),
+      finsum_eq_zero_of_forall_eq_zero]
+    intro n
+    by_cases! hn : n = 0
+    · simp [hn, hf]
+    have : d ≠ single s n := ne_iff.mpr ⟨s, by simp [hd, hn.symm]⟩
+    rw [MvPowerSeries.X_pow_eq, MvPowerSeries.coeff_monomial, if_neg this, smul_zero]
+
+theorem toMvPowerSeries_val {a : σ → MvPowerSeries τ R} (i : σ)
+    (ha : MvPowerSeries.HasSubst a) : (f.toMvPowerSeries i).subst a = f.subst (a i) := by
+  rw [toMvPowerSeries_eq_subst, subst, MvPowerSeries.subst_comp_subst_apply
+    (HasSubst.const (HasSubst.X _)) ha, MvPowerSeries.subst_X ha, subst]
+
+end CommRing
+
+end PowerSeries
+
+variable (f : σ → τ) [TendstoCofinite f] (a : σ) (p : R⟦X⟧)
+
+@[simp]
+lemma MvPowerSeries.rename_comp_toMvPowerSeries :
+    (rename (R := R) f).comp (PowerSeries.toMvPowerSeries a)
+      = PowerSeries.toMvPowerSeries (f a) := by
+  ext
+  simp [toMvPowerSeries_apply, comp_def]
+
+@[simp]
+lemma MvPowerSeries.rename_toMvPowerSeries :
+    (p.toMvPowerSeries a).rename f = p.toMvPowerSeries (f a) :=
+  DFunLike.congr_fun (rename_comp_toMvPowerSeries ..) p
+
+end toMvPowerSeries

Mathlib/RingTheory/MvPowerSeries/Rename.lean

@@ -6,7 +6,7 @@ Authors: Riccardo Brasca, Bingyu Xia
 module
 
 public import Mathlib.Order.Filter.TendstoCofinite
-public import Mathlib.RingTheory.MvPowerSeries.Basic
+public import Mathlib.RingTheory.MvPowerSeries.Substitution
 public import Mathlib.Algebra.MvPolynomial.Rename
 
 /-!
@@ -35,11 +35,6 @@ This file is patterned after `Mathlib/Algebra/MvPolynomial/Rename.lean`.
 * `MvPowerSeries.renameEquiv`
 * `MvPowerSeries.killCompl`
 
-## TODO
-
-* Show that under appropriate substitution, `MvPowerSeries.substAlgHom` coincides with
-  `MvPowerSeries.rename` in the `CommRing` case.
-
 -/
 
 @[expose] public section
@@ -291,4 +286,31 @@ theorem killCompl_map (φ : R →+* S) (p : MvPowerSeries τ R) :
 
 end CommSemiring
 
+section CommRing
+
+variable {R : Type*} [CommRing R] (p : MvPowerSeries σ R)
+
+lemma HasSubst.X_comp : HasSubst (X ∘ f : σ → MvPowerSeries τ R) where
+  const_coeff := by simp
+  coeff_zero d := Set.Finite.subset (d.support.finite_toSet.biUnion'
+    (fun i _ ↦ TendstoCofinite.finite_preimage_singleton f i)) (fun x => by
+      contrapose; intro _ _; classical simp_all [coeff_X])
+
+theorem rename_eq_subst : rename f p = p.subst (X ∘ f) := by
+  classical
+  ext n
+  rw [coeff_rename, coeff_subst (HasSubst.X_comp _) p n, finsum_eq_sum _
+    (coeff_subst_finite (HasSubst.X_comp _) p n)]
+  have (d : σ →₀ ℕ) (hd : ¬(coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) = 0) :
+      mapDomain f d = n := by
+    simp_rw [← monomial_mapDomain_eq_prod] at hd
+    exact (eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hd)).symm
+  refine (Finset.sum_subset_zero_on_sdiff ?_ ?_ (fun x hx => ?_)).symm
+  · exact Set.Finite.toFinset_mono this
+  · simp +contextual [← monomial_mapDomain_eq_prod]
+  · simp only [Set.Finite.mem_toFinset] at hx
+    simp [← this _ hx, ← monomial_mapDomain_eq_prod, coeff_monomial_same]
+
+end CommRing
+
 end MvPowerSeries