Permuting the variables of a convergent series

The Weierstrass division divides with respect to the first variable x_0. To divide with respect to an arbitrary fibre variable x_i (the division argument of [Fre17, Ch. I, 8.3] in FibreDivision.lean), the coordinates are permuted: for a permutation τ of Fin n, permConv τ is the K-algebra automorphism f(x) ↦ f(x_{τ 0}, …, x_{τ (n-1)}) of Conv K n (the renaming convEmbed of Embed.lean along the bijection τ). It sends the coordinate series X_i to X_{τ i} and a series embedded from the base along e to the series embedded along τ ∘ e; its inverse is permConv τ⁻¹.

theorem Analytic.convEmbed_toEmbedding_symm_apply {K : Type u_1} [RCLike K] {n : ℕ} (τ : Equiv.Perm (Fin n)) (f : ↥(Conv K n)) : (convEmbed K (Equiv.toEmbedding τ)) ((convEmbed K (Equiv.symm τ).toEmbedding) f) = f

Renaming along a permutation and then along its inverse is the identity on Conv K n (rename_rename and rename_id, through the instance-carrying rename).

noncomputable def Analytic.permConv (K : Type u_1) [RCLike K] {n : ℕ} (τ : Equiv.Perm (Fin n)) : ↥(Conv K n) ≃ₐ[K] ↥(Conv K n)

The K-algebra automorphism of Conv K n permuting the variables along τ, f(x) ↦ f(x_{τ 0}, …, x_{τ (n-1)}): convEmbed along the bijection τ, with inverse the embedding along τ⁻¹.

Equations

• Analytic.permConv K τ = AlgEquiv.ofAlgHom (Analytic.convEmbed K (Equiv.toEmbedding τ)) (Analytic.convEmbed K (Equiv.symm τ).toEmbedding) ⋯ ⋯

theorem Analytic.permConv_apply {K : Type u_1} [RCLike K] {n : ℕ} (τ : Equiv.Perm (Fin n)) (f : ↥(Conv K n)) : (permConv K τ) f = (convEmbed K (Equiv.toEmbedding τ)) f

theorem Analytic.permConv_symm_apply {K : Type u_1} [RCLike K] {n : ℕ} (τ : Equiv.Perm (Fin n)) (f : ↥(Conv K n)) : (permConv K τ).symm f = (convEmbed K (Equiv.symm τ).toEmbedding) f

theorem Analytic.permConv_convX {K : Type u_1} [RCLike K] {n : ℕ} (τ : Equiv.Perm (Fin n)) (i : Fin n) : (permConv K τ) (convX K i) = convX K (τ i)

permConv τ sends the coordinate series X_i to X_{τ i}.

theorem Analytic.permConv_convEmbed {K : Type u_1} [RCLike K] {n d : ℕ} (τ : Equiv.Perm (Fin n)) (e : Fin d ↪ Fin n) (a : ↥(Conv K d)) : (permConv K τ) ((convEmbed K e) a) = (convEmbed K (e.trans (Equiv.toEmbedding τ))) a

permConv τ sends a series embedded from the base along e to the series embedded along τ ∘ e.

theorem Analytic.permConv_symm {K : Type u_1} [RCLike K] {n : ℕ} (τ : Equiv.Perm (Fin n)) : (permConv K τ).symm = permConv K (Equiv.symm τ)

The inverse automorphism is the one of the inverse permutation.