Topology of finite-dimensional real vector spaces

Stream: maths

[Oliver Nash]

I recently wanted to prove a basic topological result about sets in finite-dimensional Hausdorff topological real vector spaces and I realised we don't yet have an API for these.

[Oliver Nash]

In my case I was content to sidestep this gap by simply assuming I had a norm but I did think a little about what needs to be done and I also discovered a cute blog post of Terry Tao with a nice proof that I think could be formalised immediately if someone wanted to give it a few days. Here's the post: https://terrytao.wordpress.com/2011/05/24/locally-compact-topological-vector-spaces/

[Oliver Nash]

I'm posting here because I think this would be a really fun project but I can't quite justify the diversion myself so I'm hoping somebody else might get interested.

[Oliver Nash]

For the sake of concreteness, filling in the sorrys in the below is approximately what I have in mind:

import linear_algebra.dual
import analysis.normed_space.basic

/-- Let `E` be a finite-dimensional Hausdorff topological vector space over ℝ. -/
variables {E : Type*}
variables [add_comm_group E] [topological_space E] [topological_add_group E] [t2_space E]
variables [module ℝ E] [finite_dimensional ℝ E] [has_continuous_smul ℝ E]

/-- Let `v` be a basis. -/
variables {ι : Type*} [fintype ι] (v : basis ι ℝ E)

/-- Key result: the topology is unique. -/
def basis.repr_homeo : E ≃L[ℝ] (ι → ℝ) := sorry

/-- Essentially the equivalent to `basis.repr_homeo` but can be stated without choosing a basis. -/
lemma linear_form_continuous (f : module.dual ℝ E) : continuous f := sorry

/-- Given a basis, we can define the corresponding sup norm. -/
def sup_norm_group : normed_group E := sorry

local attribute [instance] sup_norm_group

/-- It really is a norm. -/
def sup_norm_space : normed_space ℝ E := sorry

/-- And yes, it is the sup norm wrt `v`. -/
lemma sup_norm_group_eq [nonempty ι] (x : E) : ∥x∥ = ⨆ i, v.coord i x :=
sorry

local notation `|`x`|` := abs x

/-- An explicit API for accessing the topology using only the algebra. -/
lemma mem_interior_iff (x : E) {s : set E} :
  x ∈ interior s ↔ ∃ δ > (0 : ℝ), ∀ (y : E), (∀ i, |v.coord i (x - y)| < δ) → y ∈ s :=
begin
  sorry,
end

[Oliver Nash]

(hopefully I've got that right)

[Johan Commelin]

Note that the uniqueness of the topology is also a theorem about local fields. There must be a common generalisation to suitable topological fields.

[Johan Commelin]

This theorem in the case of local fields is really useful in setting up the basic API for local fields, because it allows one to show that finite extensions of local fields are again local.

[Oliver Nash]

I think I also found some notes of Keith Conrad that possibly give an argument in this generality.

[Oliver Nash]

I haven't studied these notes closely but this is what I was remembering: https://kconrad.math.uconn.edu/blurbs/topology/finite-dim-TVS.pdf

[Oliver Nash]

But I think it would be great even if someone just did this for the reals.

[Sebastien Gouezel]

This is true for any complete field. Done for instance in Bourbaki. The proof given in analysis.normed_space.finite_dimension does essentially this, modulo the fact that it is done only on normed spaces. The missing ingredient is that there is a unique topology in one dimension (i.e., on the field itself).

[Oliver Nash]

Great! So you're saying we're already very close to being able to drop the normed_group, normed_space typeclasses in docs#linear_map.continuous_of_finite_dimensional ?

[Sebastien Gouezel]

Yes. I wrote it this way mainly out of lazyness, but there is a version of essentially the same proof working over any complete field.

[Kevin Buzzard]

On both the reals and the p-adics the topology is determined uniquely by the field structure. For the reals x is close to zero iff 1/n+x and 1/n-x are both squares for some large n, and for p-adics x is close to 1 iff it is an m'th power for all m coprime to p and has a p^nth root for some large n. I don't quite know whether this is relevant though.

[Heather Macbeth]

Related discussion going on at
https://github.com/leanprover-community/mathlib/pull/9379#discussion_r715996817
by the way.

[Antoine Chambert-Loir]

By the way, the stuff over any complete fields is the first chapter of Weil's Basic number theory, and is at the heart of his topological presentation of class field theory.

[Sebastien Gouezel]

For me, the standard reference is [Bourbaki, EVT I, page 14, théorème 2]. It's possibly exactly the same as Weil's.