The embedding of Conv K d along an injection of the coordinates

For an injection e : Fin d ↪ Fin n the series in the variables x_{e 0}, …, x_{e (d-1)} form the subring convEmbed K e (Conv K d) ⊆ Conv K n: renaming the variables along e preserves the majorant norms (‖rename e f‖_ρ = ‖f‖_{ρ ∘ e}, the general form of convNorm_liftTail), so a convergent series stays convergent. This is the inclusion 𝒪_d ⊆ 𝒪_n of Noether normalization for analytic algebras (NoetherNormalization.lean): after a linear change of coordinates, 𝒪_d → 𝒪_n / I is finite and injective for a suitable choice of d coordinates. convTail is the case e = Fin.succ.

theorem Analytic.convNorm_rename {K : Type u_1} [RCLike K] {d n : ℕ} (e : Fin d ↪ Fin n) (ρ : Fin n → NNReal) (f : MvPowerSeries (Fin d) K) : ConvNorm ρ ((MvPowerSeries.rename ⇑e) f) = ConvNorm (fun (i : Fin d) => ρ (e i)) f

Renaming the variables along an injection preserves the majorant norm, ‖rename e f‖_ρ = ‖f‖_{ρ ∘ e} (the general form of convNorm_liftTail).

theorem Analytic.rename_mem_conv {K : Type u_1} [RCLike K] {d n : ℕ} (e : Fin d ↪ Fin n) {f : MvPowerSeries (Fin d) K} (hf : f ∈ Conv K d) : (MvPowerSeries.rename ⇑e) f ∈ Conv K n

A convergent series stays convergent under a renaming of the variables along an injection (extend the radius vector by 1 off the image).

noncomputable def Analytic.convEmbed (K : Type u_1) [RCLike K] {d n : ℕ} (e : Fin d ↪ Fin n) : ↥(Conv K d) →ₐ[K] ↥(Conv K n)

The embedding 𝒪_d → 𝒪_n along an injection of the coordinates, convEmbed K e : Conv K d →ₐ[K] Conv K n, f ↦ f(x_{e 0}, …, x_{e (d-1)}).

Equations

• Analytic.convEmbed K e = ((MvPowerSeries.rename ⇑e).comp (Analytic.Conv K d).val).codRestrict (Analytic.Conv K n) ⋯

@[simp]

theorem Analytic.coe_convEmbed {K : Type u_1} [RCLike K] {d n : ℕ} (e : Fin d ↪ Fin n) (c : ↥(Conv K d)) : ↑((convEmbed K e) c) = (MvPowerSeries.rename ⇑e) ↑c

theorem Analytic.convEmbed_injective {K : Type u_1} [RCLike K] {d n : ℕ} (e : Fin d ↪ Fin n) : Function.Injective ⇑(convEmbed K e)

The embedding is injective.