The elementary symmetric chart is a homeomorphism

TauCeti.Sym.coeffEquiv presents the n-th symmetric power of an algebraically closed field K as the affine space Fin n → K, by sending an unordered n-tuple to the lower coefficients of the monic polynomial having it as its root multiset. That equivalence is pure algebra. This file proves that, when K is a proper normed field — ℂ being the case of interest — it is a homeomorphism for the quotient topology of TauCeti.Sym.instTopologicalSpace.

Both halves are elementary, but neither is formal:

• the coefficients are polynomial in the roots, so the chart is continuous;
• the roots are not a polynomial function of the coefficients, and continuity of the inverse is the classical statement that the roots of a monic polynomial depend continuously on its coefficients. It is obtained here from Cauchy's bound Polynomial.cauchyBound: a root of a monic polynomial is bounded by its coefficients, so the coefficient map is proper, hence closed, and a closed continuous bijection is a homeomorphism.

Main declarations

• TauCeti.Sym.continuous_coeffEquiv_comp_ofFn: the coefficients depend continuously on an ordered tuple of roots.
• TauCeti.Polynomial.analyticAt_coeff_prod_X_sub_C and TauCeti.Sym.analyticAt_coeffEquiv_ofFn: the same forward coefficient map is analytic over any nontrivially normed field.
• TauCeti.Sym.norm_le_norm_coeffEquiv_ofFn_add_one: Cauchy's bound on the symmetric power, that an ordered tuple is bounded by one more than the norm of its coefficient tuple.
• TauCeti.Sym.isProperMap_coeffEquiv_comp_ofFn: consequently the coefficient map (Fin n → K) → (Fin n → K) is proper.
• TauCeti.Sym.coeffHomeomorph: the elementary symmetric chart Sym K n ≃ₜ (Fin n → K).
• TauCeti.Sym.eventually_exists_ofFn_eq_coeffEquiv_symm: its inverse read on ordered tuples, that nearby coefficient tuples come from ordered tuples close coordinate by coordinate; this is continuity of roots with multiplicity, stated for polynomials in TauCeti/Analysis/Polynomial/ContinuityOfRoots.lean.
• TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_map: the chart induced by an open coordinate embedding, whose symmetric power is an open subspace of affine space.
• TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_ofFn_map: the chart on a product mapped into pairwise disjoint open coordinate ranges, one point in each.
• TauCeti.Sym.analyticOnNhd_coeffEquiv_map_eval_coeffEquiv_symm: applying a univariate polynomial to every point induces an analytic map in coefficient coordinates, including at tuples where points collide.

Lane F4.1 of the analytic Heegaard Floer roadmap opens with "Sym^g(Σ) geometry: smooth complex structure (elementary symmetric functions)", after Ozsváth--Szabó (arXiv:math/0101206, §2.1): a holomorphic coordinate on the surface identifies a neighbourhood in Sym^g(Σ) with an open subset of Sym^g(ℂ), and the chart below is what makes that a chart on a topological manifold; the charted structure is assembled from it in TauCeti/Geometry/Manifold/SymmetricPower.lean. Away from the diagonal the continuity proved here is upgraded to analyticity in TauCeti/Analysis/Polynomial/SimpleRoots/Basic.lean, and its assembly across the blocks of an elementary-symmetric chart, including colliding points over ℂ, is in TauCeti/Analysis/Polynomial/RootSum/Family.lean. The complex atlas is TauCeti.isManifold_symChartedSpace; the tangent-space criterion for products of locally parametrized immersed curves is TauCeti.isMaximalTotallyReal_range_fderiv_symChartAt_ofFn. For transition maps at colliding tuples, this file also handles the case induced by a univariate polynomial; the general holomorphic case over ℂ is TauCeti.Sym.analyticAt_coeffEquiv_map_coeffEquiv_symm_of_analyticAt in TauCeti/Analysis/Polynomial/RootSum.lean.

Analyticity of the coefficients

theorem TauCeti.Polynomial.analyticAt_linearMap_monicOfCoeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (Λ : Polynomial 𝕜 →ₗ[𝕜] F) (c₀ : Fin n → 𝕜) : AnalyticAt 𝕜 (fun (c : Fin n → 𝕜) => Λ (monicOfCoeff c)) c₀

