The symmetric power of a field, charted by elementary symmetric functions

A point of the n-th symmetric power Sym R n is an unordered n-tuple of scalars, and the monic polynomial ∏_{a ∈ s} (X - a) records exactly that information: its coefficients are the elementary symmetric functions of the tuple, up to sign. Over an algebraically closed field the correspondence is a bijection in both directions, and composing it with Mathlib's identification of monic degree-n polynomials with their lower coefficients presents Sym K n as the affine space Fin n → K.

This is the algebraic heart of the symmetric product chart: for a Riemann surface Σ the symmetric product Sym^g(Σ) is given its complex manifold structure by exactly this map, read in a holomorphic coordinate on Σ — a local identification Sym^g(ℂ) ≅ ℂ^g whose coordinates are the elementary symmetric functions of the g points. Only the pointwise algebra is settled here, and it takes no analytic input: everything below is a statement about polynomials over a commutative ring or a field. The topology of Sym^g(Σ), its complex structure, and the analysis that uses them are separate later steps.

Main declarations

• TauCeti.Sym.toMonic: the monic polynomial of degree n whose roots, with multiplicity, are the points of s : Sym R n. This is Mathlib's Polynomial.ofMultiset restricted to a fixed cardinality, repackaged so that the target subtype records the degree.
• TauCeti.Sym.coeff_toMonic: Vieta's formulas, that the k-th coefficient of toMonic s is (-1) ^ (n - k) times the (n - k)-th elementary symmetric function of s.
• TauCeti.Sym.toMonic_append, TauCeti.Sym.toMonic_cons, TauCeti.Sym.toMonic_replicate: the map is multiplicative in the tuple, so adjoining a point multiplies by a linear factor and a constant tuple gives a pure power.
• TauCeti.Sym.roots_toMonic, TauCeti.Sym.toMonic_injective, TauCeti.Sym.mem_iff_isRoot: over an integral domain the tuple is recovered from the polynomial as its root multiset, and TauCeti.Sym.toMonic_ofFn_eq_of_forall_isRoot, that a monic polynomial of degree n with n distinct roots is the monic polynomial of the unordered tuple of those roots.
• TauCeti.Sym.toMonic_coeffEquiv_symm: the inverse chart, read as a polynomial rather than as a root multiset, is TauCeti.Polynomial.monicOfCoeff, the monic polynomial with prescribed lower coefficients of TauCeti/RingTheory/Polynomial/MonicOfCoeff.lean.
• TauCeti.Sym.monicEquiv: over an algebraically closed field, taking roots with multiplicity inverts toMonic, so Sym K n is equivalent to the monic polynomials of degree n.
• TauCeti.Sym.coeffEquiv: the resulting chart Sym K n ≃ (Fin n → K), with TauCeti.Sym.coeffEquiv_apply naming its coordinates as the signed elementary symmetric functions and TauCeti.Sym.coeffEquiv_symm_apply describing the inverse as a root-taking map.
• TauCeti.Sym.coeffEquiv_one_apply and TauCeti.Sym.coeffEquiv_two_apply: the chart in degrees one and two, pinning down the sign convention.
• TauCeti.Sym.toMonic_ofFn and TauCeti.Sym.coeffEquiv_ofFn_apply: read on an ordered tuple f : Fin n → R through TauCeti.Sym.ofFn, the monic polynomial is the product ∏ i, (X - C (f i)) of linear factors and the chart reads off its coefficients.
• TauCeti.Sym.exists_map_eval_esymm_eq_eval: over a commutative ring, applying a univariate polynomial to every point of a tuple acts on each elementary symmetric function by evaluating a multivariate polynomial at the elementary symmetric functions of the tuple.
• TauCeti.Sym.exists_coeffEquiv_map_eval_coeffEquiv_symm_eq_eval: applying a univariate polynomial to every point acts by multivariate polynomials in the chart 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), the totally real tori T_α, T_β, …", after Ozsváth--Szabó (arXiv:math/0101206, §2.1). This file supplies the algebra the first clause rests on, the correspondence between an unordered tuple and its monic polynomial, and stops there; the linear algebra behind the second clause is TauCeti.IsMaximalTotallyReal.finrank_eq_half in TauCeti/LinearAlgebra/TotallyReal/Finrank.lean. Vieta's formulas, the root multiset of a split monic polynomial, the multiset-to-polynomial map itself, and the equivalence between monic polynomials of degree n and polynomials of degree < n are all Mathlib's (Multiset.prod_X_sub_C_coeff, Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq, Polynomial.ofMultiset, Polynomial.monicEquivDegreeLT); nothing is vendored here.

