What is the universal property of the algebra of formal power series over a commutative ring? Let $A$ be a commutative ring. For every set $I$, $A^{\mathbb{N}^{(I)}}$ is the algebra of formal power series.
Suppose $\sigma:I\rightarrow J$ is a bijection. Ignoring topology, what is the canonical algebra isomorphism between $A^{\mathbb{N}^{(I)}}$ and $A^{\mathbb{N}^{(J)}}$?
For example, let $(\alpha_\nu)_{\nu\in\mathbb{N}^{(I)}}$ be an element of $A^{\mathbb{N}^{(I)}}$, what should be the image of this element in $A^{\mathbb{N}^{(J)}}$?
Edit:
Since $\sigma$ is a bijection, there exists a monoid isomorphism $f:\mathbb{N}^{(I)}\rightarrow\mathbb{N}^{(J)}$ such that $$f\circ\delta=\delta'\circ\sigma,$$
where $\delta,\delta'$ are the canonical injections of $I\rightarrow\mathbb{N}^{(I)}$ and $J\rightarrow\mathbb{N}^{(J)}$, respectively. Now, from set theory, we know that the mapping
$$g:A^{\mathbb{N}^{(I)}}\rightarrow A^{\mathbb{N}^{(J)}},\,(\alpha_\nu)_{\nu\in\mathbb{N}^{(I)}}\mapsto(\alpha_{f^{-1}(\mu)})_{\mu\in\mathbb{N}^{(J)}}$$
is a bijection.
Definition: By $\mathbf{N}^{(I)}$ denote the subset of $\mathbf{N}^{I}$ consisting of sequences with finite support.
 A: A more common notation is $A[[\{T_i\}_{i \in I}]]$. If $\sigma : I \to J$ is a map (Edit: with finite fibers), it induces a unique continuous ring homomorphism $A[[\{T_i\}_{i \in I}]] \to A[[\{T_j\}_{j \in J}]]$ which extends the identity on $A$ and maps $T_i \mapsto T_{\sigma(i)}$. Thus, it maps a general power series
$$\sum_{\mu \in \mathbb{N}^{(I)}} p_{\mu} \cdot \prod_{i \in I} (T_i)^{\mu_i}$$
to the power series
$$\sum_{\mu \in \mathbb{N}^{(I)}} p_{\mu} \cdot \prod_{i \in I} (T_{\sigma(i)})^{\mu_i} = \sum_{\nu \in \mathbb{N}^{(J)}} \left(\sum_{\Large \mu \in \mathbb{N}^{(I)}, \, \nu_j = \sum_{\sigma(i)=j} \mu_i} p_{\mu}\right)\cdot \prod_{j \in J} T_j^{\nu_j}.$$
When you ignore the topology, uniqueness fails, and you need to verify that the above formula indeed defines a ring homomorphism.
The whole construction is compatible with composition (it defines a functor), so a bijection $I \to J$ gets mapped to an isomorphism $A[[\{T_i\}_{i \in I}]] \to A[[\{T_j\}_{j \in J}]]$.
A: I think @tomasz' deleted answer goes in a direction most appealing to me (at least by this point...), namely, to say that a "formal power series ring" $R[[\{x_i\}]]$ over a commutative ring $R$ (probably with identity) in variables $\{x_i:i\in I\}$ is a/the projective limit of quotients $R[\{x_i\}]/I_d$ of polynomial rings $R[\{x_i\}]$ by the ideals $I_d$ consisting of polynomials of total degree $>d$.
The projective limit characterization is that a map to the proj lim is given by a compatible family of maps to the limitands. A bijection of the index sets of the variables identifies the ideals $I_d$, etc.
Really, this amounts to an assertion that an isomorphism of index sets in the category of sets induces an isomorphism of corresponding formal power series rings (with fixed ring $R$).
In particular, and maybe this is an implicit question, the postulated uniqueness of the map to the proj lim, induced by a compatible family of maps to the limitands, shows that there is a unique self-map of that proj lim that respects all those maps. So, "unique up to unique isomorphism", with that latter qualification having some significance.