The image of the monic polynomial with lower coefficients c under a linear map depends analytically on c: it is affine in c.

theorem TauCeti.Polynomial.analyticAt_coeff_prod_X_sub_C {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_2} [Fintype ι] (s : Finset ι) (k : ℕ) (v₀ : ι → 𝕜) : AnalyticAt 𝕜 (fun (v : ι → 𝕜) => (∏ i ∈ s, (Polynomial.X - Polynomial.C (v i))).coeff k) v₀

The coefficients of ∏ i ∈ s, (X - C (v i)) depend analytically on the tuple v of roots.

This is the elementary half of the chart, and the analytic counterpart of TauCeti.Sym.continuous_coeff_prod_X_sub_C: each coefficient is, up to sign, an elementary symmetric function of the roots, so the analyticity of the ring operations is all that is used.

Analyticity of the coefficients

theorem TauCeti.Sym.analyticAt_coeffEquiv_ofFn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsAlgClosed 𝕜] {n : ℕ} (v₀ : Fin n → 𝕜) : AnalyticAt 𝕜 (fun (v : Fin n → 𝕜) => (coeffEquiv 𝕜 n) (ofFn v)) v₀

The elementary symmetric chart is analytic in an ordered presentation of the tuple: by Vieta's formulas its coordinates are, up to sign, the elementary symmetric polynomials of the ordered tuple.

theorem TauCeti.Sym.analyticOnNhd_coeffEquiv_map_eval_coeffEquiv_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsAlgClosed 𝕜] {n : ℕ} (q : Polynomial 𝕜) : AnalyticOnNhd 𝕜 (fun (c : Fin n → 𝕜) => (coeffEquiv 𝕜 n) (Sym.map (fun (z : 𝕜) => Polynomial.eval z q) ((coeffEquiv 𝕜 n).symm c))) Set.univ

Applying a polynomial to a tuple is analytic in elementary symmetric coefficients. The coordinate representation is analytic everywhere, including at coefficient tuples whose corresponding points collide.

Continuity of the coefficients

theorem TauCeti.Sym.continuous_coeff_prod_X_sub_C {ι : Type u_1} {R : Type u_2} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] (s : Finset ι) (k : ℕ) : Continuous fun (f : ι → R) => (∏ i ∈ s, (Polynomial.X - Polynomial.C (f i))).coeff k

The coefficients of ∏ i ∈ s, (X - C (f i)) depend continuously on the tuple f of roots.

This is the elementary half of the chart: each coefficient is, up to sign, an elementary symmetric function of the roots, so continuity of the ring operations is all that is used.

theorem TauCeti.Sym.continuous_coeffEquiv_comp_ofFn {K : Type u_1} [NormedField K] [IsAlgClosed K] {n : ℕ} : Continuous fun (f : Fin n → K) => (coeffEquiv K n) (ofFn f)

The coefficient map (Fin n → K) → (Fin n → K), the elementary symmetric chart read on ordered tuples, is continuous.

theorem TauCeti.Sym.norm_le_norm_coeffEquiv_ofFn_add_one {K : Type u_1} [NormedField K] [IsAlgClosed K] {n : ℕ} (f : Fin n → K) : ‖f‖ ≤ ‖(coeffEquiv K n) (ofFn f)‖ + 1

Cauchy's bound on the symmetric power: the points of an unordered tuple are bounded by one more than the sup-norm of its elementary symmetric chart, because each of them is a root of the monic polynomial those coordinates present.

theorem TauCeti.Sym.isProperMap_coeffEquiv_comp_ofFn {K : Type u_1} [NormedField K] [IsAlgClosed K] {n : ℕ} [ProperSpace K] : IsProperMap fun (f : Fin n → K) => (coeffEquiv K n) (ofFn f)

The coefficient map is proper: bounded coefficients force bounded roots, by Cauchy's bound.

theorem TauCeti.Sym.isClosedMap_coeffEquiv {K : Type u_1} [NormedField K] [IsAlgClosed K] {n : ℕ} [ProperSpace K] : IsClosedMap ⇑(coeffEquiv K n)

The elementary symmetric chart is a closed map.

