Mixing the fibre coordinates: a linear change making a linear form a coordinate

The primitive element produced by PrimitiveRelations.lean is a ℂ-linear combination ∑ c_j x_j of the fibre coordinates with c_{i₀} = 1, as in the primitive-element step of the local parametrization theorem [Fre17, Ch. I, 8.2] (see also [GR84, Chapter 3, §1]). The linear automorphism mixLinear i₀ c of ℂⁿ replaces the i₀-th coordinate by that linear form and fixes the others; substituting it (substConv, Subst.lean) sends the coordinate series X_{i₀} to ∑ c_j X_j, fixes the other coordinate series, and fixes every series embedded from the base along an injection e avoiding i₀ (convEmbed e). These are the three identities the coordinate transport of the parametrization theorem needs; all proved through the function-level characterization Conv.ext_of_evalSeries_eventuallyEq.

noncomputable def Analytic.mixFwd {n : ℕ} (i₀ : Fin n) (c : Fin n → ℂ) : (Fin n → ℂ) →ₗ[ℂ] Fin n → ℂ

The linear map x ↦ (x with x_{i₀} replaced by ∑ c_j x_j).

Equations

• Analytic.mixFwd i₀ c = LinearMap.pi fun (i : Fin n) => if i = i₀ then ∑ j : Fin n, c j • LinearMap.proj j else LinearMap.proj i

noncomputable def Analytic.mixBwd {n : ℕ} (i₀ : Fin n) (c : Fin n → ℂ) : (Fin n → ℂ) →ₗ[ℂ] Fin n → ℂ

The inverse of mixFwd when c i₀ = 1: x ↦ (x with x_{i₀} replaced by x_{i₀} − ∑_{j ≠ i₀} c_j x_j).

Equations

• Analytic.mixBwd i₀ c = LinearMap.pi fun (i : Fin n) => if i = i₀ then LinearMap.proj i₀ - ∑ j ∈ Finset.univ.erase i₀, c j • LinearMap.proj j else LinearMap.proj i

theorem Analytic.mixFwd_apply {n : ℕ} (i₀ : Fin n) (c x : Fin n → ℂ) (i : Fin n) : (mixFwd i₀ c) x i = if i = i₀ then ∑ j : Fin n, c j * x j else x i

The coordinates of mixFwd.

theorem Analytic.mixBwd_apply {n : ℕ} (i₀ : Fin n) (c x : Fin n → ℂ) (i : Fin n) : (mixBwd i₀ c) x i = if i = i₀ then x i₀ - ∑ j ∈ Finset.univ.erase i₀, c j * x j else x i

The coordinates of mixBwd.

noncomputable def Analytic.mixLinear {n : ℕ} (i₀ : Fin n) (c : Fin n → ℂ) (hc : c i₀ = 1) : (Fin n → ℂ) ≃L[ℂ] Fin n → ℂ

The linear automorphism of ℂⁿ replacing x_{i₀} by the linear form ∑ c_j x_j (c i₀ = 1) and fixing the other coordinates, as a continuous linear equivalence (the type substEquiv takes).

Equations

• Analytic.mixLinear i₀ c hc = (LinearEquiv.ofLinearMap (Analytic.mixFwd i₀ c) (Analytic.mixBwd i₀ c) ⋯ ⋯).toContinuousLinearEquiv

theorem Analytic.mixLinear_apply {n : ℕ} (i₀ : Fin n) (c : Fin n → ℂ) (hc : c i₀ = 1) (x : Fin n → ℂ) (i : Fin n) : ↑(mixLinear i₀ c hc) x i = if i = i₀ then ∑ j : Fin n, c j * x j else x i

The coordinates of mixLinear, as a continuous linear map.

theorem Analytic.substConv_mixLinear_convX_self {n : ℕ} (i₀ : Fin n) (c : Fin n → ℂ) (hc : c i₀ = 1) : substConv (↑(mixLinear i₀ c hc)) (convX ℂ i₀) = ∑ j : Fin n, (algebraMap ℂ ↥(Conv ℂ n)) (c j) * convX ℂ j

Substituting mixLinear sends the coordinate series X_{i₀} to the linear form ∑ c_j X_j.

theorem Analytic.substConv_mixLinear_convX_of_ne {n : ℕ} (i₀ : Fin n) (c : Fin n → ℂ) (hc : c i₀ = 1) {i : Fin n} (hi : i ≠ i₀) : substConv (↑(mixLinear i₀ c hc)) (convX ℂ i) = convX ℂ i

Substituting mixLinear fixes the coordinate series X_i, i ≠ i₀.

theorem Analytic.substConv_mixLinear_convEmbed {n d : ℕ} (i₀ : Fin n) (c : Fin n → ℂ) (hc : c i₀ = 1) (e : Fin d ↪ Fin n) (hi₀ : i₀ ∉ Set.range ⇑e) (a : ↥(Conv ℂ d)) : substConv (↑(mixLinear i₀ c hc)) ((convEmbed ℂ e) a) = (convEmbed ℂ e) a

Substituting mixLinear fixes every series embedded from the base along an injection e whose range avoids i₀ (the base coordinates are untouched).