The monic polynomial of an unordered tuple

noncomputable def TauCeti.Sym.toMonic {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (s : Sym R n) : { p : Polynomial R // p.Monic ∧ p.natDegree = n }

The monic polynomial ∏_{a ∈ s} (X - a) of an unordered n-tuple s, bundled with its monicity and the fact that its degree is n.

The underlying polynomial is Mathlib's Polynomial.ofMultiset; the point of the subtype is that the degree is pinned to n rather than to the cardinality of the underlying multiset, which is what Polynomial.monicEquivDegreeLT consumes.

Equations

• TauCeti.Sym.toMonic s = ⟨Polynomial.ofMultiset ↑s, ⋯⟩

theorem TauCeti.Sym.coe_toMonic {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (s : Sym R n) : ↑(toMonic s) = Polynomial.ofMultiset ↑s

@[simp]

theorem TauCeti.Sym.monic_toMonic {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (s : Sym R n) : (↑(toMonic s)).Monic

@[simp]

theorem TauCeti.Sym.natDegree_toMonic {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (s : Sym R n) : (↑(toMonic s)).natDegree = n

@[simp]

theorem TauCeti.Sym.toMonic_nil {R : Type u_1} [CommRing R] [Nontrivial R] : ↑(toMonic Sym.nil) = 1

@[simp]

theorem TauCeti.Sym.toMonic_cons {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (a : R) (s : Sym R n) : ↑(toMonic (a ::ₛ s)) = (Polynomial.X - Polynomial.C a) * ↑(toMonic s)

Adjoining a point to a tuple multiplies its monic polynomial by the corresponding linear factor.

@[simp]

theorem TauCeti.Sym.toMonic_append {R : Type u_1} [CommRing R] {m n : ℕ} [Nontrivial R] (s : Sym R n) (t : Sym R m) : ↑(toMonic (s.append t)) = ↑(toMonic s) * ↑(toMonic t)

The monic polynomial of a union of two tuples is the product of their monic polynomials: this is the multiplicativity that makes Polynomial.ofMultiset an additive character.

theorem TauCeti.Sym.toMonic_ofFn {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (f : Fin n → R) : ↑(toMonic (ofFn f)) = ∏ i : Fin n, (Polynomial.X - Polynomial.C (f i))

The monic polynomial of the unordered tuple underlying an ordered one f : Fin n → R is the product of the corresponding linear factors.

@[simp]

theorem TauCeti.Sym.toMonic_replicate {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (a : R) : ↑(toMonic (Sym.replicate n a)) = (Polynomial.X - Polynomial.C a) ^ n

The monic polynomial of a constant tuple is a pure power of a linear factor.

@[simp]

theorem TauCeti.Sym.eval_toMonic {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (s : Sym R n) (x : R) : Polynomial.eval x ↑(toMonic s) = (Multiset.map (fun (a : R) => x - a) ↑s).prod

Evaluating the monic polynomial of a tuple at x multiplies together the differences between x and the points of the tuple.

theorem TauCeti.Sym.coeff_toMonic {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (s : Sym R n) {k : ℕ} (hk : k ≤ n) : (↑(toMonic s)).coeff k = (-1) ^ (n - k) * (↑s).esymm (n - k)

Vieta's formulas on the symmetric power: the k-th coefficient of the monic polynomial of an unordered n-tuple is the (n - k)-th elementary symmetric function of the tuple, up to the sign (-1) ^ (n - k).

@[simp]

theorem TauCeti.Sym.coeff_zero_toMonic {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (s : Sym R n) : (↑(toMonic s)).coeff 0 = (-1) ^ n * (↑s).prod

The constant term of the monic polynomial of a tuple is the signed product of its points.

@[simp]

theorem TauCeti.Sym.roots_toMonic {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] (s : Sym R n) : (↑(toMonic s)).roots = ↑s

Over an integral domain the points of a tuple are recovered, with multiplicity, as the roots of its monic polynomial.

theorem TauCeti.Sym.toMonic_injective {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] : Function.Injective toMonic

Over an integral domain a tuple is determined by its monic polynomial: two unordered n-tuples with the same monic polynomial are equal.

theorem TauCeti.Sym.mem_iff_isRoot {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] {a : R} {s : Sym R n} : a ∈ ↑s ↔ (↑(toMonic s)).IsRoot a

A scalar lies in a tuple exactly when it is a root of the tuple's monic polynomial.

theorem TauCeti.Sym.toMonic_ofFn_eq_of_forall_isRoot {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] {p : Polynomial R} (hp : p.Monic) (hdeg : p.natDegree = n) {w : Fin n → R} (hw : Function.Injective w) (hroot : ∀ (i : Fin n), p.IsRoot (w i)) : ↑(toMonic (ofFn w)) = p

A monic polynomial of degree n with n pairwise distinct roots is the monic polynomial of the unordered tuple of those roots: a full set of simple roots pins the polynomial down.

The chart over an algebraically closed field

Mathlib builds Polynomial.monicEquivDegreeLT and Polynomial.degreeLTEquiv as anonymous structure instances and states no apply or symm_apply lemma for either — it unfolds their definitions where it needs them, as in Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean. The four lemmas here supply those missing component lemmas once, so that the chart proofs below rewrite with named equations instead of reducing the composite equivalence.

noncomputable def TauCeti.Sym.monicEquiv (K : Type u_1) [Field K] [IsAlgClosed K] (n : ℕ) : Sym K n ≃ { p : Polynomial K // p.Monic ∧ p.natDegree = n }

Over an algebraically closed field, TauCeti.Sym.toMonic is a bijection from the n-th symmetric power onto the monic polynomials of degree n, inverted by taking roots with multiplicity.

Equations

• TauCeti.Sym.monicEquiv K n = { toFun := TauCeti.Sym.toMonic, invFun := fun (p : { p : Polynomial K // p.Monic ∧ p.natDegree = n }) => Sym.mk (↑p).roots ⋯, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.Sym.monicEquiv_apply (K : Type u_1) [Field K] [IsAlgClosed K] (n : ℕ) (s : Sym K n) : (monicEquiv K n) s = toMonic s

@[simp]

theorem TauCeti.Sym.coe_monicEquiv_symm_apply (K : Type u_1) [Field K] [IsAlgClosed K] (n : ℕ) (p : { p : Polynomial K // p.Monic ∧ p.natDegree = n }) : ↑((monicEquiv K n).symm p) = (↑p).roots

noncomputable def TauCeti.Sym.coeffEquiv (K : Type u_1) [Field K] [IsAlgClosed K] (n : ℕ) : Sym K n ≃ (Fin n → K)

The elementary symmetric chart on the n-th symmetric power of an algebraically closed field: an unordered n-tuple is determined by, and freely determines, the n lower coefficients of its monic polynomial.

By TauCeti.Sym.coeffEquiv_apply the i-th coordinate is (-1) ^ (n - i) times the (n - i)-th elementary symmetric function of the tuple.

Equations

• TauCeti.Sym.coeffEquiv K n = (TauCeti.Sym.monicEquiv K n).trans ((Polynomial.monicEquivDegreeLT n).trans (Polynomial.degreeLTEquiv K n).toEquiv)

theorem TauCeti.Sym.coeffEquiv_apply_eq_coeff {K : Type u_1} [Field K] [IsAlgClosed K] {n : ℕ} (s : Sym K n) (i : Fin n) : (coeffEquiv K n) s i = (↑(toMonic s)).coeff ↑i

The chart reads off the lower coefficients of the monic polynomial of the tuple.

@[simp]

theorem TauCeti.Sym.coeffEquiv_apply {K : Type u_1} [Field K] [IsAlgClosed K] {n : ℕ} (s : Sym K n) (i : Fin n) : (coeffEquiv K n) s i = (-1) ^ (n - ↑i) * (↑s).esymm (n - ↑i)

The coordinates of the elementary symmetric chart are the elementary symmetric functions of the tuple, in decreasing order and with alternating signs.

theorem TauCeti.Sym.coeffEquiv_ofFn_apply {K : Type u_1} [Field K] [IsAlgClosed K] {n : ℕ} (f : Fin n → K) (i : Fin n) : (coeffEquiv K n) (ofFn f) i = (∏ j : Fin n, (Polynomial.X - Polynomial.C (f j))).coeff ↑i

The chart of an unordered tuple presented by an ordered one f : Fin n → K reads off the coefficients of the product of the linear factors of f.

@[simp]

theorem TauCeti.Sym.toMonic_coeffEquiv_symm {K : Type u_1} [Field K] [IsAlgClosed K] {n : ℕ} (c : Fin n → K) : ↑(toMonic ((coeffEquiv K n).symm c)) = Polynomial.monicOfCoeff c

The inverse chart, read as a polynomial rather than as a root multiset, is TauCeti.Polynomial.monicOfCoeff: the monic polynomial of the tuple with prescribed coordinates is the monic polynomial with those lower coefficients. Equivalently, the chart itself reads off the lower coefficients of TauCeti.Sym.toMonic, which is TauCeti.Sym.coeffEquiv_apply_eq_coeff.

@[simp]

theorem TauCeti.Sym.coeffEquiv_symm_apply {K : Type u_1} [Field K] [IsAlgClosed K] {n : ℕ} (f : Fin n → K) : ↑((coeffEquiv K n).symm f) = (Polynomial.monicOfCoeff f).roots

The inverse chart sends a coefficient tuple to the root multiset of the monic polynomial it determines.

theorem TauCeti.Sym.coeffEquiv_one_apply {K : Type u_1} [Field K] [IsAlgClosed K] {s : Sym K 1} {a : K} (hs : ↑s = {a}) : (coeffEquiv K 1) s 0 = -a

In degree one the chart is negation: the single coordinate of a one-point tuple is minus that point.

theorem TauCeti.Sym.coeffEquiv_two_apply {K : Type u_1} [Field K] [IsAlgClosed K] {s : Sym K 2} {a b : K} (hs : ↑s = {a, b}) : (coeffEquiv K 2) s = ![a * b, -(a + b)]

In degree two the chart is {a, b} ↦ (ab, -(a + b)): the two lower coefficients of (X - a) (X - b) = X ^ 2 - (a + b) X + ab.

The action of a polynomial map in coefficient coordinates

theorem TauCeti.Sym.exists_map_eval_esymm_eq_eval {K : Type u_1} [CommRing K] {n : ℕ} (q : Polynomial K) : ∃ (Q : ℕ → MvPolynomial (Fin n) K), ∀ (s : Sym K n) (k : ℕ), (↑(Sym.map (fun (z : K) => Polynomial.eval z q) s)).esymm k = (MvPolynomial.eval fun (j : Fin n) => (↑s).esymm (↑j + 1)) (Q k)

Applying a polynomial to a tuple acts polynomially on the elementary symmetric functions. Over any commutative ring, for every degree k there is a multivariate polynomial Q k such that the k-th elementary symmetric function of the tuple obtained by applying q pointwise is the evaluation of Q k at the elementary symmetric functions of the original tuple, with no hypothesis excluding tuples of colliding points. This is the algebraic core of exists_coeffEquiv_map_eval_coeffEquiv_symm_eq_eval, which reads the same statement in chart coordinates.

theorem TauCeti.Sym.exists_coeffEquiv_map_eval_coeffEquiv_symm_eq_eval {K : Type u_1} [Field K] [IsAlgClosed K] {n : ℕ} (q : Polynomial K) : ∃ (Q : Fin n → MvPolynomial (Fin n) K), ∀ (c : Fin n → K), (coeffEquiv K n) (Sym.map (fun (z : K) => Polynomial.eval z q) ((coeffEquiv K n).symm c)) = fun (i : Fin n) => (MvPolynomial.eval c) (Q i)

Applying a polynomial to a tuple acts polynomially in elementary symmetric coefficients. For every coefficient tuple c, including those representing colliding points, the coefficients after applying q pointwise are evaluations of multivariate polynomials Q: exists_map_eval_esymm_eq_eval read in the signed chart coordinates given by Vieta's formulas.