noncomputable def TauCeti.Sym.coeffHomeomorph (K : Type u_1) [NormedField K] [IsAlgClosed K] (n : ℕ) [ProperSpace K] : Sym K n ≃ₜ (Fin n → K)

The elementary symmetric chart on the n-th symmetric power of a proper algebraically closed normed field is a homeomorphism onto affine n-space: an unordered n-tuple is determined, continuously and with continuous inverse, by the lower coefficients of its monic polynomial.

Continuity of the inverse is the classical continuity of the roots of a monic polynomial in its coefficients; it comes from TauCeti.Sym.isProperMap_coeffEquiv_comp_ofFn, and hence from Cauchy's bound.

Equations

• TauCeti.Sym.coeffHomeomorph K n = (TauCeti.Sym.coeffEquiv K n).toHomeomorphOfContinuousClosed ⋯ ⋯

@[simp]

theorem TauCeti.Sym.coeffHomeomorph_apply (K : Type u_1) [NormedField K] [IsAlgClosed K] (n : ℕ) [ProperSpace K] (s : Sym K n) : (coeffHomeomorph K n) s = (coeffEquiv K n) s

The chart homeomorphism is the chart equivalence.

@[simp]

theorem TauCeti.Sym.coeffHomeomorph_symm_apply (K : Type u_1) [NormedField K] [IsAlgClosed K] (n : ℕ) [ProperSpace K] (f : Fin n → K) : (coeffHomeomorph K n).symm f = (coeffEquiv K n).symm f

The inverse chart homeomorphism is the inverse chart equivalence.

theorem TauCeti.Sym.eventually_exists_ofFn_eq_coeffEquiv_symm {K : Type u_1} [NormedField K] [IsAlgClosed K] {n : ℕ} [ProperSpace K] (a : Fin n → K) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (c : Fin n → K) in nhds ((coeffEquiv K n) (ofFn a)), ∃ (b : Fin n → K), ofFn b = (coeffEquiv K n).symm c ∧ ∀ (i : Fin n), ‖a i - b i‖ < ε

Continuity of roots on ordered tuples. Every coefficient tuple close enough to that of the ordered tuple a is the coefficient tuple of an ordered tuple b with each b i close to a i.

This is the continuity of (coeffHomeomorph K n).symm, read through the open quotient map TauCeti.Sym.ofFn: it matches the roots with multiplicity, not merely each root to a nearby one.

theorem TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_map {K : Type u_1} [NormedField K] [IsAlgClosed K] {n : ℕ} [ProperSpace K] {X : Type u_2} [TopologicalSpace X] {f : X → K} (hf : Topology.IsOpenEmbedding f) : Topology.IsOpenEmbedding fun (s : Sym X n) => (coeffEquiv K n) (Sym.map f s)

The elementary symmetric chart on a coordinate patch. An open coordinate embedding into K induces an open embedding of its n-th symmetric power into affine n-space, charted by the elementary symmetric functions of its points.

This is the local model of the symmetric power of a Riemann surface at a tuple all of whose points lie in one coordinate patch; a general tuple is split into such groups by TauCeti.Sym.isOpenEmbedding_sumSubtype.

theorem TauCeti.Sym.isOpenEmbedding_coeffEquiv_comp_ofFn_map {K : Type u_1} [NormedField K] [IsAlgClosed K] {n : ℕ} [ProperSpace K] {X : Fin n → Type u_2} [(i : Fin n) → TopologicalSpace (X i)] (f : (i : Fin n) → X i → K) (hf : ∀ (i : Fin n), Topology.IsOpenEmbedding (f i)) (h : Pairwise (Function.onFun Disjoint fun (i : Fin n) => Set.range (f i))) : Topology.IsOpenEmbedding fun (x : (i : Fin n) → X i) => (coeffEquiv K n) (ofFn fun (i : Fin n) => f i (x i))

The elementary symmetric chart away from the diagonal. For open coordinate embeddings with pairwise disjoint ranges, one point in each, the elementary symmetric functions chart the tuple of points: their product is an open subspace of affine n-space.

For Sym^g of a Riemann surface this is the chart in which the totally real torus of a Heegaard diagram, a product of g curves lying in disjoint pieces, is read.