Roots of a Polynomial are Continuous w.r.t. Coefficients

Stream: Is there code for X?

[Fred Rajasekaran]

Is there any statement that says the map $(a_0, \dots, a_{n-1}) \to \text{roots}(z^n + a_{n-1} z^{n-1} + \dots a_0)$ is continuous? I'm viewing this as a map from $\mathbb{C}^n$ to the space of multisets of size $n$ with elements in $\mathbb{C}$. A topology on the space of multisets can be the quotient topology given by the standard topology on $\mathbb{C}^n$ modded out by permutations of the entries (i.e $(x_0, \dots x_{n-1}) \sim (y_0, \dots y_{n-1})$ if $(x_0, \dots x_{n-1}) = (y_{\sigma(0)}, \dots ,y_{\sigma(n-1)})$ for some $\sigma \in S_n$). Relevant stack exchange post.

I'm interested in a much more special case of this, so any help for the specific case would also be nice. I'm hoping to show that the map that sends an $n \times n$ matrix to its $n$ eigenvalues is continuous . The topology I'm putting on the space of matrices is the one generated by any matrix norm. The model I'm considering is Hermitian, though Matrix.IsHermitian.eigenvalues returns an indexed set (in decreasing order) and indexing would only work when all eigenvalues are real, hence why I am deciding to go with the more general multiset version. Also Polynomial.roots returns a multiset, and I don't think it's too hard to prove that Matrix.charpoly is continuous since its a polynomial in the entries of the matrix.

I would also be happy with the weaker statement that the eigenvalues are measurable functions instead of just continuous. Here, both the space of matrices and the space of multisets of fixed cardinality would be equipped with the Borel $\sigma$-algebras of their respective topologies.

[Luigi Massacci]

I think @Joseph Tooby-Smith might have asked a similar question in the past wrt eigenvalues if I did not hallucinate

[Eric Wieser]

I assume that mathlib currently doesn't have a topology instance on multisets?

[Joseph Tooby-Smith]

@Luigi Massacci I'm pretty sure I did too, or at least something along these lines, but I can't find it :rolling_on_the_floor_laughing:. At one point I was trying to work out how to show $SO(3)$ is connected which may have been it. Though in any case, I'm pretty sure the conclusion I ended up with is that something like this doesn't already exist.

[Junyan Xu]

It would be reasonable to put a topology on docs#Sym. The reasonable topology on docs#Multiset is probably as the disjoint union of the Syms? But we don't need it now.

[Junyan Xu]

Should the unordered configuration space be a subtype of Sym, or a quotient of a subtype of Fin n → _? We should probably show both are homeomorphic.

[Alex Meiburg]

#27118 has the fact that will connect your arguments for you - that the roots of charpoly are the eigenvalues.

[Fred Rajasekaran]

Junyan Xu said:

It would be reasonable to put a topology on docs#Sym. The reasonable topology on docs#Multiset is probably as the disjoint union of the Syms? But we don't need it now.

A topology (the quotient topology) on Sym might work. How much work do you think that would be? I don't have much experience with that kind of stuff in Lean.

And if I wanted to show the roots were continuous, since Polynomial.roots is a multiset, would I need to show that

abbrev mk (m : Multiset α) (h : Multiset.card m = n) : Sym α n :=
  ⟨m, h⟩

in Data/Sym/Basic.lean is continuous (and thus needing to define a topology on multisets anyway), or is there some way around that?

In regards to your second question, I'm not sure what the best type is. I will need to put a MeasurableSpace structure on it, and there are already some lemmas about quotient measurable spaces in MeasureTheory/MeasurableSpace/Constructions.lean, but I'm not sure which construction best matches with the statements there.

[Ben Eltschig]

List X is already equipped with a topology through docs#instTopologicalSpaceList, so equipping Multiset X and Sym X n with topologies should be as simple as unfolding the definitions and letting typeclass synthesis do its thing:

import Mathlib.Data.Sym.Basic
import Mathlib.Topology.List

instance {X : Type*} [TopologicalSpace X] : TopologicalSpace (Multiset X) := by unfold Multiset; infer_instance

instance {X : Type*} [TopologicalSpace X] {n : ℕ} : TopologicalSpace (Sym X n) := by unfold Sym; infer_instance

Writing API for them will probably take a bit more effort though, as instTopologicalSpaceList does not currently seem to have a lot of API itself.

[Ben Eltschig]

(In fact, I'm having a bit of trouble parsing the definition of instTopologicalSpaceList even; it's phrased in terms of traversable functors, which I'm not very familiar with. I would hope that is the same as the disjoint union topology with respect to lists of fixed length.)

[Edward van de Meent]

judging from List.instDiscreteTopology, it's just the discrete topology? i should really read these things

[Edward van de Meent]

juding from docs#nhds_cons, my guess is the topology would be the discrete union over topologies on the respective lengths?

[Yakov Pechersky]

I think the more idiomatic instance would be

import Mathlib.Data.Sym.Basic
import Mathlib.Topology.List

variable {X : Type*} [TopologicalSpace X]

instance : TopologicalSpace (Multiset X) :=
  .coinduced (Quotient.mk' : List X → Multiset X) inferInstance

lemma isQuotientMap_multiset_mk : Topology.IsQuotientMap (Quotient.mk' : List X → Multiset X) where
  surjective := Quotient.mk'_surjective
  eq_coinduced := rfl

[Ben Eltschig]

I think that's defeq to the other one, right? I first wrote .coinduced Multiset.ofList inferInstance too, but figured the pattern using unfold would be cleaner

[Ben Eltschig]

as long as they're all defeq I don't think it matters which one you use though

[Yakov Pechersky]

Yes, they are defeq.

import Mathlib.Data.Sym.Basic
import Mathlib.Topology.List

variable {X : Type*} [TopologicalSpace X]

def foo : TopologicalSpace (Multiset X) := by
  unfold Multiset; infer_instance

instance bar : TopologicalSpace (Multiset X) :=
  .coinduced (Quotient.mk' : List X → Multiset X) (inferInstanceAs (TopologicalSpace (List X)))

example : foo (X := X) = bar := rfl

[Eric Wieser]

Using ofList sounds like the best spelling to me